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))
  L:A List. 
  i+1<||L||
  
  (X,Y:A List.
  (L = (X @ [L[i]; L[(i+1)]] @ Y) & swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))

By:	Auto THEN AssertBY (||tl(L)|| = ||L||-1) (RWW Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1   0) THEN ListDecomp [2;2;1;2] 0 THEN ListDecomp [2;2;2;2;1] 0 THEN InstHyp [tl(L)] 4

1

5. L : A List 6. i+1<||L|| 7. ||tl(L)|| = ||L||-1   8. X,Y:A List. 8. tl(L) = (X @ [tl(L)[(i-1)]; tl(L)[(i-1+1)]] @ Y) 8. & swap(tl(L);i-1;i-1+1) = (X @ [tl(L)[(i-1+1)]; tl(L)[(i-1)]] @ Y)   X,Y:A List.   [hd(L) / tl(L)] = (X @ [L[i]; L[(i+1)]] @ Y)   & swap([hd(L) / tl(L)];i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y)

6 steps

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