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

By:	without_lemmas [`hd_wf_listp`] (RWO (Thm* L:T List, x:T, i,j:{1..(||L||+1)}. (Thm* swap([x / L];i;j) = [x / swap(L;i-1;j-1)] (0 (THEN (Analyze)

1

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

2 steps

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