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