1. T : Type
2. l : T List
3. x,y:T.
3. (f:(2||l||). increasing(f;2) & (j:2. [x; y][j] = l[(f(j))]))  x = y
4. i : 
5. j : 
6. i<||l||
7. j<||l||
8. i = j
9. i<j
10. j1 : 2
  [l[j]; l[i]][j1] = l[if j1=0 j else i fi]

1	11. j1 = 0   [l[j]; l[i]][j1] = l[j]	1 step
2	11. j1 = 0   [l[j]; l[i]][j1] = l[i]	1 step

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