equal
  (and
  ,t1:hbool. t2:hbool. all(t:hbool. implies(implies(t1,implies(t2,t)),t)))

1

(p:. q:. pq) = (t1:. t2:. t:. t1t2tt)

4 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html