PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: min auto wf 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y

A(l.Auto(l)) Automata(Alph;x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
By: BackThru 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)) THENL [Auto;Auto;Analyze]
Generated subgoal:

15. l: x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
Auto(l)

About:
memberquotientlistlambdauniversebool