-lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d.
- nth i ? v2 d = t →
- (∀j.i ≠ j → nth j ? v1 d = nth j ? v2 d) →
- v2 = change_vec ?? v1 t i.
-#sig #n #v1 #v2 #i #t #d #H1 #H2 @(eq_vec … d)
-#i0 #Hlt cases (decidable_eq_nat i0 i) #Hii0
-[ >Hii0 >nth_change_vec //
-| >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @H2 @sym_not_eq // ]
-qed.
-