------------------------------------------------------------------------ -- Equational resoning for preorders ------------------------------------------------------------------------ open import Tools.Relation module Tools.Reasoning.Preorder {a ℓ ℓ′} (P : Preorder a ℓ ℓ′) where open import Relation.Binary.Reasoning.Preorder P public