. have : σ₁.agreeOn φ.vars σ₂ := by rw [Finset.sdiff_empty] at hSC; exact hSC
  have : σ₂ ⊨ φ := (agreeOn_vars this).mp h₁
  exact False.elim (h₂ this)
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ

case insert
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s✝, σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s✝, σ₁ x = σ₂ x) → ∃ x τ, x ∈ s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert a✝² s✝, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert a✝² s✝, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ insert a✝² s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
case insert
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s✝, σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s✝, σ₁ x = σ₂ x) → ∃ x τ, x ∈ s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert a✝² s✝, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert a✝² s✝, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ insert a✝² s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ