proposition: Lemma singleton_b : mem y (singleton x) = eqb x y.
proof: Proof. generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb. destruct (eq_dec x y); destruct (mem y (singleton x)); intuition. Qed.
imports: DecidableTypeEx MSetInterface