proposition: Lemma exists_mem_4: forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
proof: Proof. intros. rewrite for_all_exists in H; auto. rewrite negb_true_iff in H. destruct (for_all_mem_4 (fun x =>negb (f x)) (Comp' f Comp) s) as (x,p); auto. elim p;intros. exists x;split;auto. rewrite <-negb_false_iff; auto. Qed.
imports: FSetProperties Zerob Sumbool DecidableTypeEx