proposition: Lemma union_b : mem x (union s s') = mem x s || mem x s'.
proof: Proof. generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition. Qed.
imports: DecidableTypeEx MSetInterface