Nuprl - hol_list_2 LEMMAs for length_append

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\|\| = \|\|l1\|\|+\|\|l2\|\|	[length_append_2]
cites the following:
Thm* 'a:S. Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). equal Thm* (l1:hlist('a). (l2:hlist('a). (length(append(l1,l2)) Thm* (l1:hlist('a). (l2:hlist('a). ,add(length(l1),length(l2)))))	[hlength_append_2]

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