L:T*, t:T. mem_f(T;t;L) 
(
i:
||L||. L[i] = t) mem_select
} == {k:
| i 
k < j }
Thm* L:T*, t:T. mem_f(T;t;L) (i:||L||. L[i] = t) mem_select
Thm* L:T*, i:||L||. mem_f(T;L[i];L) select_mem
In prior sections: int 1 bool 1 int 2 list 1 finite sets