proposition: Lemma updateList_length : forall A (v:list A) f i, length (updateList v f i) = length v.
proof: Proof. induction v. - reflexivity. - intros. simpl. destruct i. reflexivity. simpl. rewrite IHv. reflexivity. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos