proposition: Lemma update_update : forall A i `{Inhab B} v v' (M:map A B), M[i:=v][i:=v'] = M[i:=v'].
proof: Proof. Proof using. intros. applys fun_ext_1. intros k. do 3 rewrite update_impl_eq. case_if*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)