    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Documentation for subset relations over `List`s
    ------------------------------------------------------------------------

    open import Data.List.Base using (List; _∷_; [])
    open import Data.List.Membership.Propositional.Properties
      using (∈-++⁺ˡ; ∈-insert)
    open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
    open import Data.List.Relation.Unary.Any using (here; there)
    open import Relation.Binary.PropositionalEquality using (refl)

    module README.Data.List.Relation.Binary.Subset where

    ------------------------------------------------------------------------
    -- Subset Relation

    -- The Subset relation is a wrapper over `Any` and so is parameterized
    -- over an equality relation. Thus to use the subset relation we must
    -- tell Agda which equality relation to use.

    -- Decidable equality over Strings
    open import Data.String.Base using (String)
    open import Data.String.Properties using (_≟_)

    -- Open the decidable membership module using Decidable ≡ over Strings
    open import Data.List.Membership.DecPropositional _≟_

    -- Simple cases are inductive proofs

    lem₁ : ∀ {xs : List String} → xs ⊆ xs
    lem₁ p = p

    lem₂ : "A" ∷ [] ⊆ "B" ∷ "A" ∷ []
    lem₂ p = there p

    -- Or directly use the definition of subsets

    lem₃₀ : "E" ∷ "S" ∷ "B" ∷ [] ⊆ "S" ∷ "U" ∷ "B" ∷ "S" ∷ "E" ∷ "T" ∷ []
    lem₃₀ (here refl) = there (there (there (there (here refl))))  -- "E"
    lem₃₀ (there (here refl)) = here refl                          -- "S"
    lem₃₀ (there (there (here refl))) = there (there (here refl))  -- "B"

    -- Or use proofs from `Data.List.Membership.Propositional.Properties`

    lem₄ : "A" ∷  [] ⊆ "B" ∷ "A" ∷ "C" ∷ []
    lem₄ p = ∈-++⁺ˡ (there p)

    lem₅ : "B" ∷ "S" ∷ "E" ∷ [] ⊆ "S" ∷ "U" ∷ "B" ∷ "S" ∷ "E" ∷ "T" ∷ []
    lem₅ p = ∈-++⁺ˡ (there (there p))

    lem₃₁ : "E" ∷ "S" ∷ "B" ∷ [] ⊆ "S" ∷ "U" ∷ "B" ∷ "S" ∷ "E" ∷ "T" ∷ []
    lem₃₁ (here refl) = ∈-insert ("S" ∷ "U" ∷ "B" ∷ "S" ∷ [])
    lem₃₁ (there (here refl)) = here refl
    lem₃₁ (there (there (here refl))) = ∈-insert ("S" ∷ "U" ∷ [])