proposition: Lemma dom_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X : (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom (filter P m) = X.
proof: Proof. unfold_leibniz. apply dom_filter. Qed.
imports: stdpp(options)