simp only [mem_semVars]
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∈ semVars φᶜ ↔ x ∈ semVars φ
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ) ↔ ∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ