Nuprl - hol_list_2 LEMMAs for cons

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

Theorem	Name
Thm* 'a:S, h:'a, t:'a List, h':'a, t':'a List. Thm* cons(h; t) = cons(h'; t') h = h' & t = t'	[cons_11]
cites the following:
Thm* 'a:S. Thm* all Thm* (h:'a. all Thm* (h:'a. (t:hlist('a). all Thm* (h:'a. (t:hlist('a). (h':'a. all Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). equal Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). (equal Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ((cons(h,t) Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). (,cons(h',t')) Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,and Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,(equal(h,h') Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,,equal(t,t')))))))	[hcons_11]

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