next x₀ s' hx₀ ih =>
  let σ₁' := σ₁.set x₀ (!σ₁ x₀)
  by_cases h₁' : σ₁' ⊨ φ
  case neg =>
    use x₀, σ₁
    simp [h₁, h₁']
  case pos =>
    have hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x := fun x hMem => by
      have hX : x₀ ≠ x := fun h => hx₀ (h ▸ hMem)
      simp only [σ₁', σ₁.set_get_of_ne (!σ₁ x₀) hX]
      exact hS _ (Finset.mem_insert_of_mem hMem)
    have hSC' : ∀ x ∈ φ.vars \ s', σ₁' x = σ₂ x := fun x hMem => by
      by_cases hX : x₀ = x
      case pos =>
        have := hS _ (Finset.mem_insert_self _ _)
        simp only [σ₁', ← hX, PropAssignment.set_get, Bool.bnot_eq,
                    this, not_false_eq_true]
      case neg =>
        simp only [σ₁', σ₁.set_get_of_ne _ hX]
        aesop
    have ⟨x, τ, hx, H⟩ := ih h₁' hS' hSC'
    exact ⟨x, τ, Finset.mem_insert_of_mem hx, H⟩
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) φ
no goals