l:St*, eq:(St
St
).
(x,y:St. eq(x,y) 
x = y) (s:St. mem_f(St;s;l) 
mem_f(St;s;LShort(l)))
lshort_mem
Q == (P Q) & (P Q)
Thm* l:St*, eq:(StSt).
(x,y:St. eq(x,y) x = y) (s:St. mem_f(St;s;l) mem_f(St;s;LShort(l)))
lshort_mem
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
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
Thm* L1,L2:T*, t:T. mem_f(T;t;L1 @ L2) mem_f(T;t;L1) mem_f(T;t;L2)
mem_append
In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 finite sets