proposition: Lemma map_img_filter (P : K * A → Prop) `{!∀ ix, Decision (P ix)} m X : (∀ x, x ∈ X ↔ ∃ i, m !! i = Some x ∧ P (i, x)) → map_img (filter P m) ≡ X.
proof: Proof. intros HX x. rewrite elem_of_map_img, HX. unfold is_Some. by setoid_rewrite map_lookup_filter_Some. Qed.
imports: Coq(Permutation) stdpp(options)