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

is mentioned by

Thm* 'a:S.  Thm* exists Thm* (rep:hlist('a)  hprod((hnum  'a); hnum). type_definition Thm* (rep:hlist('a)  hprod((hnum  'a); hnum). (is_list_rep Thm* (rep:hlist('a)  hprod((hnum  'a); hnum). ,rep))

[hlist_ty_def]

Thm* 'a:S.  Thm* all Thm* (r:hprod((hnum  'a); hnum Thm* (r:hprod(). equal Thm* (r:hprod(). (is_list_rep(r) Thm* (r:hprod(). ,exists Thm* (r:hprod(). ,(f:hnum  'a. exists Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. equal Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. (r Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,pair Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. cond Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. (lt(m,n) Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. ,f(m) Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,((m:hnum. ,select(x:'a. t))) Thm* (r:hprod(). ,(f:hnum  'a. (n:hnum. ,,n))))))

[his_list_rep_wd]

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

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