Level: Lib Thy Top: 1 3
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(St)

  5. Fin(Alph)

Conclusion:

Fin(<St, a:Alph. s:St. Auto s a>.car)

Applied Tactic: Unfold `aset_car` 0 THEN Reduce 0 THEN NthHyp (-2)
Generated subgoals:

None