rw[←Vector.get_zero, Vector.get_tail_succ]
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.tail.head
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.get (Fin.succ 0)