2. 0<n
3.
T:Type, R1,R2:(T
TProp). R1 => R2 
R1^n-1 => R2^n-1
T:Type, R1,R2:(TTProp). R1 => R2 R1^n => R2^n
T:Type, R1,R2:(TTProp). R1 => R2 R1^n-1 => R2^n-1
T:Type, R1,R2:(TTProp). R1 => R2 R1^n => R2^n| By: |
THEN All (Unfold `rel_implies`) THEN All Reduce |
| 1 |
T:Type, R1,R2:(TTProp).
3. ( x,y:T. (x R1 y) (x R2 y)) (x,y:T. (x R1^n-1 y) (x R2^n-1 y))
4. T : Type 5. R1 : T TProp
6. R2 : T TProp
7. x,y:T. (x R1 y) (x R2 y)
8.  n = 0
9. x : T 10. y : T 11.  z:T. (x R1 z) & (z R1^n-1 y)
z:T. (x R2 z) & (z R2^n-1 y) | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |  |