let g' : ℕ → α := fun x => if x < m then g x else f x
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
⊢ Primrec g
case intro.succ
σ : 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 γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ Primrec g