simp_all only [vars, satisfies_var, Finset.mem_singleton]
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ ⊨ var y
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ var y
⊢ x ∈ vars (var y)
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ y = true
hτ' : ¬PropAssignment.set τ x (!τ x) y = true
⊢ x = y