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