no goals
α : Type u_1
β : Type ?u.259014
γ : Type ?u.259017
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : eval cf = fun n => Part.bind ↑(decode n) fun a => Part.map encode (f a)
cg : Code
eg : eval cg = fun n => Part.bind ↑(decode n) fun a => Part.map encode (g a)
a : α
⊢ (Part.bind (eval (bif c a then cf else cg) (encode a)) fun b => ↑(decode (a, b).snd)) = bif c a then f a else g a
cases c a <;> simp [ef, eg, encodek]