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
  x,y@0:T.
  (z:T. (x R z) & (z R^k-1 y@0))
  
  (L:T List. 
  (||L|| = k+1   & L[0] = x & last(L) = y@0 & (i:k. L[i] R L[(i+1)]))

1	7. x : T 8. y@0 : T 9. z : T 10. x R z 11. z R^k-1 y@0   L:T List.    ||L|| = k+1   & L[0] = x & last(L) = y@0 & (i:k. L[i] R L[(i+1)])	8 steps
2	7. x : T 8. y@0 : T 9. L : T List 10. ||L|| = k+1   11. L[0] = x 12. last(L) = y@0 13. i:k. L[i] R L[(i+1)]   z:T. (x R z) & (z R^k-1 y@0)	12 steps
3	7. T 8. T 9. L : T List 10. ||L|| = k+1     null(L)	1 step

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