proposition: Lemma union_spec : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (union s s') <-> In x s \/ In x s'.
proof: Proof. induction s; simpl in *; unfold flip; intros; auto; inv. - intuition; inv. - rewrite IHs, add_spec, InA_cons; intuition. Qed.
imports: MSetInterface