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