proposition: Lemma for_all_b : Proper (E.eq==>Logic.eq) f -> for_all f s = forallb f (elements s).
proof: Proof. intros. generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s). unfold For_all. destruct (forallb f (elements s)); destruct (for_all f s); auto; intros. - rewrite <- H1; intros. destruct H0 as (H0,_). rewrite (H2 x0) in H3. rewrite (InA_alt E.eq x0 (elements s)) in H3. destruct H3 as (a,(Ha1,Ha2)). rewrite (H _ _ Ha1). apply H0; auto. - symmetry. rewrite H0; intros. destruct H1 as (_,H1). apply H1; auto. rewrite H2. rewrite InA_alt. exists x0; split; auto with relations. Qed.
imports: DecidableTypeEx MSetInterface