constructor <;> {
  intro ⟨τ, hτ, hτ'⟩
  simp only [satisfies_neg, not_not] at hτ hτ' ⊢
  let τ' := τ.set x (!τ x)
  have : (!τ' x) = τ x := by
    simp only [τ', τ.set_get x, Bool.not_not]
  refine ⟨τ', hτ', ?_⟩
  rw [τ.set_set, this, τ.set_same]
  exact hτ
}
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ) ↔ ∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ
no goals