Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. l : Alph List

  5. EquivRel(Alph List;x,y.x Rl y)

Conclusion:

MinAuto(Auto)(l) = l

Applied Tactic: Unfold `min_auto` 0
Generated subgoals:

1. A(l.Auto(l))(l) = l