case mp =>
  intro ⟨τ, hτ, hτ'⟩
  by_contra h
  have := τ.set_get_of_ne (!τ y) h
  exact hτ' (hτ ▸ this)
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) → y = x
no goals