proposition: Lemma updateList_overflow : forall A (v : list A) f i, length v <= i -> updateList v f i = v.
proof: Proof. induction v. - reflexivity. - intros. simpl. destruct i. exfalso; inversion H. apply f_equal. rewrite IHv. reflexivity. apply le_S_n, H. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos