proposition: Lemma map_filter_union {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m1 m2 : M A) : m1 ##ₘ m2 → filter P (m1 ∪ m2) = filter P m1 ∪ filter P m2.
proof: Proof. intros. apply map_eq; intros i. apply option_eq; intros x. rewrite lookup_union_Some, !map_lookup_filter_Some, lookup_union_Some by auto using map_disjoint_filter. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)