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
n:
, f:(n
s). Bij(n; s; f)
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* s:S, l:S*. Fin(S) Dec(mem_f(S;s;l)) mem_f_dec
In prior sections: finite sets