Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. A : Automata(Alph;St)

  4. l : Alph List

Conclusion:

A([]) St

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

1. I(A) St

2. A A([]) "?" St