no goals
α : Type u_1
β : Type ?u.82494
γ : Type ?u.82497
δ : Type ?u.82500
σ : Type ?u.82503
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : ℕ → ℕ →. α
h : Partrec (Nat.unpaired f)
⊢ Partrec₂ f
simpa using Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp