rw [funext_iff]
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1) = vecCons y (vecCons x t)
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ ∀ (a : Fin (Nat.succ (Nat.succ i))), (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) a = vecCons y (vecCons x t) a