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)
  [hd(L) / tl(L)] = [hd(L) / (X @ [L[i]; L[(i+1)] / Y])]

1

tl(L) = (X @ [L[i]; L[(i+1)] / Y])

1 step

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