have : (!τ' x) = τ x := by
  simp only [τ', τ.set_get x, Bool.not_not]
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ