proposition: Lemma filter_dom {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. intros i. rewrite elem_of_filter, !elem_of_dom. unfold is_Some. setoid_rewrite map_lookup_filter_Some. naive_solver. Qed.
imports: stdpp(options)