have ⟨σ₁, hA, hS⟩ := (e τ).mp ⟨τ, τ.agreeOn_refl _, h⟩
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
⊢ τ ⊨ φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
⊢ τ ⊨ φ₂