no goals
α : Type u_1
β : Type u_2
γ : Type ?u.109928
δ : Type ?u.109931
σ : Type ?u.109934
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (g a) (fun n IH => h a (n, IH).snd) (f a) = (h a^[f a]) (g a)
induction f a <;> simp [*, -Function.iterate_succ, Function.iterate_succ']