proposition: Lemma map_filter_strong_subseteq_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. rewrite map_subseteq_spec. setoid_rewrite map_lookup_filter_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)