proposition: Lemma map_filter_strong_ext_1 (m1 m2 : M A) : (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) → filter P m1 = filter Q m2.
proof: Proof. by rewrite map_filter_strong_ext. Qed.
imports: Coq(Permutation) stdpp(options)