(5steps total) PrintForm hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bexists btrue 1 1 1 1

1. 'a : Type
2. 'a
3. True
  x:'a. True


By: DTerm x 0 THEN StrongAuto


Generated subgoals:

None

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

(5steps total) PrintForm hol bool Sections HOLlib Doc