l:St*, s:St, eq:(St
St
), sx:St.
mem_f(St;sx;l \ s) 
if eq(s,sx)
False else mem_f(St;sx;l) fi
lremove_mem
nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi
(recursive)
Thm* l:St*, s:St, eq:(StSt), sx:St.
mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi
lremove_mem