proposition: Lemma map_filter_subseteq_ext (m : M A) : filter P m ⊆ filter Q m ↔ (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)).
proof: Proof. rewrite map_filter_strong_subseteq_ext. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)