simp only [Formula.evalPrime]
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (pred_const_ X xs) then pred_const_ X xs else (pred_const_ X xs).not_)
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_const_ X xs
h1 : pred_const_ X xs ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if V (pred_const_ X xs) = true then pred_const_ X xs else (pred_const_ X xs).not_)