    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of list appending
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (Setoid)

    module Data.List.Relation.Ternary.Appending.Setoid.Properties
      {c l} (S : Setoid c l)
      where

    open import Data.List.Base as List using (List; [])
    import Data.List.Properties as List
    open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
    import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
    open import Data.Product.Base using (∃-syntax; _×_; _,_)
    open import Function.Base using (id)
    open import Relation.Binary.Core using (_⇒_)
    open import Relation.Binary.PropositionalEquality.Core using (refl)
    open import Relation.Binary.Construct.Composition using (_;_)

    open Setoid S renaming (Carrier to A)
    open import Relation.Binary.Properties.Setoid S using (≈;≈⇒≈; ≈⇒≈;≈)
    open import Data.List.Relation.Ternary.Appending.Setoid S

    private
      variable
        as bs cs ds : List A

    ------------------------------------------------------------------------
    -- Re-exporting existing properties

    open Appendingₚ public
      using (conicalˡ; conicalʳ)

    ------------------------------------------------------------------------
    -- Proving setoid-specific ones

    []++⁻¹ : Appending [] bs cs → Pointwise _≈_ bs cs
    []++⁻¹ ([]++ rs) = rs

    ++[]⁻¹ : Appending as [] cs → Pointwise _≈_ as cs
    ++[]⁻¹ {as} {cs} ls with break ls
    ... | cs₁ , cs₂ , refl , pw , []
      rewrite List.++-identityʳ cs₁
      = pw

    respʳ-≋ : ∀ {cs′} → Appending as bs cs → Pointwise _≈_ cs cs′ →
              Appending as bs cs′
    respʳ-≋ = Appendingₚ.respʳ-≋ trans trans

    respˡ-≋ : ∀ {as′ bs′} → Pointwise _≈_ as′ as → Pointwise _≈_ bs′ bs →
              Appending as bs cs → Appending as′ bs′ cs
    respˡ-≋ = Appendingₚ.respˡ-≋ trans trans

    through→ :
      ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs →
      ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs
    through→ = Appendingₚ.through→ ≈⇒≈;≈ id

    through← :
      ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs →
      ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs
    through← = Appendingₚ.through← ≈;≈⇒≈ id

    assoc→ :
      ∃[ xs ] Appending as bs xs × Appending xs cs ds →
      ∃[ ys ] Appending bs cs ys × Appending as ys ds
    assoc→ = Appendingₚ.assoc→ ≈⇒≈;≈ id ≈;≈⇒≈