(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
1. 'a : Type
2. 'a
3. True
4. 'b : Type
5. 'b
6. True
  x:'a+'b. True
By: DTerm inr(x) 0 THEN StrongAuto

Generated subgoals:

None

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

(5steps total) PrintForm hol Sections HOLlib Doc