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. increasing(f;||[x; y]||)
8. j:||[x; y]||. [x; y][j] = l[(f(j))]
9. x = l[(f(0))]
10. y = l[(f(1))]
11. l[(f(0))] = l[(f(1))]
  x = y

None

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