Thms
choice
1
Sections
AutomataTheory
Doc
sym
Def
Sym x,y:T. E(x;y) ==
a,b:T. E(a;b)
E(b;a)
Thm*
T:Type, E:(T
T
Prop). Sym x,y:T. E(x,y)
Prop
About:
a,b:T. E(a;b) 
E(b;a)
T:Type, E:(T
TProp). Sym x,y:T. E(x,y) 
Propa,b:T. E(a;b) E(b;a)
