(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 1
1. 'a : S
2. P : 'a
3. x:'a. P(x)
  P(@x:'a. (P(x)))
By: Unab [`bchoose`] THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1   P(@x:'a. (P(x)))
1 step

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