proposition: Lemma map_filter_filter Q `{!∀ x, Decision (Q x)} m : filter P (filter Q m) = filter (λ '(i, x), P (i, x) ∧ Q (i, x)) m.
proof: Proof. apply map_filter_strong_ext. intros ??. rewrite map_lookup_filter_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)