1. n : 
2. R : nnProp
3. x : n
4. y : n
5. n@0 : 
6. j:. j<n@0  (x R^j y)  (k:(n+1). x R^k y)
7. L : n List
8. ||L|| = n@0+1
9. L[0] = x
10. last(L) = y
11. i:n@0. L[i] R L[(i+1)]
12. n@0n
13. i : (n@0+1)
14. j : (n@0+1)
15. i<j
16. L[i] = L[j]
  ||firstn(i+1;L) @ nth_tl(j+1;L)|| = n@0-(j-i)+1  
  & (firstn(i+1;L) @ nth_tl(j+1;L))[0] = x
  & & last(firstn(i+1;L) @ nth_tl(j+1;L)) = y
  & & (i@0:(n@0-(j-i)). 
  & & ((firstn(i+1;L) @ nth_tl(j+1;L))[i@0] 
  & & (R (firstn(i+1;L) @ nth_tl(j+1;L))[(i@0+1)])

1	||firstn(i+1;L) @ nth_tl(j+1;L)|| = n@0-(j-i)+1	1 step
2	17. ||firstn(i+1;L) @ nth_tl(j+1;L)|| = n@0-(j-i)+1     ||firstn(i+1;L) @ nth_tl(j+1;L)|| = n@0-(j-i)+1     & (firstn(i+1;L) @ nth_tl(j+1;L))[0] = x   & & last(firstn(i+1;L) @ nth_tl(j+1;L)) = y   & & (i@0:(n@0-(j-i)).    & & ((firstn(i+1;L) @ nth_tl(j+1;L))[i@0]    & & (R (firstn(i+1;L) @ nth_tl(j+1;L))[(i@0+1)])	18 steps

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