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)). (l:'a List. \|\|l\|\| = 0 P(l)) P(nil)	[length_eq_nil]
cites the following:
Thm* 'a:S. Thm* all Thm* (P:hlist('a) hbool. equal Thm* (P:hlist('a) hbool. (all Thm* (P:hlist('a) hbool. ((l:hlist('a). implies(equal(length(l),0),P(l))) Thm* (P:hlist('a) hbool. ,P(nil)))	[hlength_eq_nil]

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