Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(Alph) Fin(St)

Conclusion:

Con(MinAuto(Auto))

Applied Tactic: InstLemma `lang_rel_equi` [Alph;L(Auto)] THENA Auto
Generated subgoals:

1. Con(MinAuto(Auto))