proposition: Lemma updateList_correct1 : forall A (v: list A) f i d1 d2, i < length v -> nth i (updateList v f i) d1 = f (nth i v d2).
proof: Proof. induction v. intros. absurd (i < 0); auto with *. intros f [|i] d1 d2 H. reflexivity. simpl. apply IHv. auto with *. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos