intro v
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ n),
    (do
        let v ← mOfFn fun i_1 => (g :> fun i v => ↑(Option.some (v.get i))) i_1 i
        f v.tail v.head) =
      (g i).bind (f i)
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i => (g :> fun i v => ↑(Option.some (v.get i))) i v
      f v.tail v.head) =
    (g v).bind (f v)