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||). 
6. increasing(f;||[x; y]||) & (j:||[x; y]||. [x; y][j] = l[(f(j))])
  x = y

1

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))]   x = y

5 steps

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