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
15. z R2 y
16. x R2 z
  (x R2 y)  x = y

None

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