    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Decidability of the disjoint relation over setoid equality.
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (DecSetoid)

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

    open import Data.Product.Base using (_,_)
    open import Data.List.Relation.Unary.Any using (map)
    open import Data.List.Relation.Unary.All using (all?; lookupₛ)
    open import Data.List.Relation.Unary.All.Properties using (¬All⇒Any¬)
    open import Relation.Binary.Definitions using (Decidable)
    open import Relation.Nullary using (yes; no; decidable-stable)
    open DecSetoid S
    open import Data.List.Relation.Binary.Equality.DecSetoid S
    open import Data.List.Relation.Binary.Disjoint.Setoid setoid public
    open import Data.List.Membership.DecSetoid S

    disjoint? : Decidable Disjoint
    disjoint? xs ys with all? (_∉? ys) xs
    ... | yes xs♯ys = yes λ (v∈ , v∈′) →
      lookupₛ setoid (λ x≈y ∉ys ∈ys → ∉ys (map (trans x≈y) ∈ys)) xs♯ys v∈ v∈′
    ... | no ¬xs♯ys = let (x , x∈ , ¬∉ys) = find (¬All⇒Any¬ (_∉? _) _ ¬xs♯ys) in
      no λ p → p (x∈ , decidable-stable (_ ∈? _) ¬∉ys)