letI : ∀ n, Primcodable { t : UTerm L μ₁ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const n))
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p 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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)