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