exact hτ' (hτ ▸ τ.set_get_of_ne (!τ x) h)
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ y = true
hτ' : ¬PropAssignment.set τ x (!τ x) y = true
h : ¬x = y
⊢ False
no goals