Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. s : S.car

  4. Fin(Alph)

  5. Fin(S.car)

Conclusion:

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

Applied Tactic: Assert 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))
Generated subgoals:

1. 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))

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