proposition: Lemma dom_imap {A B} (f : K → A → option B) (m : M A) (X : D) : (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) → dom (map_imap f m) ≡ X.
proof: Proof. intros HX k. rewrite elem_of_dom, HX, map_lookup_imap. unfold is_Some. setoid_rewrite bind_Some. naive_solver. Qed.
imports: stdpp(options)