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* L,La:T*. Fin(T) (La':T*. (t:T. mem_f(T;t;La) mem_f(T;t;L) mem_f(T;t;La')) & (t:T. mem_f(T;t;La') mem_f(T;t;La)) & (||La'||1 mem_f(T;hd(La');L))) shorten_list

Thm* L:T*, t:T. mem_f(T;t;L) (i:||L||. L[i] = t) mem_select

Thm* L1,L2:T*, t:T. mem_f(T;t;L1 @ L2) mem_f(T;t;L1) mem_f(T;t;L2) mem_append

Thm* L:T*, i:||L||. mem_f(T;L[i];L) select_mem

Thm* L:T*. ||L||1 mem_f(T;hd(L);L) hd_mem

Thm* s:S, l:S*. Fin(S) Dec(mem_f(S;s;l)) mem_f_dec

Thm* as:T*. as {x:T| mem_f(T;x;as) }* list_in_mem_f_list