Nuprl - hol_list_2 LEMMAs for length_eq

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

Theorem	Name
Thm* 'a:S, P:(('a List)), n:. Thm* (l:'a List. \|\|l\|\| = n+1 P(l)) Thm* Thm* (l:'a List. \|\|l\|\| = n (x:'a. P(cons(x; l))))	[length_eq_cons]
cites the following:
Thm* 'a:S. Thm* all Thm* (P:hlist('a) Thm* ( hbool. all Thm* ( hbool. (n:hnum. equal Thm* ( hbool. (n:hnum. (all Thm* ( hbool. (n:hnum. ((l:hlist('a). implies(equal(length(l),suc(n)),P(l))) Thm* ( hbool. (n:hnum. ,all Thm* ( hbool. (n:hnum. ,(l:hlist('a). implies Thm* ( hbool. (n:hnum. ,(l:hlist('a). (equal(length(l),n) Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). all Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). (x:'a. P(cons(x,l)))) Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l))))))	[hlength_eq_cons]

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