Def l1  l2 == l:T List. l2 = (l1 @ l)

is mentioned by

Thm* f:((T List)), t,t':. Thm* t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t')))	[concat_map_upto]
Thm* ll1,ll2:(T List) List. ll1  ll2  concat(ll1)  concat(ll2)	[concat_iseg]
Thm* i,j:. ij  upto(i)  upto(j)	[upto_iseg]

In prior sections: mb list 1 mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html