no goals
α : Type u_4
β : Type u_1
γ : Type u_2
σ : Type u_3
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
⊢ Sum.casesOn (Sum.casesOn (f a) (fun b => Sum.inr (a, b).snd) fun b => Sum.inl (a, b).snd) (fun b => Part.some (h a b))
      (g a) =
    Sum.casesOn (f a) (g a) fun c => Part.some (h a c)
cases f a <;> simp