no goals
α : Type u_1
β : Type ?u.127167
γ : Type ?u.127170
δ : Type ?u.127173
σ : Type u_2
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec 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