R:(T
TProp), n:
, x,y:T. (x R^n^-1 y) 
(x R^-1^n y)R:(TTProp), m,n:, x,y,z:T. (x R^m y) 
(y R^n z) (x R^m+n z)| Theorem | Name |
| R:(TTProp), n:, x,y:T. (x R^n^-1 y) (x R^-1^n y) | [rel_inverse_exp] |
| 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] |