1. T : Type
2. R : TTProp
3. x : T
4. y : T
5. z : T
6. n1 : 
7. x R^n1 y
8. n : 
9. y R^n z
  x R^n1+n z

By:	Using [`y',y] (BackThru (Thm* R:(TTProp), m,n:, x,y,z:T. (x R^m y)  (y R^n z)  (x R^m+n z))

None

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