rw [Finset.insert_eq, Finset.union_inter_distrib_right
    , Finset.singleton_inter_of_mem h]
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∈ semVars φ
⊢ PropAssignment.setMany τ (insert x vs) τ' ⊨ φ ↔ PropAssignment.setMany τ (insert x vs ∩ semVars φ) τ' ⊨ φ
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∈ semVars φ
⊢ PropAssignment.setMany τ ({x} ∪ vs) τ' ⊨ φ ↔ PropAssignment.setMany τ ({x} ∪ vs ∩ semVars φ) τ' ⊨ φ