dsimp [set]
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ set τ x (τ x) x' = τ x'
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ (if x' = x then τ x else τ x') = τ x'