------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

open import Prelude

open import Labelled-transition-system

module Bisimilarity.Classical.Equational-reasoning-instances
         {lts : LTS} { : Level} where

open import Bisimilarity.Classical lts

open import Equational-reasoning

instance

  reflexive∼ : Reflexive [  ]_∼_
  reflexive∼ = is-reflexive reflexive-∼

  symmetric∼ : Symmetric [  ]_∼_
  symmetric∼ = is-symmetric symmetric-∼

  trans∼∼ : Transitive [  ]_∼_ [  ]_∼_
  trans∼∼ = is-transitive transitive-∼

  convert∼∼ : Convertible [  ]_∼_ [  ]_∼_
  convert∼∼ = is-convertible id