Nuprl - hol_list_2 LEMMAs for hcons

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
8	Thm* 'a:S. Thm* all Thm* (h:'a. all Thm* (h:'a. (t:hlist('a). equal Thm* (h:'a. (t:hlist('a). (cons(h,t) Thm* (h:'a. (t:hlist('a). ,abs_list Thm* (h:'a. (t:hlist('a). ,(pair Thm* (h:'a. (t:hlist('a). ,(((m:hnum. cond Thm* (h:'a. (t:hlist('a). ,(((m:hnum. (equal(m,0) Thm* (h:'a. (t:hlist('a). ,(((m:hnum. ,h Thm* (h:'a. (t:hlist('a). ,(((m:hnum. ,fst(rep_list(t),pre(m)))) Thm* (h:'a. (t:hlist('a). ,(,suc(snd(rep_list(t))))))))	[hcons_def]
cites the following:
2	Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'a, r:'b. Thm* iso_pair('a;'b;P;rep;abs) rep(a) = r a = abs(r)	[iso_pair_rep_to_abs]
7	Thm* 'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)	[list_iso]
0	Thm* a:T, as:T List, i:. i0 cons(a; as)[i] = a	[select_cons_hd]
0	Thm* a:T, as:T List, i:. 0<i i\|\|as\|\| cons(a; as)[i] = as[(i-1)]	[select_cons_tl]
0	Thm* l:A List. \|\|l\|\|0	[non_neg_length]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html