1. A : Type
  L:A List. 
  0+1<||L||
  
  (X,Y:A List.
  (L = (X @ [L[0]; L[(0+1)]] @ Y) & swap(L;0;0+1) = (X @ [L[(0+1)]; L[0]] @ Y))

1	2. L : A List 3. 1<||L||   L = [L[0]; L[1] / tl(tl(L))]	9 steps
2	2. L : A List 3. 1<||L||   swap(L;0;1) = [L[1]; L[0] / tl(tl(L))]	9 steps

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