suffices ∀ {φ₁ φ₂} {τ : PropAssignment ν}, φ₂.semVars ⊆ X →
    equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂ by
  intro h₁ h₂ e
  ext τ
  exact ⟨this h₂ e, this h₁ e.symm⟩
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ↑(semVars φ₁) ⊆ X → ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → φ₁ = φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂