no goals
α : Type u_1
β : Type ?u.66894
σ : Type ?u.66897
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : ℕ → ℕ → α
h : Primrec (Nat.unpaired f)
⊢ Primrec₂ f
simpa using h.comp natPair