proposition: Lemma map_filter_and {A} (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} (m : M A) : filter (λ x, P x ∧ Q x) m = filter P m ∩ filter Q m.
proof: Proof. apply map_eq. intros k. rewrite lookup_intersection. rewrite !map_lookup_filter. destruct (m !! k); simpl; repeat case_guard; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)