proposition: Lemma add_spec : forall (s : t) (x y : elt) {Hs : Ok s}, In y (add x s) <-> X.eq y x \/ In y s.
proof: Proof. induction s; simpl; intros. - intuition; inv; auto. - destruct X.eq_dec; inv; rewrite InA_cons, ?IHs; intuition. + left; eauto. + inv; auto. Qed.
imports: MSetInterface