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

is mentioned by

Thm* 'a:S.  Thm* all Thm* (l:hlist('a). all Thm* (l:hlist('a). (n:hnum. equal Thm* (l:hlist('a). (n:hnum. (equal(length(l),suc(n)) Thm* (l:hlist('a). (n:hnum. ,exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). and Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). (equal(length(l'),n) Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,equal Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,(l Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,,cons(h,l'))))))))

[hlength_cons_2]

Thm* 'a:S.  Thm* all Thm* (l:hlist('a). or Thm* (l:hlist('a). (equal(l,nil) Thm* (l:hlist('a). ,exists(t:hlist('a). exists(h:'a. equal(l,cons(h,t))))))

[hlist_cases]

In prior sections: hol bool hol num hol pair hol prim rec hol restr binder hol list 1

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