intro n
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))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
⊢ ∀ (n : ℕ), (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n
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))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
n : ℕ
⊢ (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n