Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. si : S.car

  4. Fin(S.car)

  5. n :

  6. f : n Alph

  7. g : Alph n

  8. InvFuns(n;Alph;f;g)

Conclusion:

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

Applied Tactic: Assert Fin(S.car) THENA NthHyp 4
Generated subgoals:

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