Nuprl - hol_list_2 LEMMAs for append_assoc

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

Theorem	Name
Thm* 'a:S, l1,l2,l3:'a List. (l1 @ (l2 @ l3)) = ((l1 @ l2) @ l3)	[append_assoc_2]
cites the following:
Thm* 'a:S. Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). equal Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). (append(l1,append(l2,l3)) Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,append Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,(append(l1,l2) Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,,l3)))))	[happend_assoc_2]

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