Def as @ bs == Case of as; nil  bs ; a.as'  [a / (as' @ bs)]  (recursive)

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* l:T List, x:T. (x  l)  (l1,l2:T List. l = (l1 @ [x] @ l2))	[l_member_decomp]
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]
Thm* L1,L2:Top List, n:(||L1||+1). firstn(n;L1 @ L2) ~ firstn(n;L1)	[firstn_append]
Thm* P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B))	[filter_append_sq]
Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	[upto_decomp]
Thm* as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs)	[append_assoc_sq]
Def concat(ll) == reduce(l,l'. l @ l';nil;ll)	[concat]
Def upto(n) == if n=0 nil else upto(n-1) @ [(n-1)] fi  (recursive)	[upto]

In prior sections: list 1 mb list 1 mb list 2

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