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

(declare holds (! b bool type))
(declare impl (! a bool (! b bool bool)))
(declare pf_impl (! hyp bool
                 (! conc bool
                 (! continuation (! pf_hyp (holds hyp) (holds conc))
                 (holds (impl hyp conc))))))

; without sugar
(check (% b bool
       (: (holds (impl b b))
          (pf_impl b b (\ pf_b pf_b)))))

; with sugar
(check (% b bool
       (: (holds (impl b b))
          (pf_impl b b (lam pf_b pf_b)))))