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