simp
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ (n + 1)), (↑fun v => f v.tail v.head) i = (fun x x_1 => Part.some (f x x_1)) i.tail i.head
no goals