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:
 |  |  |  |  |  |  |