have : Primrec₂ (fun p q => UFormula.or (subfEquiv p) (subfEquiv q)
    : Semiformula L μ n → Semiformula L μ n → UFormula L μ) :=
  UFormula.or_primrec.comp₂
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.left)
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.right)
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_1 => x ⋎ x_1
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 q => (↑(subfEquiv p)).or ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋎ x_1