simp only [Finset.mem_singleton, mem_semVars, satisfies_var]
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y ∈ semVars (var x) ↔ y ∈ {x}
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) ↔ y = x