have := h τ (!τ x)
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
this : (PropAssignment.set τ x !τ x) ⊨ φ ↔ τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ