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 : Partrec₂ h
a : α
⊢ (bif Sum.casesOn (f a) (fun b => true) fun b => false then
      Sum.casesOn (f a) (fun b => Part.map Option.some (g (a, b).fst (a, b).snd)) fun c => Part.some Option.none
    else Sum.casesOn (f a) (fun b => Part.some Option.none) fun b => Part.map Option.some (h (a, b).fst (a, b).snd)) =
    Part.map Option.some (Sum.casesOn (f a) (g a) (h a))
cases f a <;> simp only [Bool.cond_true, Bool.cond_false]