no goals
α : Type u_1
β : Type ?u.182461
γ : Type ?u.182464
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode (c a)) (g a) fun b => f (a, b).fst) = bif c a then f a else g a
cases c a <;> rfl