no goals
α : Type u_2
β : Type u_3
γ : Type ?u.116843
δ : Type ?u.116846
σ : Type u_1
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β → Option σ
h : Primrec₂ fun a n => Option.bind (decode n) (f a)
⊢ Primrec₂ f
simpa [encodek] using h.comp fst ((@Primrec.encode β _).comp snd)