rw [not_mem_semVars] at 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.set (PropAssignment.setMany τ vs τ') x (τ' x) ⊨ φ ↔ PropAssignment.setMany τ vs τ' ⊨ φ
ν : 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 : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
⊢ PropAssignment.set (PropAssignment.setMany τ vs τ') x (τ' x) ⊨ φ ↔ PropAssignment.setMany τ vs τ' ⊨ φ