simpa using hh
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i✝ : Fin (succ 0).succ
i : Fin 1
⊢ ArithPart₁ (![↑g, ↑h] i.succ)
no goals