exact ⟨cf.rfind, Code.eval.rfind cf f hcf⟩
case intro
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : ArithPart₁ ↑f
cf : Code (n✝ + 1)
hcf : cf.eval ↑f
⊢ ∃ c, c.eval fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
no goals