1. T : Type
2. R : TTProp
3. k : 
4. 0<k
5. x,y:T.
5. (x R^k-1 y)
5. 
5. (L:T List. 
5. (||L|| = k-1+1 & L[0] = x & last(L) = y & (i:(k-1). L[i] R L[(i+1)]))
6. k = 0
7. x : T
8. y@0 : T
9. T List
10. u : T
11. v : T List
12. ||v||+1 = k+1
13. u = x
14. last([u / v]) = y@0
15. i:k. [u / v][i] R [u / v][(i+1)]
16. i : (k-1)
  v[i] R v[(i+1)]

By:	InstHyp [i+1] -2 THEN RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] -1

1

17. v[(i+1-1)] R v[(i+1+1-1)]   v[i] R v[(i+1)]

1 step

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