(module compatible-closure mzscheme
  (require "../gui.ss" 
           "../reduction-semantics.ss")
  
  (define grammar
    (language
     (B t
        f
        (B * B))))

  (define r
    (list
     (reduction/name "false" grammar (f * B_1) (term B_1)) ; [a]
     (reduction/name "true" grammar (t * B_1) (term t)))) ; [b]

  (define (compatible-closure-wrt-B a-reduction)
    (compatible-closure a-reduction grammar 'B))

  (define ->r (map compatible-closure-wrt-B r))

  (traces grammar ->r '((f * f) * (t * f))))