proposition: Lemma remove_spec : forall (s : t) (x y : elt) {Hs : Ok s}, In y (remove x s) <-> In y s /\ ~X.eq y x.
proof: Proof. induction s; simpl; intros. - intuition; inv; auto. - destruct X.eq_dec as [|Hnot]; inv; rewrite !InA_cons, ?IHs; intuition. + elim H. setoid_replace a with y; eauto. + elim H3. setoid_replace x with y; eauto. + elim Hnot. eauto. Qed.
imports: MSetInterface