proposition: Lemma add_b : mem y (add x s) = eqb x y || mem y s.
proof: Proof. generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb. destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition. Qed.
imports: DecidableTypeEx MSetInterface