proposition: Lemma dom_update_at_indom : forall A i `{IB:Inhab B} v (M:map A B), i \indom M -> dom (M[i:=v]) = dom M.
proof: Proof. Proof using. introv IB H. rewrite dom_update. set_prove_setup true. tests*: (x = i). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)