proposition: Lemma exists_b : Proper (E.eq==>Logic.eq) f -> exists_ f s = existsb f (elements s).
proof: Proof. intros. generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s). unfold Exists. destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros. - rewrite <- H1; intros. destruct H0 as (H0,_). destruct H0 as (a,(Ha1,Ha2)); auto. exists a; split; auto. rewrite H2; rewrite InA_alt; exists a; auto with relations. - symmetry. rewrite H0. destruct H1 as (_,H1). destruct H1 as (a,(Ha1,Ha2)); auto. rewrite (H2 a) in Ha1. rewrite (InA_alt E.eq a (elements s)) in Ha1. destruct Ha1 as (b,(Hb1,Hb2)). exists b; auto. rewrite <- (H _ _ Hb1); auto. Qed.
imports: DecidableTypeEx MSetInterface