(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 1
1. t1 : 
2. t2 : 
3. t1  t2
4. t : 
5. t1  t
6. t2  t
  t
By: Analyze 3 THEN Simp THEN StrongAuto THEN CompleteHypBackchain

Generated subgoals:

None

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

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