rw [update_noteq]
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ update (vecCons x t) 0 y (succ j) = vecCons y t (succ j)
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ vecCons x t (succ j) = vecCons y t (succ j)

case h
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ j ≠ 0