proposition: Lemma map_filter_or {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_union. rewrite !map_lookup_filter. destruct (m !! k); simpl; repeat case_guard; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)