intro p q
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)
⊢ ∀ (a b : Semiformula L μ n), encode ((↑(subfEquiv a)).or ↑(subfEquiv b)) = encode (a ⋎ b)
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)
p q : Semiformula L μ n
⊢ encode ((↑(subfEquiv p)).or ↑(subfEquiv q)) = encode (p ⋎ q)