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

None

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