simp only [evalPrimeFfToNot]
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V false_)
Δ_U : Set Formula
V : VarBoolAssignment
h1 : True
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U) (if evalPrime V false_ then false_ else false_.not_)