Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. l : Alph List

Conclusion:

Auto(l) A(l.Auto(l))(l)

Applied Tactic: RWH(AddrC [2;1](UnfoldC `accept_list` )) 0 THEN Reduce 0
Generated subgoals:

1. Auto(l) (F(Auto) Auto(A(l.F(Auto) Auto(l))(l)))