apply Exists.intro F
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ ∃ x ∈ Δ_U,
    (if evalPrime V x then x else x.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : PredName
xs : List VarName
F : Formula := pred_var_ X xs
h1 : pred_var_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧
    (if evalPrime V F then F else F.not_) = if V (pred_var_ X xs) = true then pred_var_ X xs else (pred_var_ X xs).not_