no goals
α : Type u_3
β : Type u_1
γ : Type ?u.184893
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn (f a) Option.none (g a) = Option.bind (f a) (g a)
cases f a <;> rfl