proposition: Lemma binds_update_same : forall A B i v (M:map A B), binds (M[i:=v]) i v.
proof: Proof. Proof using. intros. asserts IB: (Inhab B). constructor. exists* v. rewrite (@binds_eq_indom_read A B IB) in *. rewrite~ indom_update_eq. rewrite* read_update_same. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)