R2)(x,y) == (x R1 y) (x R2 y)
T:Type, R1,R2:(T
TProp). (R1 R2) 
TTPropa,b:T. E(a;b) 
E(b;a)T:Type, E:(TTProp). (Sym x,y:T. E(x,y)) Prop| Some definitions of interest. | |
| rel_or | R2)(x,y) == (x R1 y) (x R2 y) |
| T:Type, R1,R2:(TTProp). (R1 R2) TTProp | |
| sym | a,b:T. E(a;b) E(b;a) |
| T:Type, E:(TTProp). (Sym x,y:T. E(x,y)) Prop |
About:
 |  |  |  |  |  |  |  |  |