have : Primrec (fun p => UFormula.ex (subfEquiv p) : Semiformula L μ (n + 1) → UFormula L μ) :=
  UFormula.ex_primrec.comp (subtype_val.comp $ of_equiv)
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => ∃' x
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).ex
⊢ Primrec fun x => ∃' x