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

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

open import Prelude

open import Labelled-transition-system

module Similarity.Strong.Equational-reasoning-instances
{lts : LTS} {i : Size} where

open import Bisimilarity.Coinductive lts
open import Equational-reasoning
open import Similarity.Strong lts

instance

reflexive≤ : Reflexive [ i ]_≤_
reflexive≤ = is-reflexive reflexive-≤

reflexive≤′ : Reflexive [ i ]_≤′_
reflexive≤′ = is-reflexive reflexive-≤′

convert≤≤ : Convertible [ i ]_≤_ [ i ]_≤_
convert≤≤ = is-convertible id

convert≤′≤ : Convertible [ ssuc i ]_≤′_ [ i ]_≤_
convert≤′≤ = is-convertible λ p≤′q → force p≤′q

convert≤≤′ : Convertible [ i ]_≤_ [ i ]_≤′_
convert≤≤′ = is-convertible lemma
where
lemma : ∀ {p q} → [ i ] p ≤ q → [ i ] p ≤′ q
force (lemma p≤q) = p≤q

convert≤′≤′ : Convertible [ i ]_≤′_ [ i ]_≤′_
convert≤′≤′ = is-convertible id

convert∼≤ : Convertible [ i ]_∼_ [ i ]_≤_
convert∼≤ = is-convertible ∼⇒≤

convert∼′≤ : Convertible [ ssuc i ]_∼′_ [ i ]_≤_
convert∼′≤ = is-convertible (convert ∘ ∼⇒≤′)

convert∼≤′ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≤′_
convert∼≤′ {i} = is-convertible lemma
where
lemma : ∀ {p q} → [ i ] p ∼ q → [ i ] p ≤′ q
force (lemma p∼q) = ∼⇒≤ p∼q

convert∼′≤′ : ∀ {i} → Convertible [ i ]_∼′_ [ i ]_≤′_
convert∼′≤′ = is-convertible ∼⇒≤′

trans≤≤ : Transitive [ i ]_≤_ [ i ]_≤_
trans≤≤ = is-transitive transitive-≤

trans≤′≤ : Transitive [ ssuc i ]_≤′_ [ i ]_≤_
trans≤′≤ = is-transitive λ p≤′q → transitive (force p≤′q)

trans≤′≤′ : Transitive [ i ]_≤′_ [ i ]_≤′_
trans≤′≤′ = is-transitive transitive-≤′

trans≤≤′ : Transitive [ i ]_≤_ [ i ]_≤′_
trans≤≤′ = is-transitive lemma
where
lemma : ∀ {p q r} → [ i ] p ≤ q → [ i ] q ≤′ r → [ i ] p ≤′ r
force (lemma p≤q q≤′r) = transitive-≤ p≤q (force q≤′r)
```