aesop
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
no goals