proposition: Lemma map_filter_strong_ext (m1 m2 : M A) : filter P m1 = filter Q m2 ↔ (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)).
proof: Proof. intros. rewrite map_eq_iff. setoid_rewrite option_eq. setoid_rewrite map_lookup_filter_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)