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