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