proposition: Lemma map_filter_comm {A} (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} (m : M A) : filter P (filter Q m) = filter Q (filter P m).
proof: Proof. rewrite !map_filter_filter. apply map_filter_ext. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)