Level: Lib Thy Top: 1 2
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. s : S.car

  4. Fin(Alph)

  5. Fin(S.car)

  6. LL:(S.car S.car List) List BL:S.car List. t:S.car. mem_f(S.car;t;BL) (i:||LL||. LL[i].1 = t mem_f(S.car;s;LL[i].2))

Conclusion:

BL:S.car List. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act a t = s)

Applied Tactic: D (-3) THEN D (-3) THEN D (-2) THEN D (-2)
Generated subgoals:

1. BL:S.car List. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act a t = s)