next x vs hx ih =>
if h : x ∈ φ.semVars then
  rw [Finset.insert_eq, Finset.union_inter_distrib_right
      , Finset.singleton_inter_of_mem h]
  simp [PropAssignment.setMany_union]; apply ih
else
simp [Finset.insert_eq, Finset.union_inter_distrib_right
    , Finset.singleton_inter_of_not_mem h
    , PropAssignment.setMany_union]
rw [← ih _, ← τ.set_setMany_comm _ _ _ _ hx]
rw [not_mem_semVars] at h
rw [h]
case insert
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ s✝ τ' ⊨ φ ↔ PropAssignment.setMany τ (s✝ ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
⊢ PropAssignment.setMany τ (insert a✝² s✝) τ' ⊨ φ ↔ PropAssignment.setMany τ (insert a✝² s✝ ∩ semVars φ) τ' ⊨ φ
no goals