have : mOfFn (fun i => (g :> fun j v => Part.some $ v.get j) i v) = pure (Vector.ofFn (x :> fun j => v.get j)) := by
  rw[←Vector.mOfFn_pure]; apply congr_arg
  funext i; cases i using Fin.cases <;> simp[hgv]
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
this : (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = pure (ofFn (x :> fun j => v.get j))
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x