proposition: Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
proof: Proof. unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx