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