no goals
α : Type u_1
β : Type ?u.135479
γ : Type ?u.135482
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. σ
h : Nat.Partrec fun n => Part.bind ↑(decode₂ α n) fun a => Part.map encode (f a)
⊢ Partrec fun a => Part.map encode (f a)
simpa [encodek₂] using (nat_iff.2 h).comp (@Computable.encode α _)