simp only [funext_iff, forall_fin_succ]
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
⊢ update (vecCons w (vecCons x (vecCons y t))) 2 z = vecCons w (vecCons x (vecCons z t))
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
⊢ update (vecCons w (vecCons x (vecCons y t))) 2 z 0 = vecCons w (vecCons x (vecCons z t)) 0 ∧
    update (vecCons w (vecCons x (vecCons y t))) 2 z (succ 0) = vecCons w (vecCons x (vecCons z t)) (succ 0) ∧
      update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ 0)) =
          vecCons w (vecCons x (vecCons z t)) (succ (succ 0)) ∧
        ∀ (i_1 : Fin i),
          update (vecCons w (vecCons x (vecCons y t))) 2 z (succ (succ (succ i_1))) =
            vecCons w (vecCons x (vecCons z t)) (succ (succ (succ i_1)))