Nuprl - hol_list_2 LEMMAs for eq

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

Theorem	Name
Thm* 'a:S, h1,h2:'a. Thm* h1 = h2 (l1,l2:'a List. l1 = l2 cons(h1; l1) = cons(h2; l2))	[eq_list]
cites the following:
Thm* 'a:S. Thm* all Thm* (h1:'a. all Thm* (h1:'a. (h2:'a. implies Thm* (h1:'a. (h2:'a. (equal(h1,h2) Thm* (h1:'a. (h2:'a. ,all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). implies Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (equal(l1,l2) Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,equal Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,(cons(h1,l1) Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,,cons(h2,l2))))))))	[heq_list]

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