rw[←ofFn_get v.tail]
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f v.tail
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)