proposition: Lemma elements_b : mem x s = existsb (eqb x) (elements s).
proof: Proof. generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)). rewrite InA_alt. destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros. - symmetry. rewrite H1. destruct H0 as (H0,_). destruct H0 as (a,(Ha1,Ha2)); [ intuition |]. exists a; intuition. unfold eqb; destruct (eq_dec x a); auto. - rewrite <- H. rewrite H0. destruct H1 as (H1,_). destruct H1 as (a,(Ha1,Ha2)); [intuition|]. exists a; intuition. unfold eqb in *; destruct (eq_dec x a); auto; discriminate. Qed.
imports: DecidableTypeEx MSetInterface