(5steps total) PrintForm hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: union wf stype 1 1 1
1. 'a : Type
2. x:'a. True
3. 'b : Type
4. x:'b. True
  x:'a+'b. True
By: AllHyps Analyze THEN StrongAuto

Generated subgoal:

1 2. 'a
3. True
4. 'b : Type
5. 'b
6. True
  x:'a+'b. True
1 step

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

(5steps total) PrintForm hol Sections HOLlib Doc