cases h
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
h : y = x
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
case refl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ x (!τ x) x = true