proposition: Lemma map_filter_subseteq_mono m1 m2 : m1 ⊆ m2 → filter P m1 ⊆ filter P m2.
proof: Proof. rewrite map_subseteq_spec. intros Hm1m2. apply map_filter_strong_subseteq_ext. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)