proposition: Lemma filter_dom_L {A} `{!Elements K D, !FinSet K D} (P : K → Prop) `{!∀ x, Decision (P x)} (m : M A) : filter P (dom m) = dom (filter (λ kv, P kv.1) m).
proof: Proof. unfold_leibniz. apply filter_dom. Qed.
imports: stdpp(options)