proposition: Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s').
proof: Proof. generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition. Qed.
imports: DecidableTypeEx MSetInterface