Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. A : Automata(Alph;St)

  4. l : Alph List

Conclusion:

A(l) St

Applied Tactic: ListInd 4
Generated subgoals:

1. A([]) St

2. A(u::v) St