simp only [evalPrimeFfToNot]
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V (forall_ x phi))
Δ_U : Set Formula
V : VarBoolAssignment
x : VarName
phi : Formula
phi_ih : ↑phi.primeSet ⊆ Δ_U → IsDeduct (evalPrimeFfToNot V '' Δ_U) (evalPrimeFfToNot V phi)
F : Formula := forall_ x phi
h1 : forall_ x phi ∈ Δ_U
⊢ IsDeduct ((fun a => if evalPrime V a then a else a.not_) '' Δ_U)
    (if evalPrime V (forall_ x phi) then forall_ x phi else (forall_ x phi).not_)