no goals
α : Type u_2
β : Type u_1
γ : Type ?u.183096
σ : Type u_3
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (Option.some (f a)) fun n => Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (o a) (f a) (g a))
cases o a <;> simp [encodek]