apply self.irrefl x
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ False
α : Sort ?u.1585
r : α → α → Prop
self : Quasiorder r
x y : α
hxy : r x y
hyx : r y x
⊢ r x x