rw [τ.set_set, this, τ.set_same]
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) ⊨ φ
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
⊢ τ ⊨ φ