Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St). L(Auto) = L(MinAuto(Auto))
Applied Tactic: Unfold `auto_lang` 0 THEN Unfold `lang_eq` 0 THEN Unfold `min_auto` 0 THEN UnivCD THENA Auto THEN Re
duce 0
Generated subgoals:1. 
Auto(l)
A(
l.Auto(l))(l)