tauto
case a
Δ_U : Set Formula
V : VarBoolAssignment
X : DefName
xs : List VarName
F : Formula := def_ X xs
h1 : def_ X xs ∈ Δ_U
⊢ F ∈ Δ_U ∧ (if evalPrime V F then F else F.not_) = if V (def_ X xs) = true then def_ X xs else (def_ X xs).not_
no goals