Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. L1,L2:T List. t:T. mem_f(T;t;L1 @ L2) mem_f(T;t;L1) mem_f(T;t;L2)

Applied Tactic: (RepD THENM ListInd 2 THENM Reduce 0 THENM GenExRepD THENM Try ProveProp ...)
Generated subgoals:

1. (u = t mem_f(T;t;v)) mem_f(T;t;L2)

2. u = t mem_f(T;t;v @ L2)

3. u = t mem_f(T;t;v @ L2)