proposition: Lemma update_middle : forall l1 l2 n x v, n = length l1 -> update n v (l1 ++ x :: l2) = l1 & v ++ l2.
proof: Proof. Proof using IA. intros. subst. rew_list. rewrites update_app_r. { math_rewrite (length l1 - length l1 = 0). rew_list~. } { math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)