(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
1. t1 : 
2. t2 : 
3. t:. (t1  t)  (t2  t)  t
  t1  t2
By: Assert (t1  t2) THENL [BackThru 3;Id] THEN Simp THEN StrongAuto

Generated subgoals:

1 4. t1
  t1  t2
1 step
2 4. t2
  t1  t2
1 step

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