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

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