(7steps total) PrintForm Definitions Lemmas hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hexists def 1 1 1 2
1. 'a : S
2. P : 'a
3. P(@x:'a. (P(x)))
  x:'a. P(x)
By: DTerm (@x:'a. (P(x))) 0 THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

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