proposition: Lemma dom_singleton_inv {A} (m : M A) i : dom m ≡ {[i]} → ∃ x, m = {[i := x]}.
proof: Proof. intros Hdom. assert (is_Some (m !! i)) as [x ?]. { apply (elem_of_dom (D:=D)); set_solver. } exists x. apply map_eq; intros j. destruct (decide (i = j)); simplify_map_eq; [done|]. apply not_elem_of_dom. set_solver. Qed.
imports: stdpp(options)