proposition: Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> In x s.
proof: Proof. induction s; intros. - split; intros; inv. discriminate. - simpl; destruct (X.eq_dec x a); split; intros; inv; auto. + right; rewrite <- IHs; auto. + rewrite IHs; auto. Qed.
imports: MSetInterface