Def exists == p:'a. x:'a. (p(x))

is mentioned by

Thm* exists(f:hind  hind. and(one_one(f),not(onto(f))))	[hinfinity_ax]
Thm* 'b,'a:S. Thm* all Thm* (P:'a  hbool. all Thm* (P:'a  hbool. (rep:'b  'a. equal Thm* (P:'a  hbool. (rep:'b  'a. (type_definition(P,rep) Thm* (P:'a  hbool. (rep:'b  'a. ,and Thm* (P:'a  hbool. (rep:'b  'a. ,(all Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. all Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. implies Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. (equal Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. ((rep(x') Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. (,rep(x'')) Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. ,equal(x',x'')))) Thm* (P:'a  hbool. (rep:'b  'a. ,,all Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. equal Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. (P(x) Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,exists Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. equal Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. (x Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. ,rep(x')))))))))	[htype_definition_wd]
Thm* 'a,'b:S. Thm* all(f:'a  'b. equal(onto(f),all(y:'b. exists(x:'a. equal(y,f(x))))))	[honto_def]
Thm* 'a:S.  Thm* equal Thm* (exists_unique Thm* ,P:'a  hbool. and Thm* ,P:'a  hbool. (exists(P) Thm* ,P:'a  hbool. ,all Thm* ,P:'a  hbool. ,(x:'a. all(y:'a. implies(and(P(x),P(y)),equal(x,y))))))	[hexists_unique_def]
Thm* 'a:S. equal(exists,P:'a  hbool. P(select(P)))	[hexists_def]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html