have : y ≃ x₁ := Rel.trans ‹y ≃ x₂› (Rel.symm ‹x₁ ≃ x₂›)
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : y ≄ x₁
x✝ : y ≃ x₂
⊢ False
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : y ≄ x₁
x✝ : y ≃ x₂
this : y ≃ x₁
⊢ False