l:St*, f:(St
St), s:St.
mem_f(St;s;(+f)(l))
mem_f(St;s;l) 
(
s':St. mem_f(St;s';l) & f(s') = s)
add_action_mem
nil ; h.l' [h; f(h)/ (+f)(l')] (recursive)
Thm* l:St*, f:(StSt), s:St.
mem_f(St;s;(+f)(l))
mem_f(St;s;l) (s':St. mem_f(St;s';l) & f(s') = s)
add_action_mem