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 : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a =>
    Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)
a : α
⊢ (Option.casesOn (Sum.casesOn (f a) (fun x => Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b => Option.some (g a b)) fun x => Option.none)) fun c =>
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a))
cases f a <;> simp