a,b,c:T. E(a;b) 
E(b;c) E(a;c)T:Type, E:(T
TProp). (Trans x,y:T. E(x,y)) 
Prop| NOTE: | Trans(A)(R(_1;_2)) is | alpha-equivalent | to Trans x,y:A. R(x;y). |
| Who Cites trans? | |
| trans | Def Trans x,y:T. E(x;y) == 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 |
| Syntax: | Trans x,y:T. E(x;y) | has structure: | trans(T; x,y.E(x;y)) |
About:
 |  |  |  |  |  |  |