proposition: Lemma update_app_l : forall l1 i l2 v, 0 <= i < length l1 -> (l1 ++ l2)[i:=v] = (l1[i:=v]) ++ l2.
proof: Proof. Proof using. introv N. asserts IA: (Inhab A). typeclass. unfold LibContainer.update, update_inst, update_impl. rewrite length_eq in N. case_if~. rewrite~ update_app_l. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)