T:Type, L:T List, x:T, i,j:{1..(||L||+1)}.
  swap([x / L];i;j) = [x / swap(L;i-1;j-1)]

By:	Auto THEN BackThru Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b THEN Reduce 0

1	1. T : Type 2. L : T List 3. x : T 4. i : {1..(||L||+1)} 5. j : {1..(||L||+1)}   ||swap([x / L];i;j)|| = ||swap(L;i-1;j-1)||+1	1 step
2	1. T : Type 2. L : T List 3. x : T 4. i : {1..(||L||+1)} 5. j : {1..(||L||+1)} 6. i1 :  7. i1<||swap([x / L];i;j)||   swap([x / L];i;j)[i1] = [x / swap(L;i-1;j-1)][i1]	13 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html