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

case h
α : Type u_1
i : ℕ
x y z : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1