Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(Alph)

  5. Fin(St)

  6. s : St

Conclusion:

Dec(w:Alph List. Auto(w) = s)

Applied Tactic: (InstLemma `reach_list` [Alph;St;Auto] ...a)
Generated subgoals:

1. Dec(w:Alph List. Auto(w) = s)