1. n : 
2. R : nnProp
3. x : n
4. y : n
5. n@0 : 
6. x R^n@0 y
  k:(n+1). x R^k y

By:	RepeatFor 2 (MoveToConcl -1) THEN BackThru Thm* P:(Prop). (i:. (j:. j<i  P(j))  P(i))  (i:. P(i))

1

6. j:. j<n@0  (x R^j y)  (k:(n+1). x R^k y) 7. x R^n@0 y   k:(n+1). x R^k y

37 steps

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