R:(T
TProp). Trans x,y:T. x R^+ yR:(TTProp), m,n:
, x,y,z:T. (x R^m y) 
(y R^n z) (x R^m+n z)| Theorem | Name |
| R:(TTProp). Trans x,y:T. x R^+ y | [rel_plus_trans] |
| cites the following: | |
| R:(TTProp), m,n:, x,y,z:T. (x R^m y) (y R^n z) (x R^m+n z) | [rel_exp_add] |