simp [setMany, set]
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ set (setMany τ xs τ') v✝ b v = setMany (set τ v✝ b) xs τ' v
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ (if v = v✝ then b else if v ∈ xs then τ' v else τ v) = if v ∈ xs then τ' v else if v = v✝ then b else τ v