proposition: Lemma update_middle : forall i l1 l2 v w, i = length l1 -> (l1 ++ w :: l2)[i := v] = l1 & v ++ l2.
proof: Proof. Proof using. introv E. rewrites~ (>> update_app_r 0 i). rewrite update_zero. rew_list~. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)