Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St).
Fin(St) 
Fin(Alph) 
(
RL:St List. s:St. (w:Alph List. Auto(w) = s) 
mem_f(St;s;RL))
Applied Tactic: (RepD ...a)
Generated subgoals:1. RL:St List. s:St. (w:Alph List. Auto(w) = s) mem_f(St;s;RL)