Nuprl - hol_list_2 LEMMAs for length_cons

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

Theorem	Name
Thm* 'a:S, l:'a List, n:. Thm* \|\|l\|\| = n+1 (h:'a, l':'a List. \|\|l'\|\| = n & l = cons(h; l'))	[length_cons_2]
cites the following:
Thm* 'a:S. Thm* all Thm* (l:hlist('a). all Thm* (l:hlist('a). (n:hnum. equal Thm* (l:hlist('a). (n:hnum. (equal(length(l),suc(n)) Thm* (l:hlist('a). (n:hnum. ,exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). and Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). (equal(length(l'),n) Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,equal Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,(l Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,,cons(h,l'))))))))	[hlength_cons_2]

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