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

1

(p:. q:. p  q) = (t1:. t2:. t:. t1tt2tt)

6 steps

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