Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

St:. l:St List. f:St St. s:St. mem_f(St;s;(+f)(l)) mem_f(St;s;l) (s':St. mem_f(St;s';l) f s' = s)

Applied Tactic: (GenExRepD ...a)
Generated subgoals:

1. mem_f(St;s;l) (s':St. mem_f(St;s';l) f s' = s)

2. mem_f(St;s;(+f)(l))

3. mem_f(St;s;(+f)(l))