    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- A solver for proving that one list is a sublist of the other.
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (DecSetoid)

    module Data.List.Relation.Binary.Sublist.DecSetoid.Solver {c ℓ} (S : DecSetoid c ℓ) where

    open DecSetoid S

    open import Data.List.Relation.Binary.Sublist.Heterogeneous.Solver _≈_ refl _≟_
      using (Item; module Item; TList; module TList; prove) public