have : Primrec₂ (fun _ n => Add.add.foldr One.one (List.replicate n One.one) : ℕ → ℕ → Const L) :=
  (foldr_primrec _ _).comp₂ (list_replicate.comp₂ .right (.const _))
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
⊢ Primrec (numeral L)
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral L)