no goals
α : Type u_1
β : Type u_2
γ : Type ?u.61762
σ : Type u_3
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α →. β
g : α → β → σ
hf : Partrec f
hg : Computable₂ g
⊢ Partrec fun a => Part.map (g a) (f a)
simpa [bind_some_eq_map] using @Partrec.bind _ _ _ _ _ _ _ (fun a => Part.some ∘ (g a)) hf hg