aesop
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
v : ν
⊢ (if v ∈ xs₁ ∨ v ∈ xs₂ then τ' v else τ v) = if v ∈ xs₂ then τ' v else if v ∈ xs₁ then τ' v else τ v
no goals