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

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

open import Labelled-transition-system

module Bisimilarity.Weak.Coinductive.Equational-reasoning-instances
{lts : LTS} where

open import Prelude

open import Bisimilarity.Coinductive lts
import Bisimilarity.Coinductive.Equational-reasoning-instances
open import Bisimilarity.Weak.Coinductive lts
open import Equational-reasoning

instance

trans∼≈ : ∀ {i} → Transitive _∼_ [ i ]_≈_
trans∼≈ = is-transitive (transitive ∘ ∼⇒≈)

trans∼′≈ : ∀ {i} → Transitive _∼′_ [ i ]_≈_
trans∼′≈ = is-transitive (transitive ∘ ∼⇒≈″)

trans∼′≈′ : ∀ {i} → Transitive _∼′_ [ i ]_≈′_
trans∼′≈′ = is-transitive (transitive ∘ ∼⇒≈″)

trans∼≈′ : ∀ {i} → Transitive _∼_ [ i ]_≈′_
trans∼≈′ {i} = is-transitive (transitive ∘ ∼⇒≈ {i})

convert∼≈ : Convertible _∼_ _≈_
convert∼≈ = is-convertible ∼⇒≈

convert∼′≈ : Convertible _∼′_ _≈_
convert∼′≈ = is-convertible (convert ∘ ∼⇒≈″)

convert∼≈′ : Convertible _∼_ _≈′_
convert∼≈′ = is-convertible ∼⇒≈′

convert∼′≈′ : Convertible _∼′_ _≈′_
convert∼′≈′ = is-convertible ∼⇒≈″

open Bisimilarity.Coinductive.Equational-reasoning-instances
{lts = weak lts} public
```