exfalso
case tr
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ tr
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ tr
⊢ x ∈ vars tr
case tr
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ tr
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ tr
⊢ False