Def concat(ll) == reduce(l,l'. l @ l';nil;ll)

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* ll:(T List) List, x:T. (x  concat(ll))  (l:T List. (l  ll) & (x  l))	[member-concat]
Thm* ll:(T List) List, n:||concat(ll)||. Thm* m:||ll||.  Thm* ||concat(firstn(m;ll))||n Thm* & n-||concat(firstn(m;ll))||<||ll[m]|| Thm* & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]	[select_concat]
Thm* l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll))	[concat-cons]
Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))	[concat_append]

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