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]
17. ||firstn(i+1;L) @ nth_tl(j+1;L)|| = n@0-(j-i)+1
18. i@0 : (n@0-(j-i))
19. ||firstn(i+1;L)|| = i+1
20. ||nth_tl(j+1;L)|| = ||L||-(j+1)
  (firstn(i+1;L) @ nth_tl(j+1;L))[i@0] 
  R (firstn(i+1;L) @ nth_tl(j+1;L))[(i@0+1)]

By:	(RWO "select_append" 0 THEN Repeat SplitOnConclITE (THEN (Try (RWO Thm* as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i] 0)) THEN (Try ((RWO ((Thm* as:T List, n:{0...||as||}, i:(||as||-n). nth_tl(n;as)[i] = as[(i+n)] ((0))

1	21. i@0<||firstn(i+1;L)|| 22. i@0+1<||firstn(i+1;L)||   L[i@0] R L[(i@0+1)]	1 step
2	21. i@0<||firstn(i+1;L)|| 22. ||firstn(i+1;L)||i@0+1   L[i@0] R L[(i@0+1-||firstn(i+1;L)||+j+1)]	3 steps
3	21. ||firstn(i+1;L)||i@0 22. ||firstn(i+1;L)||i@0+1   L[(i@0-||firstn(i+1;L)||+j+1)] R L[(i@0+1-||firstn(i+1;L)||+j+1)]	1 step

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