apply Exists.intro F
case a
Δ_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
⊢ ∃ x_1 ∈ Δ_U,
    (if evalPrime V x_1 then x_1 else x_1.not_) =
      if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_
case a
Δ_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
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (forall_ x phi) = true then forall_ x phi else (forall_ x phi).not_