Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. si : S.car

  4. Fin(S.car)

  5. Fin(Alph)

Conclusion:

RL:S.car List. s:S.car. (w:Alph List. (S:wsi) = s) mem_f(S.car;s;RL)

Applied Tactic: (D (-1) THEN RWH (LemmaC `bij_iff_1_1_corr`) (-1) THENM D (-1) THENM D (-1) ...a)
Generated subgoals:

1. RL:S.car List. s:S.car. (w:Alph List. (S:wsi) = s) mem_f(S.car;s;RL)