{ exact Eq.symm (Function.iterate_succ_apply' f s a) }
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
a : α
s : ℕ
ih : Nat.rec a (fun x => f) s = f^[s] a
⊢ f (f^[s] a) = f^[s] (f a)
no goals