have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v) := by
  rcases Nat.ArithPart₁.exists_code (of_partrec hf) with ⟨c, hc⟩
  exact ⟨c, models_code hc⟩
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
this : ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)