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