proposition: Lemma dom_insert_lookup {A} (m : M A) i x : is_Some (m !! i) → dom (<[i:=x]>m) ≡ dom m.
proof: Proof. intros Hindom. assert (i ∈ dom m) by by apply elem_of_dom. rewrite dom_insert. set_solver. Qed.
imports: stdpp(options)