At: mem append 3
1. T: Type
2. L1: T*
3. L2: T*
4. t: T
5. u: T
6. v: T*
7. mem_f(T;t;v @ L2) 
mem_f(T;t;v) 
mem_f(T;t;L2)
8. mem_f(T;t;v @ L2) 
(mem_f(T;t;v) mem_f(T;t;L2))
9. mem_f(T;t;L2)
u = t mem_f(T;t;v @ L2)
By:
Sel 2 (Analyze 0)
THEN
BackThru 8
THEN
ProveProp
Generated subgoals:None
About:
