1. T : Type
2. R : TTProp
3. R2 : TTProp
4. Trans(T)(R2(_1,_2))
5. x,y:T. (x R y)  (x R2 y)
6. n : 
7. 0<n
8. x,y:T. (x R^n-1 y)  (x R2 y)  x = y
9. x : T
10. y : T
11. n = 0
12. z : T
13. x R z
14. z R^n-1 y
  (x R2 y)  x = y

By:	AllHyps (h.InstHyp [z;y] h THENA Complete Auto) THEN AllHyps (h.InstHyp [x;z] h THENA Complete Auto)

1

15. (z R2 y)  z = y 16. x R2 z   (x R2 y)  x = y

3 steps

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