At: mem append 1
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;v @ L2)
u = t mem_f(T;t;v) mem_f(T;t;L2)
By:
FwdThru 7 [-1]
THEN
ProveProp
Generated subgoals:None
About:
