exact this.of_eq (fun s a => by
  induction' s with s ih <;> simp[*]; { exact Eq.symm (Function.iterate_succ_apply' f s a) })
α : 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
⊢ Primrec₂ fun x x_1 => f^[x] x_1
no goals