rintro ⟨n, a⟩
σ : Type u_1
α✝ : Type u_2
β : α✝ → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α✝
inst✝⁵ : (a : α✝) → Fintype (β a)
inst✝⁴ : (a : α✝) → DecidableEq (β a)
inst✝³ : (a : α✝) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
α : Type u_5
inst✝ : Primcodable α
this : Primrec₂ fun p ih => p.2 :: ih.2
⊢ ∀ (n : ℕ × α), Nat.rec [] (fun n_1 IH => n.2 :: (n_1, IH).2) n.1 = List.replicate n.1 n.2
case mk
σ : Type u_1
α✝ : Type u_2
β : α✝ → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α✝
inst✝⁵ : (a : α✝) → Fintype (β a)
inst✝⁴ : (a : α✝) → DecidableEq (β a)
inst✝³ : (a : α✝) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
α : Type u_5
inst✝ : Primcodable α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n_1 IH => (n, a).2 :: (n_1, IH).2) (n, a).1 = List.replicate (n, a).1 (n, a).2