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
A == A False
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
In prior sections: core bool 1 int 2 list 1 finite sets