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

is mentioned by

Thm* 'b,'a:S. Thm* all Thm* (x:'b. all Thm* (x:'b. (f:'b Thm* (x:'b. ( 'a Thm* (x:'b. ( hlist('a) Thm* (x:'b. ( 'b. exists_unique Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. and Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. (equal(fn1(nil),x) Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,all Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. all Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). equal Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). (fn1 Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ((cons(h,t)) Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,f Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,(fn1(t) Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,,h Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,,t))))))))

[hlist_axiom]

In prior sections: hol bool hol prim rec

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