1. T : Type
2. L1 : T List
3. i : ||L1||
4. j : ||L1||
5. ||swap(L1;i;j)|| = ||L1||
6. ||swap(swap(L1;i;j);i;j)|| = ||swap(L1;i;j)||
7. i1 : 
8. i1<||swap(swap(L1;i;j);i;j)||
  swap(swap(L1;i;j);i;j)[i1] = L1[i1]

By:	RWW Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))] 0 THEN RWO Thm* k:, x,y,i:k. (y, x)((y, x)(i)) = i 0

None

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