Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. s : S.car

  4. Fin(Alph)

  5. Fin(S.car)

Conclusion:

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

Applied Tactic: (D 0 THENM ListInd (-1) ...a)
Generated subgoals:

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

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