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

(declare holds (! b bool type))

(check-assuming ((: b bool)
                 (: b_pf (holds b)))
                (holds b)
                b_pf)