l:St*, eq:(St
St
).
(x,y:St. eq(x,y) 
x = y) (s:St. mem_f(St;s;l) 
mem_f(St;s;LShort(l)))
lshort_mem
b == if b
True else False fi
Thm* l:St*, eq:(StSt).
(x,y:St. eq(x,y) x = y) (s:St. mem_f(St;s;l) mem_f(St;s;LShort(l)))
lshort_mem
In prior sections: bool 1 list 1 finite sets