simp only [vecCons, cons_succ]
α : Type u_1
i : ℕ
w x y z : α
t : Fin i → α
j : Fin i
⊢ vecCons w (vecCons x (vecCons y t)) (succ (succ (succ j))) =
    vecCons w (vecCons x (vecCons z t)) (succ (succ (succ j)))
no goals