proposition: Lemma update_same : forall A B (IA:Inhab B) (M:map A B) (x:A), x \indom M -> M[x:=M[x]] = M.
proof: Proof. Proof using. introv Dx. applys extensionality. { intros k. rewrite* dom_update_at_indom. } { intros k Hk. rewrite* dom_update_at_indom in Hk. rewrite read_update. case_if*. subst*. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)