    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Pairs of lists that share no common elements (setoid equality)
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (Setoid)

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

    open import Level using (_⊔_)
    open import Relation.Nullary.Negation using (¬_)
    open import Function.Base using (_∘_)
    open import Data.List.Base using (List; []; [_]; _∷_)
    open import Data.List.Relation.Unary.Any using (here; there)
    open import Data.Product.Base using (_×_; _,_)
    open import Relation.Binary.Core using (Rel)

    open Setoid S renaming (Carrier to A)
    open import Data.List.Membership.Setoid S using (_∈_; _∉_)

    ------------------------------------------------------------------------
    -- Definition

    Disjoint : Rel (List A) (ℓ ⊔ c)
    Disjoint xs ys = ∀ {v} → ¬ (v ∈ xs × v ∈ ys)

    ------------------------------------------------------------------------
    -- Operations

    contractₗ : ∀ {x xs ys} → Disjoint (x ∷ xs) ys → Disjoint xs ys
    contractₗ x∷xs∩ys=∅ (v∈xs , v∈ys) = x∷xs∩ys=∅ (there v∈xs , v∈ys)

    contractᵣ : ∀ {xs y ys} → Disjoint xs (y ∷ ys) → Disjoint xs ys
    contractᵣ xs#y∷ys (v∈xs , v∈ys) = xs#y∷ys (v∈xs , there v∈ys)