intro cxy cyx
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
⊢ coRel r x y → coRel r y x → x = y
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
⊢ x = y