proposition: Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s.
proof: Proof. intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H). destruct (mem y s); destruct (mem y (remove x s)); intuition. Qed.
imports: DecidableTypeEx MSetInterface