proposition: Lemma update_nth_same : forall n l, n < length l -> update n (nth n l) l = l.
proof: Proof. Proof using. introv E. gen n. induction l as [|x l']; intros. { rewrite length_nil in E. false. math. } { rewrite length_cons in E. rewrite update_cons_case. destruct n as [|n']; case_if. { subst. rewrite* nth_zero. } { fequals. rewrite nth_cons. math_rewrite (S n' - 1 = n')%nat. rewrite* IHl'. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)