proposition: Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) -> forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
proof: Proof. clear Comp f. intros. assert (compat_bool E.eq (fun x => orb (f x) (g x))). - unfold compat_bool, Proper, respectful; intros. rewrite (H x y H1); rewrite (H0 x y H1); auto. - unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto. assert (f a || g a = true <-> f a = true \/ g a = true). + split; auto with bool. intro H3; destruct (orb_prop _ _ H3); auto. + tauto. Qed.
imports: FSetProperties Zerob Sumbool DecidableTypeEx