------------------------------------------------------------------------
-- The logical relation for validity
------------------------------------------------------------------------

open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.LogicalRelation.Substitution
  {a} {M : Set a}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  ⦃ eqrel : EqRelSet R ⦄
  where

open EqRelSet eqrel
open Type-restrictions R

open import Definition.LogicalRelation R
open import Definition.LogicalRelation.Hidden R
open import Definition.LogicalRelation.Properties R

open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Typed.Weakening R as TW using (_∷_βŠ‡_)

open import Definition.Untyped M
open import Definition.Untyped.Neutral M
open import Definition.Untyped.Properties M

open import Tools.Fin
open import Tools.Function
open import Tools.Level
open import Tools.Nat using (Nat)
open import Tools.Product as Ξ£
import Tools.PropositionalEquality as PE
open import Tools.Reasoning.PropositionalEquality
open import Tools.Unit

private variable
  m n                                                   : Nat
  Ξ“ Ξ” Ξ—                                                 : Con Term _
  A A₁ Aβ‚‚ B B₁ Bβ‚‚ C C₁ Cβ‚‚ D E t t₁ tβ‚‚ u u₁ uβ‚‚ v v₁ vβ‚‚ w : Term _
  Οƒ σ₁ Οƒβ‚‚ σ₃                                            : Subst _ _
  ρ                                                     : Wk _ _
  l lβ€² lβ€³ l‴                                            : TypeLevel

------------------------------------------------------------------------
-- The type formers

opaque mutual

  -- Valid contexts.

  infix 4 βŠ©α΅›_

  βŠ©α΅›_ : Con Term n β†’ Set a
  βŠ©α΅› Ξ΅       = Lift _ ⊀
  βŠ©α΅› (Ξ“ βˆ™ A) = βˆƒ Ξ» l β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A

  -- Valid types.

  infix 4 _βŠ©α΅›βŸ¨_⟩_

  _βŠ©α΅›βŸ¨_⟩_ : Con Term n β†’ TypeLevel β†’ Term n β†’ Set a
  Ξ“ βŠ©α΅›βŸ¨ l ⟩ A = Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ A

  -- Valid type equality.

  infix 4 _βŠ©α΅›βŸ¨_⟩_≑_

  _βŠ©α΅›βŸ¨_⟩_≑_ : Con Term n β†’ TypeLevel β†’ Term n β†’ Term n β†’ Set a
  _βŠ©α΅›βŸ¨_⟩_≑_ {n} Ξ“ l A B =
    βŠ©α΅› Ξ“ Γ—
    (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
     Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
     Ξ” ⊩⟨ l ⟩ A [ σ₁ ] ≑ B [ Οƒβ‚‚ ])

  -- Valid substitution equality.

  infix 4 _⊩˒_≑_∷_

  _⊩˒_≑_∷_ : Con Term m β†’ Subst m n β†’ Subst m n β†’ Con Term n β†’ Set a
  Ξ” ⊩˒ _  ≑ _  ∷ Ξ΅     = ⊒ Ξ”
  Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A =
    (βˆƒ Ξ» l β†’
     (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
     Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
    Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“

opaque

  -- Valid substitutions.

  infix 4 _⊩˒_∷_

  _⊩˒_∷_ : Con Term m β†’ Subst m n β†’ Con Term n β†’ Set a
  Ξ” ⊩˒ Οƒ ∷ Ξ“ = Ξ” ⊩˒ Οƒ ≑ Οƒ ∷ Ξ“

opaque

  -- Valid term equality.

  infix 4 _βŠ©α΅›βŸ¨_⟩_≑_∷_

  _βŠ©α΅›βŸ¨_⟩_≑_∷_ :
    Con Term n β†’ TypeLevel β†’ Term n β†’ Term n β†’ Term n β†’ Set a
  _βŠ©α΅›βŸ¨_⟩_≑_∷_ {n} Ξ“ l t u A =
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A Γ—
    (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
     Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’ Ξ” ⊩⟨ l ⟩ t [ σ₁ ] ≑ u [ Οƒβ‚‚ ] ∷ A [ σ₁ ])

opaque

  -- Valid terms.

  infix 4 _βŠ©α΅›βŸ¨_⟩_∷_

  _βŠ©α΅›βŸ¨_⟩_∷_ : Con Term n β†’ TypeLevel β†’ Term n β†’ Term n β†’ Set a
  Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A = Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ t ∷ A

------------------------------------------------------------------------
-- Some characterisation lemmas

opaque
  unfolding βŠ©α΅›_

  -- A characterisation lemma for βŠ©α΅›_.

  βŠ©α΅›Ξ΅β‡” : βŠ©α΅› Ξ΅ ⇔ ⊀
  βŠ©α΅›Ξ΅β‡” = _

opaque
  unfolding βŠ©α΅›_

  -- A characterisation lemma for βŠ©α΅›_.

  βŠ©α΅›βˆ™β‡” : βŠ©α΅› Ξ“ βˆ™ A ⇔ βˆƒ Ξ» l β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A
  βŠ©α΅›βˆ™β‡” = id⇔

opaque
  unfolding _βŠ©α΅›βŸ¨_⟩_

  -- A characterisation lemma for _βŠ©α΅›βŸ¨_⟩_.

  βŠ©α΅›β‡”βŠ©α΅›β‰‘ : (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) ⇔ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ A
  βŠ©α΅›β‡”βŠ©α΅›β‰‘ = id⇔

opaque
  unfolding _βŠ©α΅›βŸ¨_⟩_ _βŠ©α΅›βŸ¨_⟩_≑_

  -- A characterisation lemma for _βŠ©α΅›βŸ¨_⟩_.

  βŠ©α΅›β‡” :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ⇔
    (βŠ©α΅› Ξ“ Γ—
     (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
      Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’ Ξ” ⊩⟨ l ⟩ A [ σ₁ ] ≑ A [ Οƒβ‚‚ ]))
  βŠ©α΅›β‡” = id⇔

opaque
  unfolding _βŠ©α΅›βŸ¨_⟩_≑_

  -- A characterisation lemma for _βŠ©α΅›βŸ¨_⟩_≑_.

  βŠ©α΅›β‰‘β‡” :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B ⇔
    (βŠ©α΅› Ξ“ Γ—
     (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
      Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’ Ξ” ⊩⟨ l ⟩ A [ σ₁ ] ≑ B [ Οƒβ‚‚ ]))
  βŠ©α΅›β‰‘β‡” = id⇔

opaque
  unfolding _βŠ©α΅›βŸ¨_⟩_∷_

  -- A characterisation lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· : Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A ⇔ Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ t ∷ A
  βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· = id⇔

opaque
  unfolding _βŠ©α΅›βŸ¨_⟩_∷_ _βŠ©α΅›βŸ¨_⟩_≑_∷_

  -- A characterisation lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  βŠ©α΅›βˆ·β‡” :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A ⇔
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A Γ—
     (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
      Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
      Ξ” ⊩⟨ l ⟩ t [ σ₁ ] ≑ t [ Οƒβ‚‚ ] ∷ A [ σ₁ ]))
  βŠ©α΅›βˆ·β‡” = id⇔

opaque
  unfolding _βŠ©α΅›βŸ¨_⟩_≑_∷_

  -- A characterisation lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β‡” :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A ⇔
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A Γ—
     (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
      Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
      Ξ” ⊩⟨ l ⟩ t [ σ₁ ] ≑ u [ Οƒβ‚‚ ] ∷ A [ σ₁ ]))
  βŠ©α΅›β‰‘βˆ·β‡” = id⇔

opaque
  unfolding _⊩˒_≑_∷_

  -- A characterisation lemma for _⊩˒_≑_∷_.

  βŠ©Λ’β‰‘βˆ·Ξ΅β‡” : Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ΅ ⇔ ⊒ Ξ”
  βŠ©Λ’β‰‘βˆ·Ξ΅β‡” = id⇔

opaque
  unfolding _⊩˒_≑_∷_

  -- A characterisation lemma for _⊩˒_≑_∷_.

  βŠ©Λ’β‰‘βˆ·βˆ™β‡” :
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A ⇔
    ((βˆƒ Ξ» l β†’
      (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
      Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
     Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“)
  βŠ©Λ’β‰‘βˆ·βˆ™β‡” = id⇔

opaque
  unfolding _⊩˒_∷_

  -- A characterisation lemma for _⊩˒_∷_.

  βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· : Ξ” ⊩˒ Οƒ ∷ Ξ“ ⇔ Ξ” ⊩˒ Οƒ ≑ Οƒ ∷ Ξ“
  βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· = id⇔

opaque

  -- A characterisation lemma for _⊩˒_∷_.

  βŠ©Λ’βˆ·Ξ΅β‡” : Ξ” ⊩˒ Οƒ ∷ Ξ΅ ⇔ ⊒ Ξ”
  βŠ©Λ’βˆ·Ξ΅β‡” {Ξ”} {Οƒ} =
    Ξ” ⊩˒ Οƒ ∷ Ξ΅      β‡”βŸ¨ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· ⟩
    Ξ” ⊩˒ Οƒ ≑ Οƒ ∷ Ξ΅  β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·Ξ΅β‡” ⟩
    ⊒ Ξ”             ░⇔

opaque

  -- A characterisation lemma for _⊩˒_∷_.

  βŠ©Λ’βˆ·βˆ™β‡” :
    Ξ” ⊩˒ Οƒ ∷ Ξ“ βˆ™ A ⇔
    ((βˆƒ Ξ» l β†’ (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ— Ξ” ⊩⟨ l ⟩ head Οƒ ∷ A [ tail Οƒ ]) Γ—
     Ξ” ⊩˒ tail Οƒ ∷ Ξ“)
  βŠ©Λ’βˆ·βˆ™β‡” {Ξ”} {Οƒ} {Ξ“} {A} =
    Ξ” ⊩˒ Οƒ ∷ Ξ“ βˆ™ A                                              β‡”βŸ¨ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· ⟩

    Ξ” ⊩˒ Οƒ ≑ Οƒ ∷ Ξ“ βˆ™ A                                          β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” ⟩

    (βˆƒ Ξ» l β†’
     (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
     Ξ” ⊩⟨ l ⟩ head Οƒ ≑ head Οƒ ∷ A [ tail Οƒ ]) Γ—
    Ξ” ⊩˒ tail Οƒ ≑ tail Οƒ ∷ Ξ“                                    β‡”Λ˜βŸ¨ (Ξ£-cong-⇔ Ξ» _ β†’ Ξ£-cong-⇔ Ξ» _ β†’ βŠ©βˆ·β‡”βŠ©β‰‘βˆ·)
                                                                      Γ—-cong-⇔
                                                                    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· ⟩
    (βˆƒ Ξ» l β†’ (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ— Ξ” ⊩⟨ l ⟩ head Οƒ ∷ A [ tail Οƒ ]) Γ—
    Ξ” ⊩˒ tail Οƒ ∷ Ξ“                                             ░⇔

------------------------------------------------------------------------
-- An introduction lemma

opaque

  -- An introduction lemma for βŠ©α΅›_.

  βŠ©α΅›-βˆ™-intro : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’ βŠ©α΅› Ξ“ βˆ™ A
  βŠ©α΅›-βˆ™-intro ⊩A = βŠ©α΅›βˆ™β‡” .projβ‚‚ (_ , ⊩A)

------------------------------------------------------------------------
-- Reflexivity

opaque

  -- Reflexivity for _⊩˒_≑_∷_.

  refl-βŠ©Λ’β‰‘βˆ· :
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩˒ Οƒ ≑ Οƒ ∷ Ξ“
  refl-βŠ©Λ’β‰‘βˆ· = βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .proj₁

opaque

  -- Reflexivity for _βŠ©α΅›βŸ¨_⟩_≑_.

  refl-βŠ©α΅›β‰‘ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ A
  refl-βŠ©α΅›β‰‘ = βŠ©α΅›β‡”βŠ©α΅›β‰‘ .proj₁

opaque

  -- Reflexivity for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  refl-βŠ©α΅›β‰‘βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ t ∷ A
  refl-βŠ©α΅›β‰‘βˆ· = βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .proj₁

------------------------------------------------------------------------
-- Some substitution lemmas

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ A [ Οƒ ]
  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩A =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ βˆ˜β†’ βŠ©α΅›β‡” .proj₁ ⊩A .projβ‚‚ βˆ˜β†’ refl-βŠ©Λ’β‰‘βˆ·

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ t [ Οƒ ] ∷ A [ Οƒ ]
  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩t =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©α΅›βˆ·β‡” .proj₁ ⊩t .projβ‚‚ βˆ˜β†’ refl-βŠ©Λ’β‰‘βˆ·

------------------------------------------------------------------------
-- Symmetry

opaque

  -- Symmetry for _⊩˒_≑_∷_.

  sym-βŠ©Λ’β‰‘βˆ· :
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩˒ Οƒβ‚‚ ≑ σ₁ ∷ Ξ“
  sym-βŠ©Λ’β‰‘βˆ· {Ξ“ = Ξ΅} =
    βŠ©Λ’β‰‘βˆ·Ξ΅β‡” .projβ‚‚ βˆ˜β†’ βŠ©Λ’β‰‘βˆ·Ξ΅β‡” .proj₁
  sym-βŠ©Λ’β‰‘βˆ· {Ξ“ = _ βˆ™ _} = Ξ» σ₁≑σ₂ β†’
    case βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₁≑σ₂ of Ξ»
      ((l , ⊩A , σ₁₀≑σ₂₀) , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’
    case conv-βŠ©β‰‘βˆ· (βŠ©α΅›β‡” .proj₁ ⊩A .projβ‚‚ Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) $
         sym-βŠ©β‰‘βˆ· σ₁₀≑σ₂₀ of Ξ»
      σ₂₀≑σ₁₀ β†’
    βŠ©Λ’β‰‘βˆ·βˆ™β‡” .projβ‚‚ ((l , ⊩A , σ₂₀≑σ₁₀) , sym-βŠ©Λ’β‰‘βˆ· Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š)

opaque

  -- Symmetry for _βŠ©α΅›βŸ¨_⟩_≑_.

  sym-βŠ©α΅›β‰‘ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ B ≑ A
  sym-βŠ©α΅›β‰‘ A≑B =
    case βŠ©α΅›β‰‘β‡” .proj₁ A≑B of Ξ»
      (βŠ©Ξ“ , A≑B) β†’
    βŠ©α΅›β‰‘β‡” .projβ‚‚ (βŠ©Ξ“ , sym-βŠ©β‰‘ βˆ˜β†’ A≑B βˆ˜β†’ sym-βŠ©Λ’β‰‘βˆ·)

opaque

  -- Symmetry for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  sym-βŠ©α΅›β‰‘βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ u ≑ t ∷ A
  sym-βŠ©α΅›β‰‘βˆ· t≑u =
    case βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u of Ξ»
      (⊩A , t≑u) β†’
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( ⊩A
      , Ξ» σ₁≑σ₂ β†’
          conv-βŠ©β‰‘βˆ· (sym-βŠ©β‰‘ $ βŠ©α΅›β‡” .proj₁ ⊩A .projβ‚‚ σ₁≑σ₂) $
          sym-βŠ©β‰‘βˆ· $ t≑u $ sym-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂)

------------------------------------------------------------------------
-- One transitivity lemma

opaque

  -- Transitivity for _⊩˒_≑_∷_.

  trans-βŠ©Λ’β‰‘ :
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩˒ Οƒβ‚‚ ≑ σ₃ ∷ Ξ“ β†’
    Ξ” ⊩˒ σ₁ ≑ σ₃ ∷ Ξ“
  trans-βŠ©Λ’β‰‘ {Ξ“ = Ξ΅} σ₁≑σ₂ _ =
    βŠ©Λ’β‰‘βˆ·Ξ΅β‡” .projβ‚‚ $ βŠ©Λ’β‰‘βˆ·Ξ΅β‡” .proj₁ σ₁≑σ₂
  trans-βŠ©Λ’β‰‘ {Ξ“ = _ βˆ™ _} σ₁≑σ₂ σ₂≑σ₃ =
    case βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₁≑σ₂ of Ξ»
      ((l , ⊩A , σ₁₀≑σ₂₀) , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’
    case βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₂≑σ₃ of Ξ»
      ((l , ⊩A , σ₂₀≑σ₃₀) , Οƒβ‚‚β‚Šβ‰‘Οƒβ‚ƒβ‚Š) β†’
    case conv-βŠ©β‰‘βˆ· (βŠ©α΅›β‡” .proj₁ ⊩A .projβ‚‚ $ sym-βŠ©Λ’β‰‘βˆ· Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) σ₂₀≑σ₃₀ of Ξ»
      σ₂₀≑σ₃₀ β†’
    βŠ©Λ’β‰‘βˆ·βˆ™β‡” .projβ‚‚
      ( (l , ⊩A , trans-βŠ©β‰‘βˆ· σ₁₀≑σ₂₀ σ₂₀≑σ₃₀)
      , trans-βŠ©Λ’β‰‘ Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š Οƒβ‚‚β‚Šβ‰‘Οƒβ‚ƒβ‚Š
      )

------------------------------------------------------------------------
-- Some well-formedness lemmas

opaque

  -- A well-formedness lemma for βŠ©α΅›_.

  wf-βŠ©α΅›-βˆ™ : βŠ©α΅› Ξ“ βˆ™ A β†’ βˆƒ Ξ» l β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A
  wf-βŠ©α΅›-βˆ™ = βŠ©α΅›βˆ™β‡” .proj₁

opaque

  -- A well-formedness lemma for _βŠ©α΅›βŸ¨_⟩_.

  wf-βŠ©α΅› : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’ βŠ©α΅› Ξ“
  wf-βŠ©α΅› = proj₁ βˆ˜β†’ βŠ©α΅›β‡” .proj₁

opaque

  -- A well-formedness lemma for _βŠ©α΅›βŸ¨_⟩_.

  wf-βˆ™-βŠ©α΅› :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B β†’
    βˆƒ Ξ» lβ€² β†’ Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A
  wf-βˆ™-βŠ©α΅› = wf-βŠ©α΅›-βˆ™ βˆ˜β†’ wf-βŠ©α΅›

opaque

  -- A well-formedness lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  wf-βŠ©α΅›βˆ· : Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A
  wf-βŠ©α΅›βˆ· = proj₁ βˆ˜β†’ βŠ©α΅›βˆ·β‡” .proj₁

opaque

  -- A well-formedness lemma for _⊩˒_∷_.

  wf-⊩˒∷ : Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’ βŠ©α΅› Ξ“
  wf-⊩˒∷ {Ξ“ = Ξ΅}     = Ξ» _ β†’ βŠ©α΅›Ξ΅β‡” .projβ‚‚ _
  wf-⊩˒∷ {Ξ“ = _ βˆ™ _} =
    βŠ©α΅›βˆ™β‡” .projβ‚‚ βˆ˜β†’ Ξ£.map idαΆ  proj₁ βˆ˜β†’ proj₁ βˆ˜β†’ βŠ©Λ’βˆ·βˆ™β‡” .proj₁

opaque

  -- A well-formedness lemma for _⊩˒_≑_∷_.

  wf-βŠ©Λ’β‰‘βˆ· : Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’ Ξ” ⊩˒ σ₁ ∷ Ξ“ Γ— Ξ” ⊩˒ Οƒβ‚‚ ∷ Ξ“
  wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ =
      βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ (trans-βŠ©Λ’β‰‘ σ₁≑σ₂ (sym-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂))
    , βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ (trans-βŠ©Λ’β‰‘ (sym-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂) σ₁≑σ₂)

------------------------------------------------------------------------
-- Changing type levels

opaque

  -- Changing type levels for _βŠ©α΅›βŸ¨_⟩_≑_.

  level-βŠ©α΅›β‰‘ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ B β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A ≑ B β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B
  level-βŠ©α΅›β‰‘ ⊩A ⊩B A≑B =
    case βŠ©α΅›β‰‘β‡” .proj₁ A≑B of Ξ»
      (βŠ©Ξ“ , A≑B) β†’
    βŠ©α΅›β‰‘β‡” .projβ‚‚
      ( βŠ©Ξ“
      , Ξ» σ₁≑σ₂ β†’
          case wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ of Ξ»
            (βŠ©Οƒβ‚ , βŠ©Οƒβ‚‚) β†’
          level-βŠ©β‰‘ (βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩A βŠ©Οƒβ‚) (βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩B βŠ©Οƒβ‚‚) $
          A≑B σ₁≑σ₂
      )

opaque

  -- Changing type levels for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  level-βŠ©α΅›β‰‘βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ≑ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A
  level-βŠ©α΅›β‰‘βˆ· ⊩A t≑u =
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( ⊩A
      , Ξ» σ₁≑σ₂ β†’
          level-βŠ©β‰‘βˆ· (βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩A $ wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ .proj₁) $
          βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚ σ₁≑σ₂
      )

opaque

  -- Changing type levels for _βŠ©α΅›βŸ¨_⟩_∷_.

  level-βŠ©α΅›βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A
  level-βŠ©α΅›βˆ· ⊩A =
    βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ βˆ˜β†’ level-βŠ©α΅›β‰‘βˆ· ⊩A βˆ˜β†’ βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .proj₁

------------------------------------------------------------------------
-- More transitivity lemmas

opaque

  -- Transitivity for _βŠ©α΅›βŸ¨_⟩_≑_.

  trans-βŠ©α΅›β‰‘ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ B ≑ C β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ C
  trans-βŠ©α΅›β‰‘ {A} {B} {C} A≑B B≑C =
    case βŠ©α΅›β‰‘β‡” .proj₁ A≑B of Ξ»
      (βŠ©Ξ“ , A≑B) β†’
    case βŠ©α΅›β‰‘β‡” .proj₁ B≑C of Ξ»
      (_ , B≑C) β†’
    βŠ©α΅›β‰‘β‡” .projβ‚‚
      ( βŠ©Ξ“
      , Ξ» {_ _} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} σ₁≑σ₂ β†’
          A [ σ₁ ]  β‰‘βŸ¨ A≑B $ refl-βŠ©Λ’β‰‘βˆ· (wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ .proj₁) ⟩⊩
          B [ σ₁ ]  β‰‘βŸ¨ B≑C σ₁≑σ₂ ⟩⊩∎
          C [ Οƒβ‚‚ ]  ∎
      )

opaque

  -- Transitivity for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  trans-βŠ©α΅›β‰‘βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ≑ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ u ≑ v ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ v ∷ A
  trans-βŠ©α΅›β‰‘βˆ· {t} {u} {v} t≑u u≑v =
    case βŠ©α΅›β‰‘βˆ·β‡” .proj₁ u≑v of Ξ»
      (⊩A , u≑v) β†’
    case βŠ©α΅›β‰‘βˆ·β‡” .proj₁ $ level-βŠ©α΅›β‰‘βˆ· ⊩A t≑u of Ξ»
      (_ , t≑u) β†’
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( ⊩A
      , Ξ» {_ _} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} σ₁≑σ₂ β†’
          t [ σ₁ ]  β‰‘βŸ¨ t≑u $ refl-βŠ©Λ’β‰‘βˆ· (wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ .proj₁) ⟩⊩∷
          u [ σ₁ ]  β‰‘βŸ¨ u≑v σ₁≑σ₂ ⟩⊩∷∎
          v [ Οƒβ‚‚ ]  ∎
      )

------------------------------------------------------------------------
-- More well-formedness lemmas

opaque

  -- A well-formedness lemma for _βŠ©α΅›βŸ¨_⟩_≑_.

  wf-βŠ©α΅›β‰‘ : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A Γ— Ξ“ βŠ©α΅›βŸ¨ l ⟩ B
  wf-βŠ©α΅›β‰‘ A≑B =
      βŠ©α΅›β‡”βŠ©α΅›β‰‘ .projβ‚‚ (trans-βŠ©α΅›β‰‘ A≑B (sym-βŠ©α΅›β‰‘ A≑B))
    , βŠ©α΅›β‡”βŠ©α΅›β‰‘ .projβ‚‚ (trans-βŠ©α΅›β‰‘ (sym-βŠ©α΅›β‰‘ A≑B) A≑B)

opaque

  -- A well-formedness lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  wf-βŠ©α΅›β‰‘βˆ· : Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A Γ— Ξ“ βŠ©α΅›βŸ¨ l ⟩ u ∷ A
  wf-βŠ©α΅›β‰‘βˆ· t≑u =
      βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ (trans-βŠ©α΅›β‰‘βˆ· t≑u (sym-βŠ©α΅›β‰‘βˆ· t≑u))
    , βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ (trans-βŠ©α΅›β‰‘βˆ· (sym-βŠ©α΅›β‰‘βˆ· t≑u) t≑u)

------------------------------------------------------------------------
-- More characterisation lemmas

opaque

  -- A variant of βŠ©α΅›β‰‘β‡”.

  βŠ©α΅›β‰‘β‡”β€² :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B ⇔
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A Γ—
     Ξ“ βŠ©α΅›βŸ¨ l ⟩ B Γ—
     (βˆ€ {m Ξ”} {Οƒ : Subst m n} β†’
      Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
      Ξ” ⊩⟨ l ⟩ A [ Οƒ ] ≑ B [ Οƒ ]))
  βŠ©α΅›β‰‘β‡”β€² {A} {B} =
      (Ξ» A≑B β†’
         case wf-βŠ©α΅›β‰‘ A≑B of Ξ»
           (⊩A , ⊩B) β†’
         ⊩A , ⊩B , Ξ» {_ _ _} β†’ βŠ©α΅›β‰‘β‡” .proj₁ A≑B .projβ‚‚ βˆ˜β†’ refl-βŠ©Λ’β‰‘βˆ·)
    , (Ξ» (⊩A , _ , A≑B) β†’
         βŠ©α΅›β‰‘β‡” .projβ‚‚
           ( wf-βŠ©α΅› ⊩A
           , Ξ» {_ _} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} σ₁≑σ₂ β†’
               A [ σ₁ ]  β‰‘βŸ¨ βŠ©α΅›β‡” .proj₁ ⊩A .projβ‚‚ σ₁≑σ₂ ⟩⊩
               A [ Οƒβ‚‚ ]  β‰‘βŸ¨ A≑B $ wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ .projβ‚‚ ⟩⊩∎
               B [ Οƒβ‚‚ ]  ∎
           ))

opaque

  -- A variant of βŠ©α΅›β‰‘β‡”.

  βŠ©α΅›β‰‘β‡”β€³ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B ⇔
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A Γ—
     Ξ“ βŠ©α΅›βŸ¨ l ⟩ B Γ—
     (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
      Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
      Ξ” ⊩⟨ l ⟩ A [ σ₁ ] ≑ B [ Οƒβ‚‚ ]))
  βŠ©α΅›β‰‘β‡”β€³ =
      (Ξ» A≑B β†’
         case wf-βŠ©α΅›β‰‘ A≑B of Ξ»
           (⊩A , ⊩B) β†’
         ⊩A , ⊩B , Ξ» {_ _ _ _} β†’ βŠ©α΅›β‰‘β‡” .proj₁ A≑B .projβ‚‚)
    , (Ξ» (⊩A , _ , A≑B) β†’
         βŠ©α΅›β‰‘β‡” .projβ‚‚ (wf-βŠ©α΅› ⊩A , A≑B))

opaque

  -- A variant of βŠ©α΅›β‰‘βˆ·β‡”.

  βŠ©α΅›β‰‘βˆ·β‡”β€² :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A ⇔
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A Γ—
     Ξ“ βŠ©α΅›βŸ¨ l ⟩ u ∷ A Γ—
     (βˆ€ {m Ξ”} {Οƒ : Subst m n} β†’
      Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
      Ξ” ⊩⟨ l ⟩ t [ Οƒ ] ≑ u [ Οƒ ] ∷ A [ Οƒ ]))
  βŠ©α΅›β‰‘βˆ·β‡”β€² {t} {u} =
      (Ξ» t≑u β†’
         case wf-βŠ©α΅›β‰‘βˆ· t≑u of Ξ»
           (⊩t , ⊩u) β†’
         ⊩t , ⊩u , Ξ» {_ _ _} β†’ βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚ βˆ˜β†’ refl-βŠ©Λ’β‰‘βˆ·)
    , (Ξ» (_ , ⊩u , t≑u) β†’
         βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
           ( wf-βŠ©α΅›βˆ· ⊩u
           , Ξ» {_ _} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} σ₁≑σ₂ β†’
               t [ σ₁ ]  β‰‘βŸ¨ t≑u $ wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ .proj₁ ⟩⊩∷
               u [ σ₁ ]  β‰‘βŸ¨ βŠ©α΅›βˆ·β‡” .proj₁ ⊩u .projβ‚‚ σ₁≑σ₂ ⟩⊩∷∎
               u [ Οƒβ‚‚ ]  ∎
           ))

opaque

  -- A variant of βŠ©α΅›β‰‘βˆ·β‡”.

  βŠ©α΅›β‰‘βˆ·β‡”β€³ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A ⇔
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A Γ—
     Ξ“ βŠ©α΅›βŸ¨ l ⟩ u ∷ A Γ—
     (βˆ€ {m Ξ”} {σ₁ Οƒβ‚‚ : Subst m n} β†’
      Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
      Ξ” ⊩⟨ l ⟩ t [ σ₁ ] ≑ u [ Οƒβ‚‚ ] ∷ A [ σ₁ ]))
  βŠ©α΅›β‰‘βˆ·β‡”β€³ =
      (Ξ» t≑u β†’
         case wf-βŠ©α΅›β‰‘βˆ· t≑u of Ξ»
           (⊩t , ⊩u) β†’
         ⊩t , ⊩u , Ξ» {_ _ _ _} β†’ βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚)
    , (Ξ» (⊩t , _ , t≑u) β†’
         βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚ (wf-βŠ©α΅›βˆ· ⊩t , t≑u))

opaque

  -- A variant of βŠ©Λ’βˆ·βˆ™β‡”.

  βŠ©Λ’βˆ·βˆ™β‡”β€² :
    Ξ” ⊩˒ Οƒ ∷ Ξ“ βˆ™ A ⇔
    ((βˆƒ Ξ» l β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
     (βˆƒ Ξ» l β†’ Ξ” ⊩⟨ l ⟩ head Οƒ ∷ A [ tail Οƒ ]) Γ—
     Ξ” ⊩˒ tail Οƒ ∷ Ξ“)
  βŠ©Λ’βˆ·βˆ™β‡”β€² {Ξ”} {Οƒ} {Ξ“} {A} =
    Ξ” ⊩˒ Οƒ ∷ Ξ“ βˆ™ A                                              β‡”βŸ¨ βŠ©Λ’βˆ·βˆ™β‡” ⟩

    (βˆƒ Ξ» l β†’ (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ— Ξ” ⊩⟨ l ⟩ head Οƒ ∷ A [ tail Οƒ ]) Γ—
    Ξ” ⊩˒ tail Οƒ ∷ Ξ“
                                                                β‡”βŸ¨ (Ξ» ((l , ⊩A , ⊩head) , ⊩tail) β†’
                                                                      (l , ⊩A) , (l , ⊩head) , ⊩tail)
                                                                 , (Ξ» ((l₁ , ⊩A) , (_ , ⊩head) , ⊩tail) β†’
                                                                      (l₁ , ⊩A , level-⊩∷ (βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩A ⊩tail) ⊩head) , ⊩tail)
                                                                 ⟩
    (βˆƒ Ξ» l β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
    (βˆƒ Ξ» l β†’ Ξ” ⊩⟨ l ⟩ head Οƒ ∷ A [ tail Οƒ ]) Γ—
    Ξ” ⊩˒ tail Οƒ ∷ Ξ“                                             ░⇔

opaque

  -- A variant of βŠ©Λ’β‰‘βˆ·βˆ™β‡”.

  βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² :
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A ⇔
    ((βˆƒ Ξ» l β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
     (βˆƒ Ξ» l β†’ Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
     Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“)
  βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² {Ξ”} {σ₁} {Οƒβ‚‚} {Ξ“} {A} =
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A                                            β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” ⟩

    (βˆƒ Ξ» l β†’
     (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ— Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
    Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                                      β‡”βŸ¨ (Ξ» ((l , ⊩A , head≑head) , tail≑tail) β†’
                                                                          (l , ⊩A) , (l , head≑head) , tail≑tail)
                                                                     , (Ξ» ((l₁ , ⊩A) , (_ , head≑head) , tail≑tail) β†’
                                                                            ( l₁ , ⊩A
                                                                            , level-βŠ©β‰‘βˆ· (βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩A (wf-βŠ©Λ’β‰‘βˆ· tail≑tail .proj₁))
                                                                                head≑head
                                                                            )
                                                                          , tail≑tail)
                                                                     ⟩
    (βˆƒ Ξ» l β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
    (βˆƒ Ξ» l β†’ Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
    Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                                      ░⇔

------------------------------------------------------------------------
-- Conversion

opaque

  -- Conversion for one of the contexts for _⊩˒_≑_∷_.

  conv-βŠ©Λ’β‰‘βˆ·-βˆ™ :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’ Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A β†’ Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ B
  conv-βŠ©Λ’β‰‘βˆ·-βˆ™ {Ξ“} {A} {B} {Ξ”} {σ₁} {Οƒβ‚‚} A≑B =
    case βŠ©α΅›β‰‘β‡”β€² .proj₁ A≑B of Ξ»
      (_ , ⊩B , A≑B) β†’

    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A                                            β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” βŸ©β†’

    (βˆƒ Ξ» l β†’
     (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ— Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
    Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                                      β†’βŸ¨ (Ξ» ((_ , ⊩A , σ₁₀≑σ₂₀) , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’
                                                                            (_ , ⊩B , conv-βŠ©β‰‘βˆ· (A≑B $ wf-βŠ©Λ’β‰‘βˆ· Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š .proj₁) σ₁₀≑σ₂₀)
                                                                          , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) ⟩
    (βˆƒ Ξ» l β†’
     (Ξ“ βŠ©α΅›βŸ¨ l ⟩ B) Γ— Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ B [ tail σ₁ ]) Γ—
    Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                                      β‡”Λ˜βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” βŸ©β†’

    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ B                                            β–‘

opaque

  -- Conversion for one of the contexts for _⊩˒_∷_.

  conv-⊩˒∷-βˆ™ : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’ Ξ” ⊩˒ Οƒ ∷ Ξ“ βˆ™ A β†’ Ξ” ⊩˒ Οƒ ∷ Ξ“ βˆ™ B
  conv-⊩˒∷-βˆ™ A≑B =
    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ βˆ˜β†’ conv-βŠ©Λ’β‰‘βˆ·-βˆ™ A≑B βˆ˜β†’ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .proj₁

opaque

  -- Conversion for the context for _βŠ©α΅›βŸ¨_⟩_.

  conv-βˆ™-βŠ©α΅› :
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A ≑ B β†’
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ C β†’
    Ξ“ βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C
  conv-βˆ™-βŠ©α΅› {Ξ“} {A} {B} {l} {C} A≑B ⊩C =
    case βŠ©α΅›β‰‘β‡”β€² .proj₁ A≑B of Ξ»
      (⊩A , ⊩B , A≑B) β†’
    βŠ©α΅›β‡” .projβ‚‚
      ( βŠ©α΅›-βˆ™-intro ⊩B
      , Ξ» {_} {Ξ” = Ξ”} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} β†’
          Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ B                            β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” βŸ©β†’

          (βˆƒ Ξ» l β†’
           (Ξ“ βŠ©α΅›βŸ¨ l ⟩ B) Γ—
           Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ B [ tail σ₁ ]) Γ—
          Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                      β†’βŸ¨ (Ξ» ((_ , _ , σ₁₀≑σ₂₀) , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’
                                                                  (_ , ⊩A , conv-βŠ©β‰‘βˆ· (sym-βŠ©β‰‘ $ A≑B $ wf-βŠ©Λ’β‰‘βˆ· Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š .proj₁) σ₁₀≑σ₂₀)
                                                                , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) ⟩
          (βˆƒ Ξ» l β†’
           (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
           Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
          Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                      β‡”Λ˜βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” βŸ©β†’

          Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A                            β†’βŸ¨ βŠ©α΅›β‡” .proj₁ ⊩C .projβ‚‚ ⟩

          Ξ” ⊩⟨ l ⟩ C [ σ₁ ] ≑ C [ Οƒβ‚‚ ]                    β–‘
      )

opaque

  -- Another kind of conversion for the context for _βŠ©α΅›βŸ¨_⟩_.

  conv-βˆ™βˆ™-βŠ©α΅› :
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A₁ ≑ Aβ‚‚ β†’
    Ξ“ βˆ™ A₁ βŠ©α΅›βŸ¨ lβ€³ ⟩ B₁ ≑ Bβ‚‚ β†’
    Ξ“ βˆ™ A₁ βˆ™ B₁ βŠ©α΅›βŸ¨ l ⟩ C β†’
    Ξ“ βˆ™ Aβ‚‚ βˆ™ Bβ‚‚ βŠ©α΅›βŸ¨ l ⟩ C
  conv-βˆ™βˆ™-βŠ©α΅› {Ξ“} {A₁} {Aβ‚‚} {B₁} {Bβ‚‚} {l} {C} A₁≑Aβ‚‚ B₁≑Bβ‚‚ ⊩C =
    case sym-βŠ©α΅›β‰‘ A₁≑Aβ‚‚ of Ξ»
      A₂≑A₁ β†’
    case βŠ©α΅›β‰‘β‡”β€² .proj₁ B₁≑Bβ‚‚ of Ξ»
      (⊩B₁ , ⊩Bβ‚‚ , B₁≑Bβ‚‚) β†’
    βŠ©α΅›β‡” .projβ‚‚
      ( βŠ©α΅›-βˆ™-intro (conv-βˆ™-βŠ©α΅› A₁≑Aβ‚‚ ⊩Bβ‚‚)
      , Ξ» {_} {Ξ” = Ξ”} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} β†’
          Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ Aβ‚‚ βˆ™ Bβ‚‚                       β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” βŸ©β†’

          (βˆƒ Ξ» l β†’
           (Ξ“ βˆ™ Aβ‚‚ βŠ©α΅›βŸ¨ l ⟩ Bβ‚‚) Γ—
           Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ Bβ‚‚ [ tail σ₁ ]) Γ—
          Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“ βˆ™ Aβ‚‚                  β†’βŸ¨ ((Ξ» ((_ , _ , σ₁₀≑σ₂₀) , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’
                                                                   ( _ , ⊩B₁
                                                                   , conv-βŠ©β‰‘βˆ·
                                                                       (sym-βŠ©β‰‘ $ B₁≑Bβ‚‚ $
                                                                        conv-⊩˒∷-βˆ™ A₂≑A₁ $ wf-βŠ©Λ’β‰‘βˆ· Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š .proj₁)
                                                                       σ₁₀≑σ₂₀
                                                                   )
                                                                 , conv-βŠ©Λ’β‰‘βˆ·-βˆ™ A₂≑A₁ Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š)) ⟩
          (βˆƒ Ξ» l β†’
           (Ξ“ βˆ™ A₁ βŠ©α΅›βŸ¨ l ⟩ B₁) Γ—
           Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ B₁ [ tail σ₁ ]) Γ—
          Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“ βˆ™ A₁                  β‡”Λ˜βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” βŸ©β†’

          Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A₁ βˆ™ B₁                       β†’βŸ¨ βŠ©α΅›β‡” .proj₁ ⊩C .projβ‚‚ ⟩

          Ξ” ⊩⟨ l ⟩ C [ σ₁ ] ≑ C [ Οƒβ‚‚ ]                     β–‘
      )

opaque

  -- Conversion for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  conv-βŠ©α΅›β‰‘βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ≑ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ B
  conv-βŠ©α΅›β‰‘βˆ· A≑B t≑u =
    case βŠ©α΅›β‰‘β‡”β€² .proj₁ A≑B of Ξ»
      (_ , ⊩B , A≑B) β†’
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( ⊩B
      , Ξ» σ₁≑σ₂ β†’
          conv-βŠ©β‰‘βˆ· (A≑B $ wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ .proj₁) $
          βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚ σ₁≑σ₂
      )

opaque

  -- Conversion for _βŠ©α΅›βŸ¨_⟩_∷_.

  conv-βŠ©α΅›βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ B
  conv-βŠ©α΅›βˆ· A≑B =
    βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ βˆ˜β†’ conv-βŠ©α΅›β‰‘βˆ· A≑B βˆ˜β†’ βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .proj₁

opaque

  -- Conversion for the context for _βŠ©α΅›βŸ¨_⟩_∷_.

  conv-βˆ™-βŠ©α΅›βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A ≑ B β†’
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ C β†’
    Ξ“ βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t ∷ C
  conv-βˆ™-βŠ©α΅›βˆ· A≑B ⊩t =
    case βŠ©α΅›βˆ·β‡” .proj₁ ⊩t of Ξ»
      (⊩C , t≑t) β†’
    βŠ©α΅›βˆ·β‡” .projβ‚‚
      ( conv-βˆ™-βŠ©α΅› A≑B ⊩C
      , t≑t βˆ˜β†’ conv-βŠ©Λ’β‰‘βˆ·-βˆ™ (sym-βŠ©α΅›β‰‘ A≑B)
      )

------------------------------------------------------------------------
-- Expansion

opaque

  -- An expansion lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  βŠ©α΅›βˆ·-⇐ :
    (βˆ€ {m Ξ”} {Οƒ : Subst m n} β†’
     Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
     Ξ” ⊒ t [ Οƒ ] β‡’ u [ Οƒ ] ∷ A [ Οƒ ]) β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A
  βŠ©α΅›βˆ·-⇐ {t} {u} tβ‡’u ⊩u =
    case βŠ©α΅›βˆ·β‡” .proj₁ ⊩u of Ξ»
      (⊩A , u≑u) β†’
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( ⊩A
      , Ξ» {_ _} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} σ₁≑σ₂ β†’
          case wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ of Ξ»
            (βŠ©Οƒβ‚ , _) β†’
          case βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]∷ ⊩u βŠ©Οƒβ‚ of Ξ»
            ⊩u[σ₁] β†’
          t [ σ₁ ]  β‰‘βŸ¨ ⊩∷-⇐* (tβ‡’u βŠ©Οƒβ‚ ⇨ id (escape-⊩∷ ⊩u[σ₁])) ⊩u[σ₁] ⟩⊩∷
          u [ σ₁ ]  β‰‘βŸ¨ u≑u σ₁≑σ₂ ⟩⊩∷∎
          u [ Οƒβ‚‚ ]  ∎
      )

------------------------------------------------------------------------
-- Some lemmas related to _⊩˒_∷_ and _⊩˒_≑_∷_

opaque

  -- A cast lemma for _⊩˒_∷_.

  cast-⊩˒∷ :
    ((x : Fin n) β†’ σ₁ x PE.≑ Οƒβ‚‚ x) β†’
    Ξ” ⊩˒ σ₁ ∷ Ξ“ β†’ Ξ” ⊩˒ Οƒβ‚‚ ∷ Ξ“
  cast-⊩˒∷ {Ξ“ = Ξ΅} _ βŠ©Οƒβ‚ =
    βŠ©Λ’βˆ·Ξ΅β‡” .projβ‚‚ $ βŠ©Λ’βˆ·Ξ΅β‡” .proj₁ βŠ©Οƒβ‚
  cast-⊩˒∷ {Ξ“ = _ βˆ™ A} σ₁≑σ₂ βŠ©Οƒβ‚ =
    case βŠ©Λ’βˆ·βˆ™β‡” .proj₁ βŠ©Οƒβ‚ of Ξ»
      ((_ , ⊩A , βŠ©Οƒβ‚β‚€) , βŠ©Οƒβ‚β‚Š) β†’
    case σ₁≑σ₂ βˆ˜β†’ (_+1) of Ξ»
      Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š β†’
    βŠ©Λ’βˆ·βˆ™β‡” .projβ‚‚
      ( ( _ , ⊩A
        , PE.substβ‚‚ (_⊩⟨_⟩_∷_ _ _) (σ₁≑σ₂ x0)
            (substVar-to-subst Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š A) βŠ©Οƒβ‚β‚€
        )
      , cast-⊩˒∷ Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š βŠ©Οƒβ‚β‚Š
      )

opaque

  -- A lemma related to _β€’β‚›_.

  βŠ©Λ’β‰‘βˆ·-β€’β‚› :
    ⊒ Ξ— β†’
    ρ ∷ Ξ— βŠ‡ Ξ” β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ— ⊩˒ ρ β€’β‚› σ₁ ≑ ρ β€’β‚› Οƒβ‚‚ ∷ Ξ“
  βŠ©Λ’β‰‘βˆ·-β€’β‚› {Ξ“ = Ξ΅} βŠ’Ξ— _ _ =
    βŠ©Λ’β‰‘βˆ·Ξ΅β‡” .projβ‚‚ βŠ’Ξ—
  βŠ©Λ’β‰‘βˆ·-β€’β‚› {Ξ“ = _ βˆ™ A} βŠ’Ξ— ΟβŠ‡ σ₁≑σ₂ =
    case βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₁≑σ₂ of Ξ»
      ((_ , ⊩A , σ₁₀≑σ₂₀) , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’
    βŠ©Λ’β‰‘βˆ·βˆ™β‡” .projβ‚‚
      ( ( _ , ⊩A
        , PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (wk-subst A)
            (wk-βŠ©β‰‘βˆ· ΟβŠ‡ βŠ’Ξ— σ₁₀≑σ₂₀)
        )
      , βŠ©Λ’β‰‘βˆ·-β€’β‚› βŠ’Ξ— ΟβŠ‡ Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š
      )

opaque

  -- A lemma related to _β€’β‚›_.

  ⊩˒∷-β€’β‚› :
    ⊒ Ξ— β†’
    ρ ∷ Ξ— βŠ‡ Ξ” β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ— ⊩˒ ρ β€’β‚› Οƒ ∷ Ξ“
  ⊩˒∷-β€’β‚› βŠ’Ξ— ΟβŠ‡ =
    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©Λ’β‰‘βˆ·-β€’β‚› βŠ’Ξ— ΟβŠ‡ βˆ˜β†’ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .proj₁

opaque

  -- A lemma related to _β‚›β€’_.

  βŠ©Λ’β‰‘βˆ·-β‚›β€’ :
    ρ ∷ Ξ” βŠ‡ Ξ“ β†’ βŠ©α΅› Ξ“ β†’ Ξ— ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ” β†’
    Ξ— ⊩˒ σ₁ β‚›β€’ ρ ≑ Οƒβ‚‚ β‚›β€’ ρ ∷ Ξ“
  βŠ©Λ’β‰‘βˆ·-β‚›β€’ TW.id _ σ₁≑σ₂ =
    σ₁≑σ₂
  βŠ©Λ’β‰‘βˆ·-β‚›β€’ (TW.step ΟβŠ‡) βŠ©Ξ“ σ₁≑σ₂ =
    case βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₁≑σ₂ of Ξ»
      ((_ , ⊩A , head≑head) , tail≑tail) β†’
    βŠ©Λ’β‰‘βˆ·-β‚›β€’ ΟβŠ‡ βŠ©Ξ“ tail≑tail
  βŠ©Λ’β‰‘βˆ·-β‚›β€’ (TW.lift {A} ΟβŠ‡) βŠ©Ξ“βˆ™A σ₁≑σ₂ =
    case wf-βŠ©α΅›-βˆ™ βŠ©Ξ“βˆ™A of Ξ»
      (_ , ⊩A) β†’
    case βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₁≑σ₂ of Ξ»
      ((_ , _ , head≑head) , tail≑tail) β†’
    βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
      ( (_ , ⊩A)
      , (_ , PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (subst-wk A) head≑head)
      , βŠ©Λ’β‰‘βˆ·-β‚›β€’ ΟβŠ‡ (wf-βŠ©α΅› ⊩A) tail≑tail
      )

opaque

  -- A lemma related to _β‚›β€’_.

  ⊩˒∷-β‚›β€’ : ρ ∷ Ξ” βŠ‡ Ξ“ β†’ βŠ©α΅› Ξ“ β†’ Ξ— ⊩˒ Οƒ ∷ Ξ” β†’ Ξ— ⊩˒ Οƒ β‚›β€’ ρ ∷ Ξ“
  ⊩˒∷-β‚›β€’ ΟβŠ‡ βŠ©Ξ“ =
    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©Λ’β‰‘βˆ·-β‚›β€’ ΟβŠ‡ βŠ©Ξ“ βˆ˜β†’ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .proj₁

opaque

  -- A lemma related to wk1Subst.

  βŠ©Λ’β‰‘βˆ·-wk1Subst :
    Ξ” ⊒ A β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” βˆ™ A ⊩˒ wk1Subst σ₁ ≑ wk1Subst Οƒβ‚‚ ∷ Ξ“
  βŠ©Λ’β‰‘βˆ·-wk1Subst ⊒A = βŠ©Λ’β‰‘βˆ·-β€’β‚› (βŠ’β†’βŠ’βˆ™ ⊒A) (TW.step TW.id)

opaque

  -- A lemma related to wk1Subst.

  ⊩˒∷-wk1Subst :
    Ξ” ⊒ A β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” βˆ™ A ⊩˒ wk1Subst Οƒ ∷ Ξ“
  ⊩˒∷-wk1Subst ⊒A =
    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©Λ’β‰‘βˆ·-wk1Subst ⊒A βˆ˜β†’ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .proj₁

opaque

  -- A lemma related to liftSubst.

  βŠ©Λ’β‰‘βˆ·-liftSubst :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ σ₁ ] ⊩˒ liftSubst σ₁ ≑ liftSubst Οƒβ‚‚ ∷ Ξ“ βˆ™ A
  βŠ©Λ’β‰‘βˆ·-liftSubst {A} ⊩A σ₁≑σ₂ =
    case escape-⊩ $ βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩A (wf-βŠ©Λ’β‰‘βˆ· σ₁≑σ₂ .proj₁) of Ξ»
      ⊒A[σ₁] β†’
    case βŠ©Λ’β‰‘βˆ·-wk1Subst ⊒A[σ₁] σ₁≑σ₂ of Ξ»
      Οƒβ‚β‡‘β‚Šβ‰‘Οƒβ‚‚β‡‘β‚Š β†’
    case var (βŠ’β†’βŠ’βˆ™ ⊒A[σ₁])
           (PE.substβ‚‚ (_∷_∈_ _) (PE.sym $ wk1Subst-wk1 A) PE.refl
              here) of Ξ»
      ⊒0 β†’
    βŠ©Λ’β‰‘βˆ·βˆ™β‡” .projβ‚‚
      ( ( _ , ⊩A
        , neutral-βŠ©β‰‘βˆ· (βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[] ⊩A $ wf-βŠ©Λ’β‰‘βˆ· Οƒβ‚β‡‘β‚Šβ‰‘Οƒβ‚‚β‡‘β‚Š .proj₁)
            (var _) (var _) ⊒0 ⊒0 (~-var ⊒0)
        )
      , Οƒβ‚β‡‘β‚Šβ‰‘Οƒβ‚‚β‡‘β‚Š
      )

opaque

  -- A lemma related to liftSubst.

  ⊩˒∷-liftSubst :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ Οƒ ] ⊩˒ liftSubst Οƒ ∷ Ξ“ βˆ™ A
  ⊩˒∷-liftSubst ⊩A =
    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©Λ’β‰‘βˆ·-liftSubst ⊩A βˆ˜β†’ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .proj₁

opaque

  -- A variant of βŠ©Λ’β‰‘βˆ·-liftSubst.

  βŠ©Λ’β‰‘βˆ·-liftSubstβ€² :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A₁ ≑ Aβ‚‚ β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” βˆ™ A₁ [ σ₁ ] ⊩˒ liftSubst σ₁ ≑ liftSubst Οƒβ‚‚ ∷ Ξ“ βˆ™ Aβ‚‚
  βŠ©Λ’β‰‘βˆ·-liftSubstβ€² {A₁} {Aβ‚‚} {σ₁} A₁≑Aβ‚‚ σ₁≑σ₂ =
    conv-βŠ©Λ’β‰‘βˆ·-βˆ™ A₁≑Aβ‚‚ $
    βŠ©Λ’β‰‘βˆ·-liftSubst (wf-βŠ©α΅›β‰‘ A₁≑Aβ‚‚ .proj₁) σ₁≑σ₂

opaque

  -- A variant of ⊩˒∷-liftSubst.

  ⊩˒∷-liftSubstβ€² :
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A₁ ≑ Aβ‚‚ β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” βˆ™ A₁ [ Οƒ ] ⊩˒ liftSubst Οƒ ∷ Ξ“ βˆ™ Aβ‚‚
  ⊩˒∷-liftSubstβ€² A₁≑Aβ‚‚ =
    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©Λ’β‰‘βˆ·-liftSubstβ€² A₁≑Aβ‚‚ βˆ˜β†’ βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .proj₁

opaque

  -- A lemma related to idSubst.

  ⊩˒∷-idSubst :
    βŠ©α΅› Ξ“ β†’
    Ξ“ ⊩˒ idSubst ∷ Ξ“
  ⊩˒∷-idSubst {Ξ“ = Ξ΅} _ =
    βŠ©Λ’βˆ·Ξ΅β‡” .projβ‚‚ Ξ΅
  ⊩˒∷-idSubst {Ξ“ = _ βˆ™ _} βŠ©Ξ“βˆ™A =
    case βŠ©α΅›βˆ™β‡” .proj₁ βŠ©Ξ“βˆ™A .projβ‚‚ of Ξ»
      ⊩A β†’
    PE.subst₃ _⊩˒_∷_ (PE.cong (_βˆ™_ _) $ subst-id _) PE.refl PE.refl $
    cast-⊩˒∷ subst-lift-id $
    ⊩˒∷-liftSubst (βŠ©α΅›βˆ™β‡” .proj₁ βŠ©Ξ“βˆ™A .projβ‚‚)
      (⊩˒∷-idSubst (βŠ©α΅›β‡” .proj₁ ⊩A .proj₁))

opaque

  -- A lemma related to sgSubst.

  βŠ©Λ’β‰‘βˆ·-sgSubst :
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A β†’
    Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ A β†’
    Ξ“ ⊩˒ sgSubst t ≑ sgSubst u ∷ Ξ“ βˆ™ A
  βŠ©Λ’β‰‘βˆ·-sgSubst ⊩A t≑u =
    βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
      ( (_ , ⊩A)
      , (_ , PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (PE.sym $ subst-id _) t≑u)
      , refl-βŠ©Λ’β‰‘βˆ· (⊩˒∷-idSubst (wf-βŠ©α΅› ⊩A))
      )

opaque

  -- A lemma related to sgSubst.

  ⊩˒∷-sgSubst :
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A β†’
    Ξ“ ⊩⟨ l ⟩ t ∷ A β†’
    Ξ“ ⊩˒ sgSubst t ∷ Ξ“ βˆ™ A
  ⊩˒∷-sgSubst ⊩A =
    βŠ©Λ’βˆ·β‡”βŠ©Λ’β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©Λ’β‰‘βˆ·-sgSubst ⊩A βˆ˜β†’ βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .proj₁

------------------------------------------------------------------------
-- Reducibility from validity

opaque

  -- If there is a valid equality between A andΒ B, then there is a
  -- reducible equality between A andΒ B.

  βŠ©α΅›β‰‘β†’βŠ©β‰‘ : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’ Ξ“ ⊩⟨ l ⟩ A ≑ B
  βŠ©α΅›β‰‘β†’βŠ©β‰‘ {Ξ“} {l} {A} {B} =
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B                            β‡”βŸ¨ βŠ©α΅›β‰‘β‡”β€² βŸ©β†’

    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ—
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ B) Γ—
    (βˆ€ {m} {Ξ” : Con Term m} {Οƒ} β†’
     Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’ Ξ” ⊩⟨ l ⟩ A [ Οƒ ] ≑ B [ Οƒ ])  β†’βŸ¨ (Ξ» (⊩A , _ , A≑B) β†’ A≑B $ ⊩˒∷-idSubst $ wf-βŠ©α΅› ⊩A) ⟩

    Ξ“ ⊩⟨ l ⟩ A [ idSubst ] ≑ B [ idSubst ]     β‰‘βŸ¨ PE.congβ‚‚ (_⊩⟨_⟩_≑_ _ _) (subst-id _) (subst-id _) βŸ©β†’

    Ξ“ ⊩⟨ l ⟩ A ≑ B                             β–‘

opaque

  -- If A is valid, then A is reducible.

  βŠ©α΅›β†’βŠ© : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’ Ξ“ ⊩⟨ l ⟩ A
  βŠ©α΅›β†’βŠ© = βŠ©β‡”βŠ©β‰‘ .projβ‚‚ βˆ˜β†’ βŠ©α΅›β‰‘β†’βŠ©β‰‘ βˆ˜β†’ βŠ©α΅›β‡”βŠ©α΅›β‰‘ .proj₁

opaque

  -- If there is a valid equality between t andΒ u, then there is a
  -- reducible equality between t andΒ u.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ· : Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A β†’ Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ A
  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ· {Ξ“} {l} {t} {u} {A} =
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A                                     β‡”βŸ¨ βŠ©α΅›β‰‘βˆ·β‡”β€² βŸ©β†’

    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A) Γ—
    (Ξ“ βŠ©α΅›βŸ¨ l ⟩ u ∷ A) Γ—
    (βˆ€ {m} {Ξ” : Con Term m} {Οƒ} β†’
     Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’ Ξ” ⊩⟨ l ⟩ t [ Οƒ ] ≑ u [ Οƒ ] ∷ A [ Οƒ ])     β†’βŸ¨ (Ξ» (⊩t , _ , t≑u) β†’ t≑u $ ⊩˒∷-idSubst $ wf-βŠ©α΅› $ wf-βŠ©α΅›βˆ· ⊩t) ⟩

    Ξ“ ⊩⟨ l ⟩ t [ idSubst ] ≑ u [ idSubst ] ∷ A [ idSubst ]  β‰‘βŸ¨ PE.cong₃ (_⊩⟨_⟩_≑_∷_ _ _)
                                                                 (subst-id _) (subst-id _) (subst-id _) βŸ©β†’

    Ξ“ ⊩⟨ l ⟩ t ≑ u ∷ A                                      β–‘

opaque

  -- If t is valid, then t is reducible.

  βŠ©α΅›βˆ·β†’βŠ©βˆ· : Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’ Ξ“ ⊩⟨ l ⟩ t ∷ A
  βŠ©α΅›βˆ·β†’βŠ©βˆ· = βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ βˆ˜β†’ βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ· βˆ˜β†’ βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .proj₁

------------------------------------------------------------------------
-- Escape lemmas

opaque

  -- An escape lemma for _βŠ©α΅›βŸ¨_⟩_.

  escape-βŠ©α΅› : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’ Ξ“ ⊒ A
  escape-βŠ©α΅› = escape-⊩ βˆ˜β†’ βŠ©α΅›β†’βŠ©

opaque

  -- An escape lemma for βŠ©α΅›_.

  escape-βŠ©α΅›β€² : βŠ©α΅› Ξ“ β†’ ⊒ Ξ“
  escape-βŠ©α΅›β€² {Ξ“ = Ξ΅}     = Ξ» _ β†’ Ξ΅
  escape-βŠ©α΅›β€² {Ξ“ = _ βˆ™ _} = βŠ’β†’βŠ’βˆ™ βˆ˜β†’ escape-βŠ©α΅› βˆ˜β†’ projβ‚‚ βˆ˜β†’ βŠ©α΅›βˆ™β‡” .proj₁

opaque

  -- An escape lemma for _βŠ©α΅›βŸ¨_⟩_≑_.

  escape-βŠ©α΅›β‰‘ : Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’ Ξ“ ⊒ A β‰… B
  escape-βŠ©α΅›β‰‘ = escape-βŠ©β‰‘ βˆ˜β†’ βŠ©α΅›β‰‘β†’βŠ©β‰‘

opaque

  -- An escape lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  escape-βŠ©α΅›βˆ· : Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’ Ξ“ ⊒ t ∷ A
  escape-βŠ©α΅›βˆ· = escape-⊩∷ βˆ˜β†’ βŠ©α΅›βˆ·β†’βŠ©βˆ·

opaque

  -- An escape lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  escape-βŠ©α΅›β‰‘βˆ· : Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A β†’ Ξ“ ⊒ t β‰… u ∷ A
  escape-βŠ©α΅›β‰‘βˆ· = escape-βŠ©β‰‘βˆ· βˆ˜β†’ βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·

opaque

  -- An escape lemma for _⊩˒_∷_.

  escape-⊩˒∷ : Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’ ⊒ Ξ” Γ— Ξ” ⊒˒ Οƒ ∷ Ξ“
  escape-⊩˒∷ {Ξ”} {Οƒ} {Ξ“ = Ξ΅} =
    Ξ” ⊩˒ Οƒ ∷ Ξ΅        β‡”βŸ¨ βŠ©Λ’βˆ·Ξ΅β‡” βŸ©β†’
    ⊒ Ξ”               β†’βŸ¨ _, id ⟩
    ⊒ Ξ” Γ— Ξ” ⊒˒ Οƒ ∷ Ξ΅  β–‘
  escape-⊩˒∷ {Ξ”} {Οƒ} {Ξ“ = Ξ“ βˆ™ A} =
    Ξ” ⊩˒ Οƒ ∷ Ξ“ βˆ™ A                                              β‡”βŸ¨ βŠ©Λ’βˆ·βˆ™β‡” βŸ©β†’

    (βˆƒ Ξ» l β†’ (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ— Ξ” ⊩⟨ l ⟩ head Οƒ ∷ A [ tail Οƒ ]) Γ—
    Ξ” ⊩˒ tail Οƒ ∷ Ξ“                                             β†’βŸ¨ (Ξ» ((_ , _ , βŠ©Οƒβ‚€) , βŠ©Οƒβ‚Š) β†’
                                                                      escape-⊩∷ βŠ©Οƒβ‚€ , escape-⊩˒∷ βŠ©Οƒβ‚Š) ⟩

    Ξ” ⊒ head Οƒ ∷ A [ tail Οƒ ] Γ— ⊒ Ξ” Γ— Ξ” ⊒˒ tail Οƒ ∷ Ξ“           β†’βŸ¨ (Ξ» (βŠ’Οƒβ‚€ , βŠ’Ξ” , βŠ’Οƒβ‚Š) β†’ βŠ’Ξ” , (βŠ’Οƒβ‚Š , βŠ’Οƒβ‚€)) ⟩

    ⊒ Ξ” Γ— Ξ” ⊒˒ Οƒ ∷ Ξ“ βˆ™ A                                        β–‘

opaque

  -- An escape lemma for _⊩˒_≑_∷_.

  escape-βŠ©Λ’β‰‘βˆ· : Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’ ⊒ Ξ” Γ— Ξ” ⊒˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“
  escape-βŠ©Λ’β‰‘βˆ· {Ξ”} {σ₁} {Οƒβ‚‚} {Ξ“ = Ξ΅} =
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ΅        β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·Ξ΅β‡” βŸ©β†’
    ⊒ Ξ”                     β†’βŸ¨ _, id ⟩
    ⊒ Ξ” Γ— Ξ” ⊒˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ΅  β–‘
  escape-βŠ©Λ’β‰‘βˆ· {Ξ”} {σ₁} {Οƒβ‚‚} {Ξ“ = Ξ“ βˆ™ A} =
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A                                            β‡”βŸ¨ βŠ©Λ’β‰‘βˆ·βˆ™β‡” βŸ©β†’

    (βˆƒ Ξ» l β†’
     (Ξ“ βŠ©α΅›βŸ¨ l ⟩ A) Γ— Ξ” ⊩⟨ l ⟩ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]) Γ—
    Ξ” ⊩˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                                      β†’βŸ¨ (Ξ» ((_ , _ , σ₁₀≑σ₂₀) , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’
                                                                          β‰…β‚œ-eq (escape-βŠ©β‰‘βˆ· σ₁₀≑σ₂₀) , escape-βŠ©Λ’β‰‘βˆ· Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) ⟩
    Ξ” ⊒ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ] Γ—
    ⊒ Ξ” Γ— Ξ” ⊒˒ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ“                                β†’βŸ¨ (Ξ» (σ₁₀≑σ₂₀ , βŠ’Ξ” , Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) β†’ βŠ’Ξ” , (Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š , σ₁₀≑σ₂₀)) ⟩

    ⊒ Ξ” Γ— Ξ” ⊒˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ βˆ™ A                                      β–‘

------------------------------------------------------------------------
-- Embedding

opaque

  -- Embedding for _βŠ©α΅›βŸ¨_⟩_.

  emb-βŠ©α΅› :
    l ≀ lβ€² β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ A
  emb-βŠ©α΅› l≀lβ€² ⊩A =
    case βŠ©α΅›β‡” .proj₁ ⊩A of Ξ»
      (βŠ©Ξ“ , A≑A) β†’
    βŠ©α΅›β‡” .projβ‚‚ (βŠ©Ξ“ , emb-βŠ©β‰‘ l≀lβ€² βˆ˜β†’ A≑A)

opaque

  -- Embedding for _βŠ©α΅›βŸ¨_⟩_∷_.

  emb-βŠ©α΅›βˆ· :
    l ≀ lβ€² β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ∷ A
  emb-βŠ©α΅›βˆ· l≀lβ€² ⊩t =
    level-βŠ©α΅›βˆ· (emb-βŠ©α΅› l≀lβ€² (wf-βŠ©α΅›βˆ· ⊩t)) ⊩t

------------------------------------------------------------------------
-- Weakening

opaque

  -- A weakening lemma for _βŠ©α΅›βŸ¨_⟩_≑_.

  wk-βŠ©α΅›β‰‘ :
    ρ ∷ Ξ” βŠ‡ Ξ“ β†’ βŠ©α΅› Ξ” β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’ Ξ” βŠ©α΅›βŸ¨ l ⟩ wk ρ A ≑ wk ρ B
  wk-βŠ©α΅›β‰‘ {ρ} {A} {B} ΟβŠ‡ βŠ©Ξ” A≑B =
    case βŠ©α΅›β‰‘β‡” .proj₁ A≑B of Ξ»
      (βŠ©Ξ“ , A≑B) β†’
    βŠ©α΅›β‰‘β‡” .projβ‚‚
      ( βŠ©Ξ”
      , Ξ» {_ _} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} σ₁≑σ₂ β†’
          wk ρ A [ σ₁ ]  β‰‘βŸ¨ subst-wk A βŸ©βŠ©β‰‘
          A [ σ₁ β‚›β€’ ρ ]  β‰‘βŸ¨ A≑B $ βŠ©Λ’β‰‘βˆ·-β‚›β€’ ΟβŠ‡ βŠ©Ξ“ σ₁≑σ₂ βŸ©βŠ©βˆŽβ‰‘
          B [ Οƒβ‚‚ β‚›β€’ ρ ]  β‰‘Λ˜βŸ¨ subst-wk B ⟩
          wk ρ B [ Οƒβ‚‚ ]  ∎
      )

opaque

  -- Single-step weakening for _βŠ©α΅›βŸ¨_⟩_≑_.

  wk1-βŠ©α΅›β‰‘ : Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ C β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A ≑ B β†’ Ξ“ βˆ™ C βŠ©α΅›βŸ¨ l ⟩ wk1 A ≑ wk1 B
  wk1-βŠ©α΅›β‰‘ ⊩C =
    wk-βŠ©α΅›β‰‘ (TW.step TW.id) (βŠ©α΅›-βˆ™-intro ⊩C)

opaque

  -- A weakening lemma for _βŠ©α΅›βŸ¨_⟩_.

  wk-βŠ©α΅› : ρ ∷ Ξ” βŠ‡ Ξ“ β†’ βŠ©α΅› Ξ” β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’ Ξ” βŠ©α΅›βŸ¨ l ⟩ wk ρ A
  wk-βŠ©α΅› ΟβŠ‡ βŠ©Ξ” =
    βŠ©α΅›β‡”βŠ©α΅›β‰‘ .projβ‚‚ βˆ˜β†’ wk-βŠ©α΅›β‰‘ ΟβŠ‡ βŠ©Ξ” βˆ˜β†’ βŠ©α΅›β‡”βŠ©α΅›β‰‘ .proj₁

opaque

  -- Single-step weakening for _βŠ©α΅›βŸ¨_⟩_.

  wk1-βŠ©α΅› : Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ B β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ A β†’ Ξ“ βˆ™ B βŠ©α΅›βŸ¨ l ⟩ wk1 A
  wk1-βŠ©α΅› ⊩B =
    wk-βŠ©α΅› (TW.step TW.id) (βŠ©α΅›-βˆ™-intro ⊩B)

opaque

  -- A weakening lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  wk-βŠ©α΅›β‰‘βˆ· :
    ρ ∷ Ξ” βŠ‡ Ξ“ β†’ βŠ©α΅› Ξ” β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A β†’
    Ξ” βŠ©α΅›βŸ¨ l ⟩ wk ρ t ≑ wk ρ u ∷ wk ρ A
  wk-βŠ©α΅›β‰‘βˆ· {ρ} {t} {u} {A} ΟβŠ‡ βŠ©Ξ” t≑u =
    case wf-βŠ©α΅›βˆ· $ wf-βŠ©α΅›β‰‘βˆ· t≑u .proj₁ of Ξ»
      ⊩A β†’
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( wk-βŠ©α΅› ΟβŠ‡ βŠ©Ξ” ⊩A
      , Ξ» {_ _} {σ₁ = σ₁} {Οƒβ‚‚ = Οƒβ‚‚} σ₁≑σ₂ β†’
          wk ρ t [ σ₁ ] ∷ wk ρ A [ σ₁ ]  β‰‘βŸ¨ subst-wk t βŸ©βŠ©βˆ·βˆ·β‰‘
                                          ⟨ subst-wk A βŸ©βŠ©βˆ·β‰‘
          t [ σ₁ β‚›β€’ ρ ] ∷ A [ σ₁ β‚›β€’ ρ ]  β‰‘βŸ¨ βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚ $
                                            βŠ©Λ’β‰‘βˆ·-β‚›β€’ ΟβŠ‡ (wf-βŠ©α΅› ⊩A) σ₁≑σ₂ βŸ©βŠ©βˆ·βˆŽβˆ·β‰‘
          u [ Οƒβ‚‚ β‚›β€’ ρ ]                  β‰‘Λ˜βŸ¨ subst-wk u ⟩
          wk ρ u [ Οƒβ‚‚ ]                  ∎
      )

opaque

  -- Single-step weakening for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  wk1-βŠ©α΅›β‰‘βˆ· :
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ B β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ A β†’
    Ξ“ βˆ™ B βŠ©α΅›βŸ¨ l ⟩ wk1 t ≑ wk1 u ∷ wk1 A
  wk1-βŠ©α΅›β‰‘βˆ· ⊩B =
    wk-βŠ©α΅›β‰‘βˆ· (TW.step TW.id) (βŠ©α΅›-βˆ™-intro ⊩B)

opaque

  -- A weakening lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  wk-βŠ©α΅›βˆ· :
    ρ ∷ Ξ” βŠ‡ Ξ“ β†’ βŠ©α΅› Ξ” β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’ Ξ” βŠ©α΅›βŸ¨ l ⟩ wk ρ t ∷ wk ρ A
  wk-βŠ©α΅›βˆ· ΟβŠ‡ βŠ©Ξ” =
    βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ βˆ˜β†’ wk-βŠ©α΅›β‰‘βˆ· ΟβŠ‡ βŠ©Ξ” βˆ˜β†’ βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .proj₁

opaque

  -- Single-step weakening for _βŠ©α΅›βŸ¨_⟩_∷_.

  wk1-βŠ©α΅›βˆ· : Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ B β†’ Ξ“ βŠ©α΅›βŸ¨ l ⟩ t ∷ A β†’ Ξ“ βˆ™ B βŠ©α΅›βŸ¨ l ⟩ wk1 t ∷ wk1 A
  wk1-βŠ©α΅›βˆ· ⊩B =
    wk-βŠ©α΅›βˆ· (TW.step TW.id) (βŠ©α΅›-βˆ™-intro ⊩B)

------------------------------------------------------------------------
-- Substitution lemmas

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₀≑[]β‚€ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B ≑ C β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ≑ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ B [ t ]β‚€ ≑ C [ u ]β‚€
  βŠ©α΅›β‰‘β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₀≑[]β‚€ {B} {C} B≑C t≑u =
    case βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u of Ξ»
      (⊩A , t≑u) β†’
    βŠ©α΅›β‰‘β‡” .projβ‚‚
      ( wf-βŠ©α΅› ⊩A
      , Ξ» σ₁≑σ₂ β†’
          PE.substβ‚‚ (_⊩⟨_⟩_≑_ _ _) (substConsId B) (substConsId C) $
          βŠ©α΅›β‰‘β‡” .proj₁ B≑C .projβ‚‚ $
          βŠ©Λ’β‰‘βˆ·βˆ™β‡” .projβ‚‚ ((_ , ⊩A , t≑u σ₁≑σ₂) , σ₁≑σ₂)
      )

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_.

  βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚€ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ t ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ B [ t ]β‚€
  βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚€ ⊩B ⊩t =
    βŠ©α΅›β‡”βŠ©α΅›β‰‘ .projβ‚‚ $ βŠ©α΅›β‰‘β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₀≑[]β‚€ (refl-βŠ©α΅›β‰‘ ⊩B) (refl-βŠ©α΅›β‰‘βˆ· ⊩t)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚€βˆ· :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ B β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t [ u ]β‚€ ∷ B [ u ]β‚€
  βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚€βˆ· {t} {B} ⊩t ⊩u =
    case βŠ©α΅›βˆ·β‡” .proj₁ ⊩t of Ξ»
      (⊩B , t≑t) β†’
    βŠ©α΅›βˆ·β‡” .projβ‚‚
      ( βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚€ ⊩B ⊩u
      , Ξ» σ₁≑σ₂ β†’
          PE.subst₃ (_⊩⟨_⟩_≑_∷_ _ _)
            (substConsId t) (substConsId t) (substConsId B) $
          t≑t $
          βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
            ( wf-βˆ™-βŠ©α΅› ⊩B
            , (_ , βŠ©α΅›βˆ·β‡” .proj₁ ⊩u .projβ‚‚ σ₁≑σ₂)
            , σ₁≑σ₂
            )
      )

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₁₀≑[]₁₀ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C₁ ≑ Cβ‚‚ β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€³ ⟩ t₁ ≑ tβ‚‚ ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l‴ ⟩ u₁ ≑ uβ‚‚ ∷ B [ t₁ ]β‚€ β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ C₁ [ t₁ , u₁ ]₁₀ ≑ Cβ‚‚ [ tβ‚‚ , uβ‚‚ ]₁₀
  βŠ©α΅›β‰‘β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₁₀≑[]₁₀ {B} {C₁} {Cβ‚‚} C₁≑Cβ‚‚ t₁≑tβ‚‚ u₁≑uβ‚‚ =
    case βŠ©α΅›β‰‘β‡” .proj₁ C₁≑Cβ‚‚ of Ξ»
      (βŠ©Ξ“βˆ™Aβˆ™B , C₁≑Cβ‚‚) β†’
    case wf-βŠ©α΅›-βˆ™ βŠ©Ξ“βˆ™Aβˆ™B of Ξ»
      (_ , ⊩B) β†’
    case wf-βˆ™-βŠ©α΅› ⊩B of Ξ»
      (_ , ⊩A) β†’
    βŠ©α΅›β‰‘β‡” .projβ‚‚
      ( wf-βŠ©α΅› ⊩A
      , Ξ» σ₁≑σ₂ β†’
          PE.substβ‚‚ (_⊩⟨_⟩_≑_ _ _)
            (PE.sym $ [,]-[]-fusion C₁) (PE.sym $ [,]-[]-fusion Cβ‚‚) $
          C₁≑Cβ‚‚ $
          βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
            ( (_ , ⊩B)
            , ( _
              , PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (PE.sym $ substConsId B)
                  (βŠ©α΅›β‰‘βˆ·β‡” .proj₁ u₁≑uβ‚‚ .projβ‚‚ σ₁≑σ₂)
              )
            , βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
                ( (_ , ⊩A)
                , (_ , βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t₁≑tβ‚‚ .projβ‚‚ σ₁≑σ₂)
                , σ₁≑σ₂
                )
            )
      )

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_.

  βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]₁₀ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€³ ⟩ t ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l‴ ⟩ u ∷ B [ t ]β‚€ β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ C [ t , u ]₁₀
  βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]₁₀ ⊩C ⊩t ⊩u =
    βŠ©α΅›β‡”βŠ©α΅›β‰‘ .projβ‚‚ $
    βŠ©α΅›β‰‘β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₁₀≑[]₁₀
      (refl-βŠ©α΅›β‰‘ ⊩C) (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©α΅›β‰‘βˆ· ⊩u)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₁₀≑[]β‚β‚€βˆ· :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ C β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€³ ⟩ u₁ ≑ uβ‚‚ ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ l‴ ⟩ v₁ ≑ vβ‚‚ ∷ B [ u₁ ]β‚€ β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t₁ [ u₁ , v₁ ]₁₀ ≑ tβ‚‚ [ uβ‚‚ , vβ‚‚ ]₁₀ ∷ C [ u₁ , v₁ ]₁₀
  βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₁₀≑[]β‚β‚€βˆ· {B} {t₁} {tβ‚‚} {C} t₁≑tβ‚‚ u₁≑uβ‚‚ v₁≑vβ‚‚ =
    case wf-βŠ©α΅›βˆ· $ wf-βŠ©α΅›β‰‘βˆ· t₁≑tβ‚‚ .proj₁ of Ξ»
      ⊩C β†’
    case wf-βˆ™-βŠ©α΅› ⊩C of Ξ»
      (_ , ⊩B) β†’
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]₁₀
          ⊩C (wf-βŠ©α΅›β‰‘βˆ· u₁≑uβ‚‚ .proj₁) (wf-βŠ©α΅›β‰‘βˆ· v₁≑vβ‚‚ .proj₁)
      , Ξ» σ₁≑σ₂ β†’
          PE.subst₃ (_⊩⟨_⟩_≑_∷_ _ _) (PE.sym $ [,]-[]-fusion t₁)
            (PE.sym $ [,]-[]-fusion tβ‚‚) (PE.sym $ [,]-[]-fusion C) $
          βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t₁≑tβ‚‚ .projβ‚‚ $
          βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
            ( (_ , ⊩B)
            , ( _
              , (PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _)
                   (PE.sym $ substConsId B) $
                 βŠ©α΅›β‰‘βˆ·β‡” .proj₁ v₁≑vβ‚‚ .projβ‚‚ σ₁≑σ₂)
              )
            , βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
                ( wf-βˆ™-βŠ©α΅› ⊩B
                , (_ , βŠ©α΅›β‰‘βˆ·β‡” .proj₁ u₁≑uβ‚‚ .projβ‚‚ σ₁≑σ₂)
                , σ₁≑σ₂
                )
            )

      )

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚β‚€βˆ· :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t ∷ C β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€² ⟩ u ∷ A β†’
    Ξ“ βŠ©α΅›βŸ¨ lβ€³ ⟩ v ∷ B [ u ]β‚€ β†’
    Ξ“ βŠ©α΅›βŸ¨ l ⟩ t [ u , v ]₁₀ ∷ C [ u , v ]₁₀
  βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β‚β‚€βˆ· ⊩t ⊩u ⊩v =
    βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›[]₁₀≑[]β‚β‚€βˆ·
      (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©α΅›β‰‘βˆ· ⊩u) (refl-βŠ©α΅›β‰‘βˆ· ⊩v)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑²≑[]↑² :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ D ≑ E β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ lβ€² ⟩ t ∷ wk2 A β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ l ⟩ D [ t ]↑² ≑ E [ t ]↑²
  βŠ©α΅›β‰‘β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑²≑[]↑² {A} {D} {E} D≑E ⊩t =
    case βŠ©α΅›β‰‘β‡” .proj₁ D≑E of Ξ»
      (βŠ©Ξ“βˆ™A , D≑E) β†’
    βŠ©α΅›β‰‘β‡” .projβ‚‚
      ( wf-βŠ©α΅› (wf-βŠ©α΅›βˆ· ⊩t)
      , Ξ» σ₁≑σ₂ β†’
          PE.substβ‚‚ (_⊩⟨_⟩_≑_ _ _) (substComp↑² D _) (substComp↑² E _) $
          D≑E $
          βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
            ( wf-βŠ©α΅›-βˆ™ βŠ©Ξ“βˆ™A
            , ( _
              , PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (wk2-tail A)
                  (βŠ©α΅›βˆ·β‡” .proj₁ ⊩t .projβ‚‚ σ₁≑σ₂)
              )
            , βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ (βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₁≑σ₂ .projβ‚‚) .projβ‚‚
            )
      )

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_.

  βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑² :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ D β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ lβ€² ⟩ t ∷ wk2 A β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ l ⟩ D [ t ]↑²
  βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑² ⊩D ⊩t =
    βŠ©α΅›β‡”βŠ©α΅›β‰‘ .projβ‚‚ $ βŠ©α΅›β‰‘β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑²≑[]↑² (refl-βŠ©α΅›β‰‘ ⊩D) ⊩t

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑²≑[]β†‘Β²βˆ· :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ D β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ lβ€² ⟩ v ∷ wk2 A β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ l ⟩ t [ v ]↑² ≑ u [ v ]↑² ∷ D [ v ]↑²
  βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑²≑[]β†‘Β²βˆ· {A} {t} {u} {D} t≑u ⊩v =
    case wf-βŠ©α΅›βˆ· (wf-βŠ©α΅›β‰‘βˆ· t≑u .proj₁) of Ξ»
      ⊩D β†’
    βŠ©α΅›β‰‘βˆ·β‡” .projβ‚‚
      ( βŠ©α΅›β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑² ⊩D ⊩v
      , Ξ» σ₁≑σ₂ β†’
          PE.subst₃ (_⊩⟨_⟩_≑_∷_ _ _) (substComp↑² t _) (substComp↑² u _)
            (substComp↑² D _) $
          βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚ $
          βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
            ( wf-βˆ™-βŠ©α΅› ⊩D
            , ( _
              , PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (wk2-tail A)
                  (βŠ©α΅›βˆ·β‡” .proj₁ ⊩v .projβ‚‚ σ₁≑σ₂)
              )
            , βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ (βŠ©Λ’β‰‘βˆ·βˆ™β‡” .proj₁ σ₁≑σ₂ .projβ‚‚) .projβ‚‚
            )
      )

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β†‘Β²βˆ· :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ D β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ lβ€² ⟩ u ∷ wk2 A β†’
    Ξ“ βˆ™ B βˆ™ C βŠ©α΅›βŸ¨ l ⟩ t [ u ]↑² ∷ D [ u ]↑²
  βŠ©α΅›βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]β†‘Β²βˆ· ⊩t ⊩u =
    βŠ©α΅›βˆ·β‡”βŠ©α΅›β‰‘βˆ· .projβ‚‚ $ βŠ©α΅›β‰‘βˆ·β†’βŠ©α΅›βˆ·β†’βŠ©α΅›[]↑²≑[]β†‘Β²βˆ· (refl-βŠ©α΅›β‰‘βˆ· ⊩t) ⊩u

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©[]₀≑[]β‚€ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B ≑ C β†’
    Ξ“ ⊩⟨ lβ€² ⟩ t ≑ u ∷ A β†’
    Ξ“ ⊩⟨ l ⟩ B [ t ]β‚€ ≑ C [ u ]β‚€
  βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©[]₀≑[]β‚€ B≑C t≑u =
    case wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›β‰‘ B≑C .proj₁) of Ξ»
      (_ , ⊩A) β†’
    βŠ©α΅›β‰‘β‡” .proj₁ B≑C .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·-sgSubst ⊩A (level-βŠ©β‰‘βˆ· (βŠ©α΅›β†’βŠ© ⊩A) t≑u)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©βˆ·β†’βŠ©[]β‚€ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B β†’
    Ξ“ ⊩⟨ lβ€² ⟩ t ∷ A β†’
    Ξ“ ⊩⟨ l ⟩ B [ t ]β‚€
  βŠ©α΅›β†’βŠ©βˆ·β†’βŠ©[]β‚€ ⊩B ⊩t =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $ βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©[]₀≑[]β‚€ (refl-βŠ©α΅›β‰‘ ⊩B) (refl-βŠ©β‰‘βˆ· ⊩t)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[]₀≑[]β‚€βˆ· :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ≑ u ∷ B β†’
    Ξ“ ⊩⟨ lβ€² ⟩ v ≑ w ∷ A β†’
    Ξ“ ⊩⟨ l ⟩ t [ v ]β‚€ ≑ u [ w ]β‚€ ∷ B [ v ]β‚€
  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[]₀≑[]β‚€βˆ· t≑u v≑w =
    case wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›βˆ· (wf-βŠ©α΅›β‰‘βˆ· t≑u .proj₁)) of Ξ»
      (_ , ⊩A) β†’
    βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t≑u .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·-sgSubst ⊩A (level-βŠ©β‰‘βˆ· (βŠ©α΅›β†’βŠ© ⊩A) v≑w)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©βˆ·β†’βŠ©[]β‚€βˆ· :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ B β†’
    Ξ“ ⊩⟨ lβ€² ⟩ u ∷ A β†’
    Ξ“ ⊩⟨ l ⟩ t [ u ]β‚€ ∷ B [ u ]β‚€
  βŠ©α΅›βˆ·β†’βŠ©βˆ·β†’βŠ©[]β‚€βˆ· ⊩t ⊩u =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $ βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[]₀≑[]β‚€βˆ· (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©β‰‘βˆ· ⊩u)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,] :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B₁ ≑ Bβ‚‚ β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t₁ ≑ tβ‚‚ ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ l ⟩ B₁ [ consSubst σ₁ t₁ ] ≑ Bβ‚‚ [ consSubst Οƒβ‚‚ tβ‚‚ ]
  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,] B₁≑Bβ‚‚ σ₁≑σ₂ t₁≑tβ‚‚ =
    βŠ©α΅›β‰‘β‡” .proj₁ B₁≑Bβ‚‚ .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚ (wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›β‰‘ B₁≑Bβ‚‚ .proj₁) , (_ , t₁≑tβ‚‚) , σ₁≑σ₂)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[,] :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ l ⟩ B [ consSubst Οƒ t ]
  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[,] ⊩B βŠ©Οƒ ⊩t =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $
    βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,] (refl-βŠ©α΅›β‰‘ ⊩B) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ) (refl-βŠ©β‰‘βˆ· ⊩t)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,]∷ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ B β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ u₁ ≑ uβ‚‚ ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ l ⟩ t₁ [ consSubst σ₁ u₁ ] ≑ tβ‚‚ [ consSubst Οƒβ‚‚ uβ‚‚ ] ∷
      B [ consSubst σ₁ u₁ ]
  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,]∷ t₁≑tβ‚‚ σ₁≑σ₂ u₁≑uβ‚‚ =
    βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t₁≑tβ‚‚ .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
      (wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›βˆ· $ wf-βŠ©α΅›β‰‘βˆ· t₁≑tβ‚‚ .proj₁) , (_ , u₁≑uβ‚‚) , σ₁≑σ₂)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[,]∷ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ B β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ u ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ l ⟩ t [ consSubst Οƒ u ] ∷ B [ consSubst Οƒ u ]
  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[,]∷ ⊩t βŠ©Οƒ ⊩u =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,]∷ (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ) (refl-βŠ©β‰‘βˆ· ⊩u)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑] :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B₁ ≑ Bβ‚‚ β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ σ₁ ] ⊩⟨ l ⟩ B₁ [ σ₁ ⇑ ] ≑ Bβ‚‚ [ Οƒβ‚‚ ⇑ ]
  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑] B₁≑Bβ‚‚ σ₁≑σ₂ =
    βŠ©α΅›β‰‘β‡” .proj₁ B₁≑Bβ‚‚ .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·-liftSubst (wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›β‰‘ B₁≑Bβ‚‚ .proj₁) .projβ‚‚) σ₁≑σ₂

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[⇑] :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ Οƒ ] ⊩⟨ l ⟩ B [ Οƒ ⇑ ]
  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[⇑] ⊩B βŠ©Οƒ =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $ βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑] (refl-βŠ©α΅›β‰‘ ⊩B) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑]∷ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ B β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ σ₁ ] ⊩⟨ l ⟩ t₁ [ σ₁ ⇑ ] ≑ tβ‚‚ [ Οƒβ‚‚ ⇑ ] ∷ B [ σ₁ ⇑ ]
  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑]∷ t₁≑tβ‚‚ σ₁≑σ₂ =
    βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t₁≑tβ‚‚ .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·-liftSubst (wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›βˆ· (wf-βŠ©α΅›β‰‘βˆ· t₁≑tβ‚‚ .proj₁)) .projβ‚‚)
      σ₁≑σ₂

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[⇑]∷ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ B β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ Οƒ ] ⊩⟨ l ⟩ t [ Οƒ ⇑ ] ∷ B [ Οƒ ⇑ ]
  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[⇑]∷ ⊩t βŠ©Οƒ =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $ βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑]≑[⇑]∷ (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑] :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C₁ ≑ Cβ‚‚ β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ σ₁ ] βˆ™ B [ σ₁ ⇑ ] ⊩⟨ l ⟩ C₁ [ σ₁ ⇑ ⇑ ] ≑ Cβ‚‚ [ Οƒβ‚‚ ⇑ ⇑ ]
  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑] C₁≑Cβ‚‚ σ₁≑σ₂ =
    case wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›β‰‘ C₁≑Cβ‚‚ .proj₁) of Ξ»
      (_ , ⊩B) β†’
    βŠ©α΅›β‰‘β‡” .proj₁ C₁≑Cβ‚‚ .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·-liftSubst ⊩B $ βŠ©Λ’β‰‘βˆ·-liftSubst (wf-βˆ™-βŠ©α΅› ⊩B .projβ‚‚) σ₁≑σ₂

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[⇑⇑] :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ Οƒ ] βˆ™ B [ Οƒ ⇑ ] ⊩⟨ l ⟩ C [ Οƒ ⇑ ⇑ ]
  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©[⇑⇑] ⊩C βŠ©Οƒ =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $ βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑] (refl-βŠ©α΅›β‰‘ ⊩C) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑]∷ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ C β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ σ₁ ] βˆ™ B [ σ₁ ⇑ ] ⊩⟨ l ⟩ t₁ [ σ₁ ⇑ ⇑ ] ≑ tβ‚‚ [ Οƒβ‚‚ ⇑ ⇑ ] ∷
      C [ σ₁ ⇑ ⇑ ]
  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑]∷ t₁≑tβ‚‚ σ₁≑σ₂ =
    case wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›βˆ· (wf-βŠ©α΅›β‰‘βˆ· t₁≑tβ‚‚ .proj₁)) of Ξ»
      (_ , ⊩B) β†’
    βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t₁≑tβ‚‚ .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·-liftSubst ⊩B $ βŠ©Λ’β‰‘βˆ·-liftSubst (wf-βˆ™-βŠ©α΅› ⊩B .projβ‚‚) σ₁≑σ₂

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[⇑⇑]∷ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t ∷ C β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” βˆ™ A [ Οƒ ] βˆ™ B [ Οƒ ⇑ ] ⊩⟨ l ⟩ t [ Οƒ ⇑ ⇑ ] ∷ C [ Οƒ ⇑ ⇑ ]
  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[⇑⇑]∷ ⊩t βŠ©Οƒ =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $ βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[⇑⇑]≑[⇑⇑]∷ (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B₁ ≑ Bβ‚‚ β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t₁ ≑ tβ‚‚ ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ l ⟩ B₁ [ σ₁ ⇑ ] [ t₁ ]β‚€ ≑ Bβ‚‚ [ Οƒβ‚‚ ⇑ ] [ tβ‚‚ ]β‚€
  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ {B₁} {Bβ‚‚} B₁≑Bβ‚‚ σ₁≑σ₂ t₁≑tβ‚‚ =
    PE.substβ‚‚ (_⊩⟨_⟩_≑_ _ _)
      (PE.sym $ singleSubstComp _ _ B₁)
      (PE.sym $ singleSubstComp _ _ Bβ‚‚) $
    βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,] B₁≑Bβ‚‚ σ₁≑σ₂ t₁≑tβ‚‚

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑][]β‚€ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ l ⟩ B [ Οƒ ⇑ ] [ t ]β‚€
  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑][]β‚€ ⊩B βŠ©Οƒ ⊩t =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $
    βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ (refl-βŠ©α΅›β‰‘ ⊩B) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)
      (refl-βŠ©β‰‘βˆ· ⊩t)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€βˆ· :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ B β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ u₁ ≑ uβ‚‚ ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ l ⟩ t₁ [ σ₁ ⇑ ] [ u₁ ]β‚€ ≑ tβ‚‚ [ Οƒβ‚‚ ⇑ ] [ uβ‚‚ ]β‚€ ∷
      B [ σ₁ ⇑ ] [ u₁ ]β‚€
  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€βˆ· {t₁} {tβ‚‚} {B} t₁≑tβ‚‚ σ₁≑σ₂ u₁≑uβ‚‚ =
    PE.subst₃ (_⊩⟨_⟩_≑_∷_ _ _)
      (PE.sym $ singleSubstComp _ _ t₁)
      (PE.sym $ singleSubstComp _ _ tβ‚‚)
      (PE.sym $ singleSubstComp _ _ B) $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,]∷ t₁≑tβ‚‚ σ₁≑σ₂ u₁≑uβ‚‚

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑][]β‚€βˆ· :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ B β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ u ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ l ⟩ t [ Οƒ ⇑ ] [ u ]β‚€ ∷ B [ Οƒ ⇑ ] [ u ]β‚€
  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑][]β‚€βˆ· ⊩t βŠ©Οƒ ⊩u =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€βˆ· (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)
      (refl-βŠ©β‰‘βˆ· ⊩u)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]β‚€[]≑[]β‚€[] :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B₁ ≑ Bβ‚‚ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t₁ [ σ₁ ] ≑ tβ‚‚ [ Οƒβ‚‚ ] ∷ A [ σ₁ ] β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ B₁ [ t₁ ]β‚€ [ σ₁ ] ≑ Bβ‚‚ [ tβ‚‚ ]β‚€ [ Οƒβ‚‚ ]
  βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]β‚€[]≑[]β‚€[] {B₁} {Bβ‚‚} B₁≑Bβ‚‚ t₁[σ₁]≑tβ‚‚[Οƒβ‚‚] σ₁≑σ₂ =
    PE.substβ‚‚ (_⊩⟨_⟩_≑_ _ _)
      (PE.sym $ singleSubstLift B₁ _)
      (PE.sym $ singleSubstLift Bβ‚‚ _) $
    βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€ B₁≑Bβ‚‚ σ₁≑σ₂ t₁[σ₁]≑tβ‚‚[Οƒβ‚‚]

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]β‚€[] :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ B β†’
    Ξ” ⊩⟨ lβ€² ⟩ t [ Οƒ ] ∷ A [ Οƒ ] β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ B [ t ]β‚€ [ Οƒ ]
  βŠ©α΅›β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]β‚€[] {t} ⊩B ⊩t[Οƒ] βŠ©Οƒ =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $
    βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]β‚€[]≑[]β‚€[] {tβ‚‚ = t} (refl-βŠ©α΅›β‰‘ ⊩B) (refl-βŠ©β‰‘βˆ· ⊩t[Οƒ])
      (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]β‚€[]≑[]β‚€[]∷ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ B β†’
    Ξ” ⊩⟨ lβ€² ⟩ u₁ [ σ₁ ] ≑ uβ‚‚ [ Οƒβ‚‚ ] ∷ A [ σ₁ ] β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ t₁ [ u₁ ]β‚€ [ σ₁ ] ≑ tβ‚‚ [ uβ‚‚ ]β‚€ [ Οƒβ‚‚ ] ∷ B [ u₁ ]β‚€ [ σ₁ ]
  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]β‚€[]≑[]β‚€[]∷ {t₁} {tβ‚‚} {B} t₁≑tβ‚‚ σ₁≑σ₂ u₁[σ₁]≑uβ‚‚[Οƒβ‚‚] =
    PE.subst₃ (_⊩⟨_⟩_≑_∷_ _ _) (PE.sym $ singleSubstLift t₁ _)
      (PE.sym $ singleSubstLift tβ‚‚ _) (PE.sym $ singleSubstLift B _) $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑][]₀≑[⇑][]β‚€βˆ· t₁≑tβ‚‚ u₁[σ₁]≑uβ‚‚[Οƒβ‚‚] σ₁≑σ₂

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]β‚€[]∷ :
    Ξ“ βˆ™ A βŠ©α΅›βŸ¨ l ⟩ t ∷ B β†’
    Ξ” ⊩⟨ lβ€² ⟩ u [ Οƒ ] ∷ A [ Οƒ ] β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ t [ u ]β‚€ [ Οƒ ] ∷ B [ u ]β‚€ [ Οƒ ]
  βŠ©α΅›βˆ·β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]β‚€[]∷ {u} ⊩t ⊩u[Οƒ] βŠ©Οƒ =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]β‚€[]≑[]β‚€[]∷ {uβ‚‚ = u} (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©β‰‘βˆ· ⊩u[Οƒ])
      (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]₁₀ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C₁ ≑ Cβ‚‚ β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t₁ ≑ tβ‚‚ ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ u₁ ≑ uβ‚‚ ∷ B [ σ₁ ⇑ ] [ t₁ ]β‚€ β†’
    Ξ” ⊩⟨ l ⟩ C₁ [ σ₁ ⇑ ⇑ ] [ t₁ , u₁ ]₁₀ ≑ Cβ‚‚ [ Οƒβ‚‚ ⇑ ⇑ ] [ tβ‚‚ , uβ‚‚ ]₁₀
  βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]₁₀
    {B} {C₁} {Cβ‚‚} C₁≑Cβ‚‚ σ₁≑σ₂ t₁≑tβ‚‚ u₁≑uβ‚‚ =
    PE.substβ‚‚ (_⊩⟨_⟩_≑_ _ _)
      (PE.sym $ doubleSubstComp C₁ _ _ _)
      (PE.sym $ doubleSubstComp Cβ‚‚ _ _ _) $
    βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[,]≑[,] C₁≑Cβ‚‚
      (βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
         ( wf-βˆ™-βŠ©α΅› (wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›β‰‘ C₁≑Cβ‚‚ .proj₁) .projβ‚‚)
         , (_ , t₁≑tβ‚‚)
         , σ₁≑σ₂
         )) $
    PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (singleSubstComp _ _ B) u₁≑uβ‚‚

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑⇑][]₁₀ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ u ∷ B [ Οƒ ⇑ ] [ t ]β‚€ β†’
    Ξ” ⊩⟨ l ⟩ C [ Οƒ ⇑ ⇑ ] [ t , u ]₁₀
  βŠ©α΅›β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑⇑][]₁₀ ⊩C βŠ©Οƒ ⊩t ⊩u =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $
    βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]₁₀ (refl-βŠ©α΅›β‰‘ ⊩C) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)
      (refl-βŠ©β‰‘βˆ· ⊩t) (refl-βŠ©β‰‘βˆ· ⊩u)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]β‚β‚€βˆ· :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ C β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ u₁ ≑ uβ‚‚ ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ v₁ ≑ vβ‚‚ ∷ B [ σ₁ ⇑ ] [ u₁ ]β‚€ β†’
    Ξ” ⊩⟨ l ⟩ t₁ [ σ₁ ⇑ ⇑ ] [ u₁ , v₁ ]₁₀ ≑ tβ‚‚ [ Οƒβ‚‚ ⇑ ⇑ ] [ uβ‚‚ , vβ‚‚ ]₁₀ ∷
      C [ σ₁ ⇑ ⇑ ] [ u₁ , v₁ ]₁₀
  βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]β‚β‚€βˆ·
    {B} {t₁} {tβ‚‚} {C} t₁≑tβ‚‚ σ₁≑σ₂ u₁≑uβ‚‚ v₁≑vβ‚‚ =
    case wf-βˆ™-βŠ©α΅› (wf-βŠ©α΅›βˆ· (wf-βŠ©α΅›β‰‘βˆ· t₁≑tβ‚‚ .proj₁)) of Ξ»
      (_ , ⊩B) β†’
    PE.subst₃ (_⊩⟨_⟩_≑_∷_ _ _)
      (PE.sym $ doubleSubstComp t₁ _ _ _)
      (PE.sym $ doubleSubstComp tβ‚‚ _ _ _)
      (PE.sym $ doubleSubstComp C _ _ _) $
    βŠ©α΅›β‰‘βˆ·β‡” .proj₁ t₁≑tβ‚‚ .projβ‚‚ $
    βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚
      ( (_ , ⊩B)
      , ( _
        , PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (singleSubstComp _ _ B) v₁≑vβ‚‚
        )
      , βŠ©Λ’β‰‘βˆ·βˆ™β‡”β€² .projβ‚‚ (wf-βˆ™-βŠ©α΅› ⊩B , (_ , u₁≑uβ‚‚) , σ₁≑σ₂)
      )

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑⇑][]β‚β‚€βˆ· :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t ∷ C β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ lβ€² ⟩ u ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ v ∷ B [ Οƒ ⇑ ] [ u ]β‚€ β†’
    Ξ” ⊩⟨ l ⟩ t [ Οƒ ⇑ ⇑ ] [ u , v ]₁₀ ∷ C [ Οƒ ⇑ ⇑ ] [ u , v ]₁₀
  βŠ©α΅›βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©βˆ·β†’βŠ©βˆ·β†’βŠ©[⇑⇑][]β‚β‚€βˆ· ⊩t βŠ©Οƒ ⊩u ⊩v =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]β‚β‚€βˆ· (refl-βŠ©α΅›β‰‘βˆ· ⊩t) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)
      (refl-βŠ©β‰‘βˆ· ⊩u) (refl-βŠ©β‰‘βˆ· ⊩v)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_ and _⊩⟨_⟩_≑_.

  βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]₁₀[]≑[]₁₀[] :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C₁ ≑ Cβ‚‚ β†’
    Ξ” ⊩⟨ lβ€² ⟩ t₁ [ σ₁ ] ≑ tβ‚‚ [ Οƒβ‚‚ ] ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ u₁ [ σ₁ ] ≑ uβ‚‚ [ Οƒβ‚‚ ] ∷ B [ t₁ ]β‚€ [ σ₁ ] β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ C₁ [ t₁ , u₁ ]₁₀ [ σ₁ ] ≑ Cβ‚‚ [ tβ‚‚ , uβ‚‚ ]₁₀ [ Οƒβ‚‚ ]
  βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]₁₀[]≑[]₁₀[]
    {B} {C₁} {Cβ‚‚} C₁≑Cβ‚‚ t₁[σ₁]≑tβ‚‚[Οƒβ‚‚] u₁[σ₁]≑uβ‚‚[Οƒβ‚‚] σ₁≑σ₂ =
    PE.substβ‚‚ (_⊩⟨_⟩_≑_ _ _)
      (PE.sym $ [,]-[]-commute C₁)
      (PE.sym $ [,]-[]-commute Cβ‚‚) $
    βŠ©α΅›β‰‘β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]₁₀ C₁≑Cβ‚‚ σ₁≑σ₂ t₁[σ₁]≑tβ‚‚[Οƒβ‚‚]
      (PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (singleSubstLift B _)
         u₁[σ₁]≑uβ‚‚[Οƒβ‚‚])

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_ and _⊩⟨_⟩_.

  βŠ©α΅›β†’βŠ©βˆ·β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]₁₀[] :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ C β†’
    Ξ” ⊩⟨ lβ€² ⟩ t [ Οƒ ] ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ u [ Οƒ ] ∷ B [ t ]β‚€ [ Οƒ ] β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ C [ t , u ]₁₀ [ Οƒ ]
  βŠ©α΅›β†’βŠ©βˆ·β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]₁₀[] {t} {u} ⊩C ⊩t[Οƒ] ⊩u[Οƒ] βŠ©Οƒ =
    βŠ©β‡”βŠ©β‰‘ .projβ‚‚ $
    βŠ©α΅›β‰‘β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]₁₀[]≑[]₁₀[] {tβ‚‚ = t} {uβ‚‚ = u} (refl-βŠ©α΅›β‰‘ ⊩C)
      (refl-βŠ©β‰‘βˆ· ⊩t[Οƒ]) (refl-βŠ©β‰‘βˆ· ⊩u[Οƒ]) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_≑_∷_ and _⊩⟨_⟩_≑_∷_.

  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]₁₀[]≑[]₁₀[]∷ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t₁ ≑ tβ‚‚ ∷ C β†’
    Ξ” ⊩⟨ lβ€² ⟩ u₁ [ σ₁ ] ≑ uβ‚‚ [ Οƒβ‚‚ ] ∷ A [ σ₁ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ v₁ [ σ₁ ] ≑ vβ‚‚ [ Οƒβ‚‚ ] ∷ B [ u₁ ]β‚€ [ σ₁ ] β†’
    Ξ” ⊩˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ t₁ [ u₁ , v₁ ]₁₀ [ σ₁ ] ≑ tβ‚‚ [ uβ‚‚ , vβ‚‚ ]₁₀ [ Οƒβ‚‚ ] ∷
      C [ u₁ , v₁ ]₁₀ [ σ₁ ]
  βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]₁₀[]≑[]₁₀[]∷
    {B} {t₁} {tβ‚‚} {C} t₁≑tβ‚‚ u₁[σ₁]≑uβ‚‚[Οƒβ‚‚] v₁[σ₁]≑vβ‚‚[Οƒβ‚‚] σ₁≑σ₂ =
    PE.subst₃ (_⊩⟨_⟩_≑_∷_ _ _) (PE.sym $ [,]-[]-commute t₁)
      (PE.sym $ [,]-[]-commute tβ‚‚) (PE.sym $ [,]-[]-commute C) $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©[⇑⇑][]₁₀≑[⇑⇑][]β‚β‚€βˆ· t₁≑tβ‚‚ σ₁≑σ₂ u₁[σ₁]≑uβ‚‚[Οƒβ‚‚]
      (PE.subst (_⊩⟨_⟩_≑_∷_ _ _ _ _) (singleSubstLift B _)
         v₁[σ₁]≑vβ‚‚[Οƒβ‚‚])

opaque

  -- A substitution lemma for _βŠ©α΅›βŸ¨_⟩_∷_ and _⊩⟨_⟩_∷_.

  βŠ©α΅›βˆ·β†’βŠ©βˆ·β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]₁₀[]∷ :
    Ξ“ βˆ™ A βˆ™ B βŠ©α΅›βŸ¨ l ⟩ t ∷ C β†’
    Ξ” ⊩⟨ lβ€² ⟩ u [ Οƒ ] ∷ A [ Οƒ ] β†’
    Ξ” ⊩⟨ lβ€³ ⟩ v [ Οƒ ] ∷ B [ u ]β‚€ [ Οƒ ] β†’
    Ξ” ⊩˒ Οƒ ∷ Ξ“ β†’
    Ξ” ⊩⟨ l ⟩ t [ u , v ]₁₀ [ Οƒ ] ∷ C [ u , v ]₁₀ [ Οƒ ]
  βŠ©α΅›βˆ·β†’βŠ©βˆ·β†’βŠ©βˆ·β†’βŠ©Λ’βˆ·β†’βŠ©[]₁₀[]∷ {u} {v} ⊩t ⊩u[Οƒ] ⊩v[Οƒ] βŠ©Οƒ =
    βŠ©βˆ·β‡”βŠ©β‰‘βˆ· .projβ‚‚ $
    βŠ©α΅›β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©β‰‘βˆ·β†’βŠ©Λ’β‰‘βˆ·β†’βŠ©[]₁₀[]≑[]₁₀[]∷ {uβ‚‚ = u} {vβ‚‚ = v} (refl-βŠ©α΅›β‰‘βˆ· ⊩t)
      (refl-βŠ©β‰‘βˆ· ⊩u[Οƒ]) (refl-βŠ©β‰‘βˆ· ⊩v[Οƒ]) (refl-βŠ©Λ’β‰‘βˆ· βŠ©Οƒ)