Level: Lib Thy Top: 1 4
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(St)

  5. Fin(Alph)

  6. RL:<St, a:Alph. s:St. Auto s a>.car List s:<St, a:Alph. s:St. Auto s a>.car (w:Alph List. (<St, a:Alph. s:St. Auto s a>:wI(Auto)) = s) mem_f(<St, a:Alph. s:St. Auto s a>.car;s;RL)

Conclusion:

RL:St List. s:St. (w:Alph List. Auto(w) = s) mem_f(St;s;RL)

Applied Tactic: Unfold `aset_car` (-1) THEN Reduce (-1)
Generated subgoals:

1. RL:St List. s:St. (w:Alph List. Auto(w) = s) mem_f(St;s;RL)