a,b:T. E(a;b) 
E(b;a)T:Type, E:(T
TProp). Sym x,y:T. E(x,y) 
Prop| Who Cites sym? | |
| sym | Def Sym x,y:T. E(x;y) == a,b:T. E(a;b) E(b;a) |
| Thm* T:Type, E:(TTProp). Sym x,y:T. E(x,y) Prop |
| Syntax: | Sym x,y:T. E(x;y) | has structure: | sym(T; x,y.E(x;y)) |
About:
 |  |  |  |  |  |  |