Def (rec) mem_f(T;a;bs) == Case of bs : null False ; b.bs' b = a T mem_f(T;a;bs')

Thm* a:T, bs:T*. mem_f(T;a;bs) Prop