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