Nuprl - Proof: hand def

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hand def

equal

(and

t1:hbool.

t2:hbool. all(

t:hbool. implies(implies(t1,implies(t2,t)),t)))

By:	Simpset [`hol_to_nuprl`] THEN Simp THEN StrongAuto

Generated subgoal:

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

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html