At: min auto comp 1 1 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. l: Alph*
5. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
(
l.Auto(l)
) 
(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
By: Analyze
THENL
[BackThru
Thm* 
Auto:Automata(Alph;St), l:x,y:Alph*//(x LangOf(Auto)-induced Equiv y).
Auto(l)
;Id]
Generated subgoals:None
About:
