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
"?" ; h.t h
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*. ||L||1 mem_f(T;hd(L);L) hd_mem
Thm* L:T*. 0 < ||L|| L = hd(L).tl(L) hd_tl