(declare bool type)
(declare tt bool)
(declare ff bool)

(declare holds (! b bool type))
(declare and (! a bool (! b bool bool)))

(declare-rule pf_and
              ((: a bool)
               (: b bool)
               (holds a)
               (holds b))
              (holds (and a b)))

(check
  (% a bool
  (% b bool
  (% pf_a (holds a)
  (% pf_b (holds b)
  (: (holds (and a b))
     (pf_and a b pf_a pf_b)))))))
(check
  (% a bool
  (% b bool
  (% pf_a (holds a)
  (% pf_b (holds b)
  (: (holds (and a b))
     (pf_and _ _ pf_a pf_b)))))))