Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

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

  5. l : x,y:(Alph List)//(x Rl y)

Conclusion:

Auto(l)

Applied Tactic: D 5 THENA Auto
Generated subgoals:

1. Auto(l1) = Auto(l2)