ext v
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v : ν
τ' : PropAssignment ν
⊢ setMany τ {v} τ' = set τ v (τ' v)
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ {v✝} τ' v = set τ v✝ (τ' v✝) v