    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of the propositional prefix relation
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Binary.Prefix.Propositional.Properties {a} {A : Set a} where

    open import Data.List.Base using (List; []; _∷_)
    open import Data.List.Properties using (++-monoid)

    open import Data.List.Relation.Binary.Prefix.Heterogeneous
      using (Prefix; []; _∷_; fromView; _++_)
    open import Data.List.Relation.Binary.Prefix.Homogeneous.Properties
    import Data.List.Relation.Binary.Pointwise as Pointwise

    open import Algebra.Properties.Monoid.Divisibility (++-monoid A)

    open import Relation.Binary.PropositionalEquality using (_≡_; refl)
    open import Relation.Binary using (_⇒_)

    ------------------------------------------------------------------------
    -- The inductive definition of the propositional Prefix relation is
    -- equivalent to the notion of left divisibility induced by the
    -- (List A, _++_, []) monoid

    Prefix-as-∣ˡ : Prefix _≡_ ⇒ _∣ˡ_
    Prefix-as-∣ˡ []          = ε∣ˡ _
    Prefix-as-∣ˡ (refl ∷ tl) = x∣ˡy⇒zx∣ˡzy (_ ∷ []) (Prefix-as-∣ˡ tl)

    ∣ˡ-as-Prefix : _∣ˡ_ ⇒ Prefix _≡_
    ∣ˡ-as-Prefix (rest , refl) = fromView (Pointwise.refl refl ++ rest)