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