+
+lemma nth_default : ∀A,i,n.∀v:Vector A n.∀d1,d2. i < n →
+ nth i ? v d1 = nth i ? v d2.
+#A #i elim i -i
+ [#n #v #d1 #d2 #ltOn lapply v @(lt_O_n_elim … ltOn)
+ -v #m #v >(vec_expand … v) //
+ |#i #Hind #n #v #d1 #d2 #ltn lapply ltn lapply v @(lt_O_n_elim … (ltn_to_ltO … ltn))
+ -v -ltn #m #v #ltim >(vec_expand … v) @(Hind m (vec_tail A (S m) v) d1 d2 ?)
+ @le_S_S_to_le //
+ ]
+qed.
+
+lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d.
+ (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2.
+#A #n elim n -n
+ [#v1 #v2 #H >(vector_nil A v1) >(vector_nil A v2) //
+ |#n #Hind #v1 #v2 #d #H >(vec_expand … v1) >(vec_expand … v2)
+ >(Hind (vec_tail … v1) (vec_tail … v2) d)
+ [cut (vec_hd A n v1 = vec_hd A n v2) //
+ cut (∀i,d1,d2. i < S n → nth i A v1 d1 = nth i A v2 d2)
+ [#i #d1 #d2 #Hi >(nth_default ????? d) // >(nth_default ???? d2 d) // @H //]
+ -H #H @(H 0) //
+ |#i #ltin @(H (S i)) @le_S_S //
+ ]
+ ]
+qed.
+
+lemma nth_vec_map :
+ ∀A,B,f,i,n.∀v:Vector A n.∀d.
+ f (nth i ? v d) = nth i ? (vec_map A B f n v) (f d).
+#A #B #f #i elim i
+[ *
+ [ #v #d >(vector_nil … v) %
+ | #n0 #v #d >(vec_expand … v) % ]
+| #i0 #IH *
+ [ #v #d >(vector_nil … v) normalize cases i0 //
+ | #n #v #d >(vec_expand … v) whd in ⊢ (??(?%)%);
+ >(IH n (vec_tail A (S n) v) d) % ] ]
+qed.
+