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
nil ; h.l' h.(LShort(l') \ h) (recursive)
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