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

None

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