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

is mentioned by

Thm* 'a:S.  Thm* all Thm* (e:'a. all Thm* (e:'a. (f:'a  hnum  'a. exists_unique Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. and Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. (equal(fn1(0),e) Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,all Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. equal Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. (fn1(suc(n)) Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. ,f Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. ,(fn1(n) Thm* (e:'a. (f:'a  hnum  'a. (fn1:hnum  'a. ,(n:hnum. ,,n)))))))

[hnum_axiom]

In prior sections: hol bool

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