intro hxy hyx
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
⊢ reflRel r x y → reflRel r y x → x = y
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : reflRel r x y
hyx : reflRel r y x
⊢ x = y