(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
       (@ bb b
       (: bool b))))

; with sugar
(check (% b bool
       (let bb b
       (: bool b))))