1. T : Type
2. R : TTProp
3. m : 
4. 0<m
5. n:, x,y,z:T. (x R^m-1 y)  (y R^n z)  (x R^m-1+n z)
6. n : 
7. x : T
8. y : T
9. z : T
10. y R^n z
11. m=0
12. m+n=0
13. z:T. (x R z) & (z R^m-1 y)
  z@0:T. (x R z@0) & (z@0 R^m+n-1 z)

1

13. z1 : T 14. z1 R^m-1 y   z1 R^m+n-1 z

2 steps

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