intro ⟨h₁, h₂⟩
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁ → equivalentOver X φ₁ φ₂
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
⊢ equivalentOver X φ₁ φ₂