no goals
α : Type u_1
β : Type ?u.132671
γ : Type ?u.132674
δ : Type ?u.132677
σ : Type ?u.132680
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
n : α
⊢ (!decide (p n)) = decide ((fun a => ¬p a) n)
simp