exact Primrec₂.encode_iff.mp <| (Primrec.encode.comp₂ this).of_eq <| by
  intro p q
  simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
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)).and ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
no goals