proposition: Lemma union_filter: forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
proof: Proof. clear Comp' Comp f. intros. assert (Proper (E.eq==>Logic.eq) (fun x => orb (f x) (g x))). - repeat red; 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: MSetProperties Zerob Sumbool Lia DecidableTypeEx