    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- A larger example for sublists (propositional case):
    -- Simply-typed lambda terms with globally unique variables
    -- (both bound and free ones).
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where

    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; sym; cong; subst)
    open import Relation.Binary.PropositionalEquality.Properties
      using (module ≡-Reasoning)
    open ≡-Reasoning

    open import Data.List.Base using (List; []; _∷_; [_])
    open import Data.List.Membership.Propositional using (_∈_)
    open import Data.List.Relation.Unary.All using (Null; [])
    open import Data.List.Relation.Binary.Sublist.Propositional using
      ( _⊆_; []; _∷_; _∷ʳ_
      ; ⊆-refl; ⊆-trans; minimum
      ; from∈; to∈; lookup
      ; ⊆-pushoutˡ; RawPushout
      ; Disjoint; DisjointUnion
      ; separateˡ; Separation
      )
    open import Data.List.Relation.Binary.Sublist.Propositional.Properties using
      ( ∷ˡ⁻
      ; ⊆-trans-assoc
      ; from∈∘to∈; from∈∘lookup; lookup-⊆-trans
      ; ⊆-pushoutˡ-is-wpo
      ; Disjoint→DisjointUnion; DisjointUnion→Disjoint
      ; Disjoint-sym; DisjointUnion-inj₁; DisjointUnion-inj₂; DisjointUnion-[]ʳ
      ; weakenDisjoint; weakenDisjointUnion; shrinkDisjointˡ
      ; disjoint⇒disjoint-to-union; DisjointUnion-fromAny∘toAny-∷ˡ⁻
      ; equalize-separators
      )

    open import Data.Product.Base using (_,_; proj₁; proj₂)

    infixr 8 _⇒_
    infix 1 _⊢_~_▷_

    -- Simple types over a set Base of base types.

    data Ty : Set where
      base : (o : Base) → Ty
      _⇒_ : (a b : Ty) → Ty

    -- Typing contexts are lists of types.

    Cxt = List Ty

    variable
      a b : Ty
      Γ Δ : Cxt
      x y : a ∈ Γ

    -- The familiar intrinsically well-typed formulation of STLC
    -- where a de Bruijn index x is a pointer into the context.

    module DeBruijn where

      data Tm (Δ : Cxt) : (a : Ty) → Set where
        var : (x : a ∈ Δ) → Tm Δ a
        abs : (t : Tm (a ∷ Δ) b) → Tm Δ (a ⇒ b)
        app : (t : Tm Δ (a ⇒ b)) (u : Tm Δ a) → Tm Δ b

    -- We formalize now intrinsically well-typed STLC with
    -- named variables that are globally unique, i.e.,
    -- each variable can be bound at most once.

    -- List of bound variables of a term.

    BVars = List Ty

    variable
      B    : BVars
      noBV : Null B

    -- There is a single global context Γ of all variables used in the terms.
    -- Each list of bound variables B is a sublist of Γ.

    variable
      β βₜ βᵤ yβ β\y : B ⊆ Γ

    -- Named terms are parameterized by a sublist β : B ⊆ Γ of bound variables.
    -- Variables outside B can occur as free variables in a term.
    --
    --   * Variables x do not contain any bound variables (Null B).
    --
    --   * The bound variables of an application (t u) is the disjoint union
    --     of the bound variables βₜ of t and βᵤ of u.
    --
    --   * The bound variables β of an abstraction λyt is the disjoint union
    --     of the single variable y and the bound variables β\y of t.

    module UniquelyNamed where

      data Tm (β : B ⊆ Γ) : (a : Ty) → Set where

        var : (noBV : Null B)
              (x : a ∈ Γ)
            → Tm β a

        abs : (y : a ∈ Γ)
              (y# : DisjointUnion (from∈ y) β\y β)
              (t : Tm β\y b)
            → Tm β (a ⇒ b)

        app : (t : Tm βₜ (a ⇒ b))
              (u : Tm βᵤ a)
              (t#u : DisjointUnion βₜ βᵤ β)
            → Tm β b

      pattern var! x = var [] x

      -- Bound variables β : B ⊆ Γ can be considered in a larger context Γ′
      -- obtained by γ : Γ ⊆ Γ′.  The embedding β′ : B ⊆ Γ′ is simply the
      -- composition of β and γ, and terms can be coerced recursively:

      weakenBV : ∀ {Γ B Γ′} {β : B ⊆ Γ} (γ : Γ ⊆ Γ′)  →
              Tm β a → Tm (⊆-trans β γ) a

      weakenBV γ (var noBV x)  = var noBV (lookup γ x)
      weakenBV γ (app t u t#u) = app (weakenBV γ t) (weakenBV γ u) (weakenDisjointUnion γ t#u)
      weakenBV γ (abs y y# t)  = abs y′ y′# (weakenBV γ t)
        where
        y′  = lookup γ y
        -- Typing:  y′# : DisjointUnion (from∈ y′) (⊆-trans β\y γ) (⊆-trans β γ)
        y′# = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#)

    -- We bring de Bruijn terms into scope as Exp.

    open DeBruijn renaming (Tm to Exp)
    open UniquelyNamed

    variable
      t u  : Tm β a
      f e  : Exp Δ a

    -- Relating de Bruijn terms and uniquely named terms.
    --
    -- The judgement δ ⊢ e ~ β ▷ t relates a de Bruijn term e with
    -- potentially free variables δ : Δ ⊆ Γ to a named term t with exact
    -- bound variables β : B ⊆ Γ.  The intention is to relate exactly the
    -- terms with the same meaning.
    --
    -- The judgement will imply the disjointness of Δ and B.

    variable
      δ yδ : Δ ⊆ Γ

    data _⊢_~_▷_ {Γ Δ : Cxt} (δ : Δ ⊆ Γ) : ∀{a} (e : Exp Δ a) {B} (β : B ⊆ Γ) (t : Tm β a) → Set where

      -- Free de Bruijn index x : a ∈ Δ is related to free variable
      -- y : a ∈ Γ if δ : Δ ⊆ Γ maps x to y.

      var : ∀{y} (δx≡y : lookup δ x ≡ y) (δ#β : Disjoint δ β)
          → δ ⊢ var x ~ β ▷ var! y

      -- Unnamed lambda δ ⊢ λ.e is related to named lambda y,β ▷ λy.t
      -- if body y,δ ⊢ e is related to body β ▷ t.

      abs : (y#δ : DisjointUnion (from∈ y) δ yδ)
          → (y#β : DisjointUnion (from∈ y) β yβ)
          → yδ ⊢ e ~ β ▷ t
          → δ ⊢ abs e ~ yβ ▷ abs y y#β t

      -- Application δ ⊢ f e is related to application βₜ,βᵤ ▷ t u
      -- if function δ ⊢ f is related to βₜ ▷ t
      -- and argument δ ⊢ e is related to βᵤ ▷ u.

      app : δ ⊢ f ~ βₜ ▷ t
          → δ ⊢ e ~ βᵤ ▷ u
          → (t#u : DisjointUnion βₜ βᵤ β)
          → δ ⊢ app f e ~ β ▷ app t u t#u

    -- A dependent substitution lemma for ~.
    -- Trivial, but needed because term equality t : Tm β a ≡ t′ : Tm β′ a is heterogeneous,
    -- or, more precisely, indexed by a sublist equality β ≡ β′.

    subst~ : ∀ {a Δ Γ B} {δ δ′ : Δ ⊆ Γ} {β β′ : B ⊆ Γ}
             {e : Exp Δ a} {t : Tm β a} {t′ : Tm β′ a}
             (δ≡δ′ : δ ≡ δ′)
             (β≡β′ : β ≡ β′)
             (t≡t′ : subst (λ □ → Tm □ a) β≡β′ t ≡ t′) →
             δ ⊢ e ~ β ▷ t →
             δ′ ⊢ e ~ β′ ▷ t′
    subst~ refl refl refl d = d

    -- The judgement δ ⊢ e ~ β ▷ t relative to Γ
    -- can be transported to a bigger context γ : Γ ⊆ Γ′.

    weaken~ : ∀{a Δ B Γ Γ′} {δ : Δ ⊆ Γ} {β : B ⊆ Γ} {e : Exp Δ a} {t : Tm β a}  (γ : Γ ⊆ Γ′)
      (let δ′ = ⊆-trans δ γ)
      (let β′ = ⊆-trans β γ)
      (let t′ = weakenBV γ t) →
      δ ⊢ e ~ β ▷ t →
      δ′ ⊢ e ~ β′ ▷ t′
    weaken~ γ (var refl δ#β)  = var (lookup-⊆-trans γ _) (weakenDisjoint γ δ#β)
    weaken~ γ (abs y#δ y#β d) = abs y′#δ′ y′#β′ (weaken~ γ d)
      where
      y′#δ′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#δ)
      y′#β′ = subst (λ □ → DisjointUnion □ _ _) (sym (from∈∘lookup _ _)) (weakenDisjointUnion γ y#β)
    weaken~ γ (app dₜ dᵤ t#u) = app (weaken~ γ dₜ) (weaken~ γ dᵤ) (weakenDisjointUnion γ t#u)

    -- Lemma:  If δ ⊢ e ~ β ▷ t, then
    -- the (potentially) free variables δ of the de Bruijn term e
    -- are disjoint from the bound variables β of the named term t.

    disjoint-fv-bv : δ ⊢ e ~ β ▷ t → Disjoint δ β
    disjoint-fv-bv (var _ δ#β) = δ#β

    disjoint-fv-bv {β = yβ} (abs y⊎δ y⊎β d) = δ#yβ
      where
      δ#y     = Disjoint-sym (DisjointUnion→Disjoint y⊎δ)
      yδ#β    = disjoint-fv-bv d
      δ⊆yδ,eq = DisjointUnion-inj₂ y⊎δ
      δ⊆yδ    = proj₁ δ⊆yδ,eq
      eq      = proj₂ δ⊆yδ,eq
      δ#β     = subst (λ □ → Disjoint □ _) eq (shrinkDisjointˡ δ⊆yδ yδ#β)
      δ#yβ    = disjoint⇒disjoint-to-union δ#y δ#β y⊎β

    disjoint-fv-bv (app dₜ dᵤ βₜ⊎βᵤ) = disjoint⇒disjoint-to-union δ#βₜ δ#βᵤ βₜ⊎βᵤ
      where
      δ#βₜ = disjoint-fv-bv dₜ
      δ#βᵤ = disjoint-fv-bv dᵤ

    -- Translating de Bruijn terms to uniquely named terms.
    --
    -- Given a de Bruijn term Δ ⊢ e : a, we seek to produce a named term
    -- β ▷ t : a that is related to the de Bruijn term.  On the way, we have
    -- to compute the global context Γ that hosts all free and bound
    -- variables of t.

    -- Record (NamedOf e) collects all the outputs of the translation of e.

    record NamedOf (e : Exp Δ a) : Set where
      constructor mkNamedOf
      field
        {glob} : Cxt                    -- Γ
        emb    : Δ ⊆ glob               -- δ : Δ ⊆ Γ
        {bv}   : BVars                  -- B
        bound  : bv ⊆ glob              -- β : B ⊆ Γ
        {tm}   : Tm bound a             -- t : Tm β a
        relate : emb ⊢ e ~ bound ▷ tm   -- δ ⊢ e ~ β ▷ t

    -- The translation.

    dB→Named : (e : Exp Δ a) → NamedOf e

    -- For the translation of a variable x : a ∈ Δ, we can pick Γ := Δ and B := [].
    -- Δ and B are obviously disjoint subsets of Γ.

    dB→Named (var x) = record
        { emb    = ⊆-refl     -- Γ := Δ
        ; bound  = minimum _  -- no bound variables
        ; relate = var refl (DisjointUnion→Disjoint DisjointUnion-[]ʳ)
        }

    -- For the translation of an abstraction
    --
    --   abs (t : Exp (a ∷ Δ) b) : Exp Δ (a ⇒ b)
    --
    -- we recursively have Γ, B and β : B ⊆ Γ with z,δ : (a ∷ Δ) ⊆ Γ
    -- and know that B # a∷Δ.
    --
    -- We keep Γ and produce embedding δ : Δ ⊆ Γ and bound variables z ⊎ β.

    dB→Named {Δ = Δ} {a = a ⇒ b} (abs e) with dB→Named e
    ... | record{ glob = Γ; emb = zδ; bound = β; relate = d } =
      record
        { glob   = Γ
        ; emb    = δ̇
        ; bound  = proj₁ (proj₂ z⊎β)
        ; relate = abs [a]⊆Γ⊎δ (proj₂ (proj₂ z⊎β)) d
        }
      where
      -- Typings:
      -- zδ   : a ∷ Δ ⊆ Γ
      -- β    : bv ⊆ Γ
      zδ#β    = disjoint-fv-bv d
      z       : a ∈ Γ
      z       = to∈ zδ
      [a]⊆Γ   = from∈ z
      δ̇       = ∷ˡ⁻ zδ
      [a]⊆Γ⊎δ = DisjointUnion-fromAny∘toAny-∷ˡ⁻ zδ
      [a]⊆aΔ  : [ a ] ⊆ (a ∷ Δ)
      [a]⊆aΔ  = refl ∷ minimum _
      eq      : ⊆-trans [a]⊆aΔ zδ ≡ [a]⊆Γ
      eq      = sym (from∈∘to∈ _)
      z#β     : Disjoint [a]⊆Γ β
      z#β     = subst (λ □ → Disjoint □ β) eq (shrinkDisjointˡ [a]⊆aΔ zδ#β)
      z⊎β     = Disjoint→DisjointUnion z#β

    -- For the translation of an application (f e) we have by induction
    -- hypothesis two independent extensions δ₁ : Δ ⊆ Γ₁ and δ₂ : Δ ⊆ Γ₂
    -- and two bound variable lists β₁ : B₁ ⊆ Γ₁ and β₂ : B₂ ⊆ Γ₂.
    -- We need to find a common global context Γ such that
    --
    --   (a) δ : Δ ⊆ Γ and
    --   (b) the bound variables embed disjointly as β₁″ : B₁ ⊆ Γ and β₂″ : B₂ ⊆ Γ.
    --
    -- (a) δ is (eventually) found via a weak pushout of δ₁ and δ₂, giving
    -- ϕ₁ : Γ₁ ⊆ Γ₁₂  and  ϕ₂ : Γ₂ ⊆ Γ₁₂.
    --
    -- (b) The bound variable embeddings
    --
    --   β₁′ = β₁ϕ₁ : B₁ ⊆ Γ₁₂ and
    --   β₂′ = β₂ϕ₂ : B₂ ⊆ Γ₁₂ and
    --
    -- may be overlapping, but we can separate them by enlarging the global
    -- context to Γ with two embeddings
    --
    --   γ₁ : Γ₁₂ ⊆ Γ
    --   γ₂ : Γ₁₂ ⊆ Γ
    --
    -- such that
    --
    --   β₁″ = β₁′γ₁ : B₁ ⊆ Γ
    --   β₂″ = β₂′γ₂ : B₂ ⊆ Γ
    --
    -- are disjoint.  Since Δ is disjoint to both B₁ and B₂ we have equality of
    --
    --   δ₁ϕ₁γ₁ : Δ ⊆ Γ
    --   δ₂ϕ₂γ₂ : Δ ⊆ Γ
    --
    -- Thus, we can return either of them as δ.

    dB→Named (app f e) with dB→Named f | dB→Named e
    ... | mkNamedOf {Γ₁} δ₁ β₁ {t} d₁ | mkNamedOf {Γ₂} δ₂ β₂ {u} d₂ =
      mkNamedOf δ̇ β̇ (app d₁″ d₂″ β₁″⊎β₂″)
      where
      -- Disjointness of δᵢ and βᵢ from induction hypotheses.
      δ₁#β₁   = disjoint-fv-bv d₁
      δ₂#β₂   = disjoint-fv-bv d₂

      -- join δ₁ and δ₂ via weak pushout
      po      = ⊆-pushoutˡ δ₁ δ₂
      Γ₁₂     = RawPushout.upperBound po
      ϕ₁      = RawPushout.leg₁ po
      ϕ₂      = RawPushout.leg₂ po
      δ₁′     = ⊆-trans δ₁ ϕ₁
      δ₂′     = ⊆-trans δ₂ ϕ₂
      β₁′     = ⊆-trans β₁ ϕ₁
      β₂′     = ⊆-trans β₂ ϕ₂
      δ₁′#β₁′ : Disjoint δ₁′ β₁′
      δ₁′#β₁′ = weakenDisjoint ϕ₁ δ₁#β₁
      δ₂′#β₂′ : Disjoint δ₂′ β₂′
      δ₂′#β₂′ = weakenDisjoint ϕ₂ δ₂#β₂
      δ₁′≡δ₂′ : δ₁′ ≡ δ₂′
      δ₁′≡δ₂′ = ⊆-pushoutˡ-is-wpo δ₁ δ₂
      δ₂′#β₁′ : Disjoint δ₂′ β₁′
      δ₂′#β₁′ = subst (λ □ → Disjoint □ β₁′) δ₁′≡δ₂′ δ₁′#β₁′

      -- separate β₁ and β₂
      sep     : Separation β₁′ β₂′
      sep     = separateˡ β₁′ β₂′
      γ₁      = Separation.separator₁ sep
      γ₂      = Separation.separator₂ sep
      β₁″     = Separation.separated₁ sep
      β₂″     = Separation.separated₂ sep

      -- produce their disjoint union
      uni     = Disjoint→DisjointUnion (Separation.disjoint sep)
      β̇       = proj₁ (proj₂ uni)
      β₁″⊎β₂″ : DisjointUnion β₁″ β₂″ β̇
      β₁″⊎β₂″ = proj₂ (proj₂ uni)
      ι₁      = DisjointUnion-inj₁ β₁″⊎β₂″
      ι₂      = DisjointUnion-inj₂ β₁″⊎β₂″

      -- after separation, the FVs are still disjoint from the BVs.
      δ₁″     = ⊆-trans δ₂′ γ₁
      δ₂″     = ⊆-trans δ₂′ γ₂
      δ₁″≡δ₂″ : δ₁″ ≡ δ₂″
      δ₁″≡δ₂″ = equalize-separators δ₂′#β₁′ δ₂′#β₂′
      δ₁″#β₁″ : Disjoint δ₁″ β₁″
      δ₁″#β₁″ = weakenDisjoint γ₁ δ₂′#β₁′
      δ₂″#β₂″ : Disjoint δ₂″ β₂″
      δ₂″#β₂″ = weakenDisjoint γ₂ δ₂′#β₂′
      δ̇       = δ₂″
      δ₂″#β₁″ : Disjoint δ₂″ β₁″
      δ₂″#β₁″ = subst (λ □ → Disjoint □ β₁″) δ₁″≡δ₂″ δ₁″#β₁″
      δ̇#β̇     : Disjoint δ̇ β̇
      δ̇#β̇     = disjoint⇒disjoint-to-union δ₂″#β₁″ δ₂″#β₂″ β₁″⊎β₂″

      -- Combined weakening from Γᵢ to Γ
      γ₁′     = ⊆-trans ϕ₁ γ₁
      γ₂′     = ⊆-trans ϕ₂ γ₂

      -- Weakening and converting the first derivation.
      d₁′     : ⊆-trans δ₁ γ₁′ ⊢ f ~ ⊆-trans β₁ γ₁′ ▷ weakenBV γ₁′ t
      d₁′     = weaken~ γ₁′ d₁
      δ₁≤δ̇    : ⊆-trans δ₁ γ₁′ ≡ ⊆-trans δ₂′ γ₂
      δ₁≤δ̇    = begin
                ⊆-trans δ₁ γ₁′ ≡⟨ ⊆-trans-assoc ⟩
                ⊆-trans δ₁′ γ₁ ≡⟨ cong (λ □ → ⊆-trans □ γ₁) δ₁′≡δ₂′ ⟩
                ⊆-trans δ₂′ γ₁ ≡⟨⟩
                δ₁″            ≡⟨ δ₁″≡δ₂″ ⟩
                δ₂″            ≡⟨⟩
                δ̇              ∎
      β₁≤β₁″  : ⊆-trans β₁ γ₁′ ≡ β₁″
      β₁≤β₁″  = ⊆-trans-assoc
      d₁″     : δ̇ ⊢ f ~ β₁″ ▷ subst (λ □ → Tm □ _) β₁≤β₁″ (weakenBV γ₁′ t)
      d₁″     =  subst~ δ₁≤δ̇ β₁≤β₁″ refl d₁′

      -- Weakening and converting the second derivation.
      d₂′     : ⊆-trans δ₂ γ₂′ ⊢ e ~ ⊆-trans β₂ γ₂′ ▷ weakenBV γ₂′ u
      d₂′     = weaken~ γ₂′ d₂
      β₂≤β₂″  : ⊆-trans β₂ γ₂′ ≡ β₂″
      β₂≤β₂″  = ⊆-trans-assoc
      δ₂≤δ̇    : ⊆-trans δ₂ γ₂′ ≡ δ̇
      δ₂≤δ̇    = ⊆-trans-assoc
      d₂″     : δ̇ ⊢ e ~ β₂″ ▷ subst (λ □ → Tm □ _) β₂≤β₂″ (weakenBV γ₂′ u)
      d₂″     = subst~ δ₂≤δ̇ β₂≤β₂″ refl d₂′