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

In prior sections: core int 1 bool 1 int 2 finite sets