Nuprl - mb_event_system_1 LEMMAs for concat_map

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

Rank	Theorem	Name
3	Thm* f:((T List)), t,t':. Thm* t<t' concat(map(f;upto(t))) @ (f(t)) concat(map(f;upto(t')))	[concat_map_upto]
cites the following:
0	Thm* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))	[map_append_sq]
1	Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))	[concat_append]
0	Thm* l:T List. (l @ nil) ~ l	[append_nil_sq]
0	Thm* l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll))	[concat-cons]
2	Thm* ll1,ll2:(T List) List. ll1 ll2 concat(ll1) concat(ll2)	[concat_iseg]
0	Thm* f:(AB), L1,L2:A List. L1 L2 map(f;L1) map(f;L2)	[iseg_map]
2	Thm* i,j:. ij upto(i) upto(j)	[upto_iseg]

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