case mp =>
  intro h
  exact ⟨fun σ₁ h₁ => h σ₁ |>.mp ⟨σ₁, σ₁.agreeOn_refl X, h₁⟩,
    fun σ₂ h₂ => h σ₂ |>.mpr ⟨σ₂, σ₂.agreeOn_refl X, h₂⟩⟩
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ → extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
no goals