rw [Equiv.swap_apply_of_ne_of_ne, cons_succ, cons_succ]
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ cons x (cons y t) (↑(Equiv.swap 0 1) (succ (succ j))) = t j
case a
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 0

case a
α : Type u_1
i : ℕ
x y : α
t : Fin i → α
j : Fin i
⊢ succ (succ j) ≠ 1