have : Primrec₂ (fun s a => s.rec a (fun _ => f) : ℕ → α → α) :=
  to₂ (nat_rec' fst snd (hf.comp₂ (snd.comp₂ Primrec₂.right)))
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
⊢ Primrec₂ fun x x_1 => f^[x] x_1
α : 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