proposition: Lemma map_filter_filter_r Q `{!∀ x, Decision (Q x)} m : (∀ i x, m !! i = Some x → Q (i, x) → P (i, x)) → filter P (filter Q m) = filter Q m.
proof: Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)