Nuprl - hol_list_2 LEMMAs for not_eq

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

Theorem	Name
Thm* 'a:S, h1,h2:'a. h1 = h2 (l1,l2:'a List. cons(h1; l1) = cons(h2; l2))	[not_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. (not(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). not 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))))))))	[hnot_eq_list]

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