suffices ∀ φ₁ φ₂ τ, equivalentOver Y φ₁ φ₂ →
    (∃ (σ₁ : PropAssignment ν), σ₁.agreeOn X τ ∧ σ₁ ⊨ φ₁) →
    ∃ (σ₂ : PropAssignment ν), σ₂.agreeOn X τ ∧ σ₂ ⊨ φ₂ from
  fun e τ => ⟨this φ₁ φ₂ τ e, this φ₂ φ₁ τ e.symm⟩
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ ∀ (φ₁ φ₂ : PropFun ν) (τ : PropAssignment ν),
    equivalentOver Y φ₁ φ₂ →
      (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂