At: lremove mem 2 2 2 2
1. St: Type
2. l: St*
3. s: St
4. eq: St
St
5. sx: St
6. u: St
7. v: St*
8. 
eq(s,sx)
9. mem_f(St;sx;v \ s) 
mem_f(St;sx;v)
10. eq(s,u)
mem_f(St;sx;u.(v \ s)) (u = sx 
mem_f(St;sx;v))
By:
Analyze 0
THEN
RecUnfold `mem_f` 0
THEN
Reduce 0
THEN
ProveProp
Generated subgoals:None
About:
