1. T : Type
2. R : TTProp
3. a : T
4. b : T
5. c : T
6. n1 : 
7. a R^n1 b
8. n : 
9. b R^n c
  a R^n1+n c

By:	Using [`y',b] (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