1. T : Type
2. L : T List
3. x : T
4. i : {1..(||L||+1)}
5. j : {1..(||L||+1)}
6. i1 : 
7. i1<||swap([x / L];i;j)||
8. i1 = 0
  swap([x / L];i;j)[i1] = swap(L;i-1;j-1)[(i1-1)]

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

1

7. i1<||[x / L]|| 8. i1 = 0   [x / L][((i, j)(i1))] = L[((i-1, j-1)(i1-1))]

5 steps

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