P:(A
AProp), X,Y:A List, a,b:A.
Thm* P(a,b)
((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y))a,b:T List. ||a|| = ||b|| 
(i:
. i<||a|| a[i] = b[i]) a = bas,bs:T List. ||as @ bs|| = ||as||+||bs|| L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))]as,bs:T List, i:||as||. (as @ bs)[i] = as[i]as,bs:T List, i:{||as||..(||as||+||bs||)
}. (as @ bs)[i] = bs[(i-||as||)]a:T, as:T List, i:. 0<i i
||as|| [a / as][i] = as[(i-1)]