simp [setMany, set]
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ {v✝} τ' v = set τ v✝ (τ' v✝) v
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ (if v = v✝ then τ' v else τ v) = if v = v✝ then τ' v✝ else τ v