Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. x : Alph List

  5. y : Alph List

  6. z : Alph List

  7. Auto(x) = Auto(y)

Conclusion:

Auto(z @ x) = Auto(z @ y)

Applied Tactic: ListInd 6
Generated subgoals:

1. Auto([] @ x) = Auto([] @ y)

2. Auto((u::v) @ x) = Auto((u::v) @ y)