no goals
α : Type ?u.81753
β : Type ?u.81756
γ : Type ?u.81759
σ : Type ?u.81762
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : ℕ →. ℕ
⊢ Partrec f ↔ Nat.Partrec f
simp [Partrec, map_id']