Thms
automata
5
Sections
AutomataTheory
Doc
NOTE:
Trans(A)(R(_1;_2)) is
alpha-equivalent
to Trans x,y:A. R(x;y).
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:(T
T
Prop). Trans x,y:T. E(x,y)
Prop
About:
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) 
Propa,b,c:T. E(a;b) E(b;c) E(a;c)
