Thm* Alph:Type, L:LangOver(Alph), g:((x,y:Alph*//(x L-induced Equiv y))). A(g) Automata(Alph;x,y:Alph*//(x L-induced Equiv y))
About:
s,a. a.s),nil,g >
Alph:Type, L:LangOver(Alph), g:((x,y:Alph*//(x L-induced Equiv y))
).
A(g) 
Automata(Alph;x,y:Alph*//(x L-induced Equiv y))s,a. a.s),nil,g >
