refine' ⟨rfl, rfl, fun j => _⟩
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) 0 = vecCons y (vecCons x t) 0 ∧
    (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ 0) = vecCons y (vecCons x t) (succ 0) ∧
      ∀ (i_1 : Fin i),
        (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ i_1)) = vecCons y (vecCons x t) (succ (succ i_1))
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ (vecCons x (vecCons y t) ∘ ↑(Equiv.swap 0 1)) (succ (succ j)) = vecCons y (vecCons x t) (succ (succ j))