proposition: Lemma update_app_r : forall l2 j l1 i ij v, i = length l1 -> 0 <= j -> ij = i + j -> (l1 ++ l2)[ij:=v] = l1 ++ (l2[j:=v]).
proof: Proof. Proof using. intros. asserts IA: (Inhab A). typeclass. subst ij. unfold LibContainer.update, update_inst, update_impl. do 2 (case_if; [ math | ]). rewrite Zabs2Nat.inj_add; try math. subst i. rewrite length_eq. rewrite abs_nat. rewrite~ update_app_r. fequals_rec. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)