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))
a,b:T List. ||a|| = ||b|| 
(i:. i<||a|| a[i] = b[i]) a = bL:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| L1,L2:T List, i,j:||L1||.
Thm* L2 = swap(L1;i;j)
Thm*
Thm* L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||
& L1 = swap(L2;i;j)
Thm* & (
x:||L2||. 
x = i x = j L2[x] = L1[x])a:T, as:T List, i:. 0<i i
||as|| [a / as][i] = as[(i-1)]l:A List. ||l||
1 ||tl(l)|| = ||l||-1 L:T List, x:T, i,j:{1..(||L||+1)
}.
Thm* swap([x / L];i;j) = [x / swap(L;i-1;j-1)]
as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)]