At: quo list accept 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. LangOf(Auto)(l1) 
LangOf(Auto)(l2)
Auto(l1)
= Auto(l2)
By:
Unfold `auto_lang` 7
THEN
Reduce 7
THEN
BackThru
Thm* 
a,b:
. (a b) 
a = b
Generated subgoals:None
About:
