At: min auto wf 1 1 1 1 1 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
5. l1: Alph*
6. l2: Alph*
7. Auto(l1)
Auto(l2)
Auto(l1) = Auto(l2)
By: BackThru
Thm* 
a,b:
. (a b) 
a = b
Generated subgoals:None
About:
