intro i
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),
    (do
        let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
        f (v.get 0) (v.get 1)) =
      f (g i) (h i)
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
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)