match hxy, hyz with
| Or.inr rfl, Or.inr rfl => right; rfl
| Or.inr rfl, Or.inl hyz => left; exact hyz
| Or.inl hxy, Or.inr rfl => left; exact hxy
| Or.inl hxy, Or.inl hyz => left; exact Transitive.trans hxy hyz
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x z
no goals