+let rec change_vec (A:Type[0]) (n:nat) on n ≝
+match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with
+[ O ⇒ λv,a,i.v
+| S m ⇒ λv,a,i.
+ match i with
+ [ O ⇒ vec_cons A a m (vec_tail … v)
+ | S j ⇒ vec_cons A (vec_hd A m v) m (change_vec A m (vec_tail … v) a j)
+ ]
+].
+
+lemma nth_change_vec : ∀A,i,n,v,a,d. i < n →
+ nth i ? (change_vec A n v a i) d = a.
+#A #i elim i
+ [#n #v #a #d #ltOn lapply v -v @(lt_O_n_elim n ltOn ??) //
+ |#m #Hind #n #v #a #d #Hlt
+ lapply Hlt lapply v @(lt_O_n_elim … (ltn_to_ltO … Hlt))
+ #p #v #ltmp @Hind @le_S_S_to_le //
+ ]
+qed.
+
+lemma nth_change_vec_neq : ∀A,j,i,n,v,a,d. i ≠ j →
+ nth j ? (change_vec A n v a i) d = nth j ? v d.
+#A #j elim j
+ [#i * // #n #v #a #d cases i
+ [#H @False_ind @(absurd ?? H) //
+ |#i0 #_ >(vec_expand ?? v) in ⊢ (???%); //
+ ]
+ |#m #Hind #i * // cases i // #i0 #n #v #a #d #neqim
+ whd in ⊢(??%?); whd in match (tail ??); >Hind
+ [>(vec_expand ??v) in ⊢ (???%); // |@(not_to_not … neqim) // ]
+ ]
+qed.
+
+lemma change_vec_same : ∀sig,n,v,i,d.
+ change_vec sig n v (nth i ? v d) i = v.
+#sig #n #v #i #d @(eq_vec … d)
+#i0 #Hi0 cases (decidable_eq_nat i i0) #Hi0
+[ >Hi0 >nth_change_vec //
+| >nth_change_vec_neq //
+]
+qed.
+
+lemma change_vec_cons_tail :∀A,n,vA,a,b,i.
+ change_vec A (S n) (vec_cons ? a n vA) b (S i) =
+ vec_cons ? a n (change_vec A n vA b i).
+#A #n #vA cases vA //
+qed.
+
+lemma change_vec_commute : ∀A,n,v,a,b,i,j. i ≠ j →
+ change_vec A n (change_vec A n v a i) b j
+ = change_vec A n (change_vec A n v b j) a i.
+#A #n #v #a #b #i #j #Hij @(eq_vec … a)
+#k #Hk cases (decidable_eq_nat k i) #Hki
+[ >Hki >nth_change_vec // >(nth_change_vec_neq ??????? (sym_not_eq … Hij))
+ >nth_change_vec //
+| cases (decidable_eq_nat k j) #Hkj
+ [ >Hkj >nth_change_vec // >(nth_change_vec_neq ??????? Hij) >nth_change_vec //
+ | >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
+ >(nth_change_vec_neq ??????? (sym_not_eq … Hkj))
+ >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
+ >(nth_change_vec_neq ??????? (sym_not_eq … Hkj)) //
+ ]
+]
+qed.
+
+lemma change_vec_change_vec : ∀A,n,v,a,b,i.
+ change_vec A n (change_vec A n v a i) b i = change_vec A n v b i.
+#A #n #v #a #b #i @(eq_vec … a) #i0 #Hi0
+cases (decidable_eq_nat i i0) #Hii0
+[ >Hii0 >nth_change_vec // >nth_change_vec //
+| >nth_change_vec_neq // >nth_change_vec_neq //
+ >nth_change_vec_neq // ]
+qed.
+
+
+(*
+lemma length_make_listi: ∀A,a,n,i.
+ |make_listi A a n i| = n.
+#A #a #n elim n // #m #Hind normalize //
+qed.
+definition change_vec ≝ λA,n,v,a,i.
+ make_veci A (λj.if (eqb i j) then a else (nth j A v a)) n 0.
+