Level: Lib Thy Top: 1 2
Hypotheses:

  1. Alph :

  2. St :

  3. A : Automata(Alph;St)

  4. l : Alph List

  5. u : Alph

  6. v : Alph List

  7. A(v) St

Conclusion:

A(u::v) St

Applied Tactic: RecCaseSplit `compute_list` THEN Auto
Generated subgoals:

None