Level: Lib Thy Top: 1 2
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. sL : S.car List

  4. Fin(Alph)

  5. Fin(S.car)

  6. n: TBL:S.car List (s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (||TBL|| = n (i:||TBL||. j:i. (TBL[i] = TBL[j])) (s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (AL:S.car List (s:S.car. mem_f(S.car;s;AL) (w:Alph List. mem_f(S.car;(S:ws);sL))) (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) (s:S.car. a:Alph. mem_f(S.car;S.act a s;TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL))))

Conclusion:

TBL:S.car List. s:S.car. mem_f(S.car;s;TBL) (w:Alph List. mem_f(S.car;(S:ws);sL))

Applied Tactic: (D (-2) THEN RWH (LemmaC `bij_iff_1_1_corr`) (-2) THENM D (-2) THENM D (-2) ...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))