choose cg hcg using fun i            => exists_code (hg i)
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
cg : Fin n✝ → Code n✝¹
hcg : ∀ (i : Fin n✝), (cg i).eval (g i)
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f