funext i
case h
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
⊢ (fun i => (g :> fun j v => Part.some (v.get j)) i v) = fun i => pure ((x :> fun j => v.get j) i)
case h.h
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
i : Fin n.succ
⊢ (g :> fun j v => Part.some (v.get j)) i v = pure ((x :> fun j => v.get j) i)