Def exists_unique == p:'a. b_exists_unique('a;x.p(x))

is mentioned by

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]

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