    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Convenient syntax for reasoning with a setoid
    ------------------------------------------------------------------------

    -- Example use:

    -- n*0≡0 : ∀ n → n * 0 ≡ 0
    -- n*0≡0 zero    = refl
    -- n*0≡0 (suc n) = begin
    --   suc n * 0 ≈⟨ refl ⟩
    --   n * 0 + 0 ≈⟨ ... ⟩
    --   n * 0     ≈⟨ n*0≡0 n ⟩
    --   0         ∎

    -- Module `≡-Reasoning` in `Relation.Binary.PropositionalEquality`
    -- is recommended for equational reasoning when the underlying equality
    -- is `_≡_`.

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Reasoning.Syntax using (module ≈-syntax)

    module Relation.Binary.Reasoning.Setoid {s₁ s₂} (S : Setoid s₁ s₂) where

    open Setoid S

    import Relation.Binary.Reasoning.Base.Single _≈_ refl trans
      as SingleRelReasoning

    ------------------------------------------------------------------------
    -- Reasoning combinators

    -- Export the combinators for single relation reasoning, hiding the
    -- single misnamed combinator.
    open SingleRelReasoning public
      hiding (step-∼)
      renaming (∼-go to ≈-go)

    -- Re-export the equality-based combinators instead
    open ≈-syntax _IsRelatedTo_ _IsRelatedTo_ ≈-go sym public