(7steps total) PrintForm Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hor def 1 1 2 2
1. t1 : 
2. t2 : 
3. t:. (t1  t)  (t2  t)  t
4. t2
  t1  t2
By: Sel 2 (Analyze 0) THEN Simp THEN StrongAuto

Generated subgoals:

None

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

(7steps total) PrintForm Definitions hol bool Sections HOLlib Doc