proposition: Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m1 m2 : M A) : m1 ##ₘ m2 → filter P m1 ##ₘ filter P m2.
proof: Proof. rewrite !map_disjoint_spec. intros ? i x y. rewrite !map_lookup_filter_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)