no goals
α : Type u_1
β : Type ?u.127715
γ : Type ?u.127718
δ : Type ?u.127721
σ : Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
c : α → Prop
inst✝ : DecidablePred c
f g : α → σ
hc : PrimrecPred c
hf : Primrec f
hg : Primrec g
⊢ Primrec fun a => if c a then f a else g a
simpa using cond hc hf hg