At the moment we have: ```agda _≤_ : Rel A _ x ≤ y = (x < y) ⊎ (x ≈ y) ``` and ```agda data ReflClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where refl : Reflexive (ReflClosure _∼_) [_] : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _∼_ x y ``` Should we merge the two definitions by introducing a separate inductive type for `_≤_` and implementing `ReflClosure` in terms of it? This would make `ReflClosure` more lazy by changing the type of `refl` from `Reflexive _` to `x ≡ y → ReflClosure _∼_ x y`.