right
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x x
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ x = x