Nuprl - hol_list_2 LEMMAs for list_not

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

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

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