------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties related to Data.Star
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
-- module directly.
------------------------------------------------------------------------
{-# OPTIONS --without-K --safe #-}
module Data.Star.Properties where
open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
public