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
  increasing(x.if x=0 j else i fi;2)

1

10. i@0 : 1   if i@0=0 j else i fi<if i@0+1=0 j else i fi

1 step

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