rcases Part.eq_none_or_eq_some (g v) with (hgv | ⟨x, hgv⟩)
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
case inl
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
hgv : g v = Part.none
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)

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) = (g v).bind (f v)