x,y:T. (x R1 y) 
(x R2 y)T:Type, R1,R2:(T
TProp). R1 = > R2 
Prop| Who Cites rel implies? | |
| rel_implies | Def R1 = > R2 == x,y:T. (x R1 y) (x R2 y) |
| Thm* T:Type, R1,R2:(TTProp). R1 = > R2 Prop |
| Syntax: | R1 = > R2 | has structure: | rel_implies(T; R1; R2) |
About:
 |  |  |  |  |  |  |