Nuprl - hol_list_2 LEMMAs for map_append

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

Theorem	Name
Thm* 'a,'b:S, f:('a'b), l1,l2:'a List. Thm* map(f;l1 @ l2) = (map(f;l1) @ map(f;l2))	[map_append_2]
cites the following:
Thm* 'a,'b:S. Thm* all Thm* (f:'a 'b. all Thm* (f:'a 'b. (l1:hlist('a). all Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). equal Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). (map(f,append(l1,l2)) Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). ,append Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). ,(map(f,l1) Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). ,,map(f,l2))))))	[hmap_append_2]

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