Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. S:ActionSet(Alph). si:S.car.
Fin(S.car)
Fin(Alph)
(
RL:S.car List. s:S.car. (w:Alph List. (S:w
si) = s) 
mem_f(S.car;s;RL))
Applied Tactic: (RepD ...a)
Generated subgoals:1. RL:S.car List. s:S.car. (w:Alph List. (S:wsi) = s) mem_f(S.car;s;RL)