no goals
α : Type u_2
β : Type u_1
γ : Type ?u.191844
σ : Type ?u.191847
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn (f a) (g a) fun b => b) = Option.getD (f a) (g a)
cases f a <;> rfl