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

is mentioned by

Thm* P:(AAProp), X,Y:A List, a,b:A. Thm* P(a,b)  ((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y))	[swap_adjacent_instance]
Thm* k:, L1,L2:(k-1) List. Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)	[compose_flips_append]
Thm* L1,L2:(TT) List. Thm* compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2)	[compose_append]
Thm* i:, L:A List. Thm* i+1<||L|| Thm*  Thm* (X,Y:A List. Thm* (L = (X @ [L[i]; L[(i+1)]] @ Y) Thm* (& swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))	[swap_adjacent_decomp]

In prior sections: list 1 mb list 1

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