simp [*]
case h'.h.e'_4
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
a✝ : PropAssignment.set τ x b ⊨ φ
⊢ τ = PropAssignment.set (PropAssignment.set τ x b) x !PropAssignment.set τ x b x
no goals