1. T : Type
2. L : T List
3. TT
4. n : (||L||-1)
5. (n, n+1)  ||L||||L||
6. ||swap(L;n;n+1)|| = ||L||
7. f : ||L||||L||
8. i:||L||. f(i) = (n, n+1)(i)
9. ||L||
10. j : ||L||
  swap(L;n;n+1)[(f(j))] = L[j]

By:	RWO Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))] 0 THEN Subst' (f(j) = (n, n+1)(j)) 0 THEN EasyHyp

1

L[((n, n+1)((n, n+1)(j)))] = L[j]

3 steps

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