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