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