no goals
α : Type u_2
β : Type u_1
γ : Type ?u.114704
δ : Type ?u.114707
σ : Type u_3
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (Option.bind (f x) fun b => some (g x b)) = Option.map (g x) (f x)
cases f x <;> rfl