simp
case empty
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
τ : PropAssignment ν
⊢ PropAssignment.setMany τ ∅ τ' ⊨ φ ↔ PropAssignment.setMany τ (∅ ∩ semVars φ) τ' ⊨ φ
no goals