have ⟨x, τ, hx, H⟩ := ih h₁' hS' hSC'
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : 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 x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
hSC' : ∀ x ∈ vars φ \ s', σ₁' x = σ₂ x
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : 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 x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
h₁' : σ₁' ⊨ φ
hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x
hSC' : ∀ x ∈ vars φ \ s', σ₁' x = σ₂ x
x : ν
τ : PropAssignment ν
hx : x ∈ s'
H : τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ