1. A : Type
2. i : 
3. 0<i
4. L:A List. 
4. i-1+1<||L||
4. 
4. (X,Y:A List.
4. (L = (X @ [L[(i-1)]; L[(i-1+1)]] @ Y)
4. (& swap(L;i-1;i-1+1) = (X @ [L[(i-1+1)]; L[(i-1)]] @ Y))
5. L : A List
6. i+1<||L||
7. ||tl(L)|| = ||L||-1
8. X : A List
9. Y : A List
10. tl(L) = (X @ [tl(L)[(i-1)]; tl(L)[(i-1+1)]] @ Y)
11. swap(tl(L);i-1;i-1+1) = (X @ [tl(L)[(i-1+1)]; tl(L)[(i-1)]] @ Y)
  swap(tl(L);i-1;i+1-1) = (X @ [L[(i+1)]; L[i] / Y])

By:	RWO Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)] -1

1

11. swap(tl(L);i-1;i-1+1) = (X @ [L[(i-1+1+1)]; L[(i-1+1)]] @ Y)   swap(tl(L);i-1;i+1-1) = (X @ [L[(i+1)]; L[i] / Y])

1 step

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