a,b:T. E(a;b) 
E(b;a)
Thm* T:Type, E:(T
TProp). Sym x,y:T. E(x,y) 
Prop
a,b,c:T. E(a;b) E(b;c) E(a;c)
Thm* T:Type, E:(TTProp). Trans x,y:T. E(x,y) Prop
| sym |
Def Sym x,y:T. E(x;y) == a,b:T. E(a;b) E(b;a)
Thm* |
| trans |
Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b) E(b;c) E(a;c)
Thm* |
About:
 |  |  |  |  |  |  |