R1,R2:(T
TProp). R1 => R2 
R1^* => R2^*n:
, T:Type, R1,R2:(TTProp). R1 => R2 R1^n => R2^n| Theorem | Name |
| R1,R2:(TTProp). R1 => R2 R1^* => R2^* | [rel_star_monotone] |
| cites the following: | |
| n:, T:Type, R1,R2:(TTProp). R1 => R2 R1^n => R2^n | [rel_exp_monotone] |