ext v
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
⊢ setMany τ (xs₁ ∪ xs₂) τ' = setMany (setMany τ xs₁ τ') xs₂ τ'
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ (xs₁ ∪ xs₂) τ' v = setMany (setMany τ xs₁ τ') xs₂ τ' v