proposition: Lemma filter_union : forall A B (IB:Inhab B) (f:A->B->Prop) M1 M2, disjoint M1 M2 -> filter f (M1 \u M2) = (filter f M1) \u (filter f M2).
proof: Proof. Proof using. introv IB D. extens. intros x. unfold disjoint, disjoint_inst, disjoint_impl, dom, dom_inst, dom_impl in D. rew_set in D. specializes D x. rew_set in D. unfold union, union_inst, union_impl, filter. cases (M2 x); cases (M1 x); try solve [ auto | case_if* ]. false* D. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)