Thms relation autom Sections AutomataTheory Doc

NOTE: Trans(A)(R(_1;_2)) is alpha-equivalent to Trans x,y:A. R(x;y).

trans Def basic Trans x,y:T. E(x;y) == a,b,c:T. E(a;b) E(b;c) E(a;c)

Thm* E:(TTProp). Trans x,y:T. E(x,y) Prop