proposition: Lemma nth_update_same : forall n l v, n < length l -> nth n (update n v l) = v.
proof: Proof. Proof using. intros n l. gen n. induction l; introv N; rew_list in N. { false. math. } { destruct n as [|n']. { rewrite update_zero. rew_listx~. } { rewrite update_cons. rew_listx. applys* IHl. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)