Def (x:T. b(x))(x) == b(x)

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.  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]
Def every == p:'a. l:'a List. every(p;l)	[hevery]
Def el == n:. l:'a List. if n=0 then hd(l) else el(n-1,tl(l)) fi  Def (recursive)	[hel]
Def map2 == f:'a'b. l1:'a. l2:'b. map2(f;l1;l2)	[hmap2]
Def map == f:'a'b. l:'a List. map(f;l)	[hmap]
Def length == l:'a List. ||l||	[hlength]
Def flat == l:('a List) List. flatten(l)	[hflat]
Def append == l1:'a List. l2:'a List. l1 @ l2	[happend]
Def it_sum == l: List. it_sum(l)	[hit_sum]
Def tl == l:'a List. tl(l)	[htl]
Def hd == l:'a List. if null(l) then arb('a) else head(l) fi	[hhd]
Def null == l:'a List. null(l)	[hnull]
Def cons == x:'a. l:'a List. cons(x; l)	[hcons]
Def abs_list == r:('a). @a:'a List. (r = rep_list('a;a))	[habs_list]
Def rep_list == l:'a List. rep_list('a;l)	[hrep_list]
Def is_list_rep Def == r:('a). f:'a Def == r:('a). n: Def == r:('a). (r Def == r:('a). = <m:. if m<n then f(m) else @x:'a. true fi ,n>)	[his_list_rep]
Def rep_list('a;l) == <n:. if n<||l|| then l[n] else arb('a) fi ,||l||>	[rep_list]

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

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