L:LangOver(Alph).
Fin(Alph) 
Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l)))
(
St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto))
mn_31
DA(l)
Thm* L:LangOver(Alph).
Fin(Alph)
Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l)))
(St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto))
mn_31
Thm* L:LangOver(Alph).
Fin(Alph)
(St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto))
(R:(Alph*
Alph*Prop).
(EquivRel x,y:Alph*. x R y) c
(g:((x,y:Alph*//R(x,y))
).
Fin(x,y:Alph*//R(x,y))
& (l:Alph*. L(l) 
g(l))
& (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))))
mn_12