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

is mentioned by

Thm* Q:((T List)Prop).  Thm* Q(nil) Thm*  Thm* (x:T. Q([x])) Thm*  Thm* (ys,ys':T List. Q(ys)  Q(ys')  Q(ys @ ys'))  (zs:T List. Q(zs))	[list_append_ind]
Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i]	[select_append_front]
Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)]	[select_append_back]
Thm* as,bs:T List. rev(as @ bs) = (rev(bs) @ rev(as))	[reverse_append]
Thm* f:(AB), as,as':A List. map(f;as @ as') = (map(f;as) @ map(f;as'))	[map_append]
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||	[length_append]
Thm* as:T List. (as @ nil) = as	[append_back_nil]
Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs))	[append_assoc]
Def rev(as) == Case of as; nil  nil ; a.as'  rev(as') @ [a]  (recursive)	[reverse]

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