Def S == {T:Type| x:T. True }

is mentioned by

Thm* 'a:S. equal(nil,abs_list(pair((n:hnum. select(e:'a. t)),0)))	[hnil_def]
Thm* 'a:S.  Thm* and Thm* (all(a:hlist('a). equal(abs_list(rep_list(a)),a)) Thm* ,all Thm* ,(r:hprod((hnum  'a); hnum). equal Thm* ,(r:hprod((hnum  'a); hnum). (is_list_rep(r) Thm* ,(r:hprod((hnum  'a); hnum). ,equal(rep_list(abs_list(r)),r))))	[hlist_iso_def]
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. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)	[list_iso]
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]
Thm* 'a:S. hlist('a)  S	[hlist_wf]
Thm* 'a:S. el  (hnum  hlist('a)  'a)	[hel_wf]
Thm* 'a:S. hd  (hlist('a)  'a)	[hhd_wf]
Thm* 'a:S, n:, l:'a List. n<||l||  el(n,l) = l[n]	[hel_nuprl]
Thm* 'a:S, l:'a List. mt(l)  hd(l) = head(l)	[hhd_nuprl]
Thm* 'a:S. 'a List  S	[list_wf_stype]
Thm* 'a:S, l:'a List. rep_list('a;l)  ('a)	[rep_list_wf]

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

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