simp_all [s]
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
s : Finset ν := Finset.filter (fun x => σ₁ x ≠ σ₂ x) (vars φ)
hS : ∀ x ∈ s, σ₁ x ≠ σ₂ x
⊢ ∀ x ∈ vars φ \ s, σ₁ x = σ₂ x
no goals