+let rec resize A (l:list A) i d on i ≝
+ match i with
+ [ O ⇒ [ ]
+ | S j ⇒ (hd ? l d)::resize A (tail ? l) j d
+ ].
+
+lemma length_resize : ∀A,l,i,d. |resize A l i d| = i.
+#A #l #i lapply l -l elim i
+ [#l #d %
+ |#m #Hind #l cases l
+ [#d normalize @eq_f @Hind
+ |#a #tl #d normalize @eq_f @Hind
+ ]
+ ]
+qed.
+
+lemma resize_id : ∀A,n,l,d. |l| = n →
+ resize A l n d = l.
+#A #n elim n
+ [#l #d #H >(lenght_to_nil … H) //
+ |#m #Hind * #d normalize
+ [#H destruct |#a #tl #H @eq_f @Hind @injective_S // ]
+ ]
+qed.
+
+definition resize_vec :∀A,n.Vector A n → ∀i.A→Vector A i.
+#A #n #a #i #d @(mk_Vector A i (resize A a i d) ) @length_resize
+qed.
+
+axiom nth_resize_vec :∀A,n.∀v:Vector A n.∀d,i,j. i < j →i < n →
+ nth i ? (resize_vec A n v j d) d = nth i ? v d.
+
+lemma resize_vec_id : ∀A,n.∀v:Vector A n.∀d.
+ resize_vec A n v n d = v.
+#A #n #v #d @(eq_vec … d) #i #ltin @nth_resize_vec //
+qed.
+
+definition vec_single: ∀A,a. Vector A 1 ≝ λA,a.
+ mk_Vector A 1 [a] (refl ??).
+
+definition vec_cons_right : ∀A.∀a:A.∀n. Vector A n → Vector A (S n).
+#A #a #n #v >(plus_n_O n) >plus_n_Sm @(vec_append … v (vec_single A a))
+>length_append >(len A n v) //
+qed.
+
+lemma eq_cons_right : ∀A,a1,a2.∀n.∀v1,v2:Vector A n.
+ a1 = a2 → v1 = v2 → vec_cons_right A a1 n v1 = vec_cons_right A a2 n v2.
+// qed.
+
+axiom nth_cons_right_n: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
+ nth n ? (vec_cons_right A a n v) d = a.
+
+axiom nth_cons_right_lt: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.∀i. i < n →
+ nth i ? (vec_cons_right A a n v) d = nth i ? v d.
+(*
+#A #a #n elim n
+ [#v #d >(vector_nil … v) //
+ |#m #Hind #v #d >(vec_expand … v) whd in ⊢ (??%?);
+ whd in match (vec_cons_right ????);
+*)
+
+axiom resize_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
+ resize_vec ? (S n) (vec_cons_right A a n v) n d = v.