match hxy, hyx with
| Or.inr rfl, _ => rfl
| _, Or.inr rfl => rfl
| Or.inl hxy, Or.inl hyx =>
  absurd hxy
  exact Asymmetric.asymm hyx
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : reflRel r x y
hyx : reflRel r y x
⊢ x = y
no goals