funext j
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
case h
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
j : Fin (succ 1)
⊢ ![↑g, ↑h] j i = pure (![g i, h i] j)