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

{-# OPTIONS --backtracking-instance-search #-}

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

module Definition.Typed.Substitution.Primitive.Primitive
  {a} {M : Set a}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  where

open Type-restrictions R

open import Definition.Typed R
open import Definition.Typed.Inversion.Primitive R
open import Definition.Typed.Properties.Admissible.Var R
open import Definition.Typed.Properties.Well-formed R
open import Definition.Typed.Reasoning.Term.Primitive R
open import Definition.Typed.Size R
open import Definition.Typed.Weakening R as W hiding (wk)

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

open import Tools.Fin
open import Tools.Function
open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Reasoning.PropositionalEquality
open import Tools.Relation
open import Tools.Size
open import Tools.Size.Instances
open import Tools.Sum using (inj₂)

private variable
  k m n                      : Nat
  x                          : Fin _
  Γ Δ Η                      : Con Term _
  A A₁ A₂ B t t₁ t₂ u v      : Term _
  σ σ₁ σ₁₁ σ₁₂ σ₂ σ₂₁ σ₂₂ σ₃ : Subst _ _
  ρ                          : Wk _ _
  s s₂                       : Size
  p q                        : M

------------------------------------------------------------------------
-- An admissible equality rule

opaque

  -- Lambdas preserve definitional equality.
  --
  -- See also Definition.Typed.Properties.Admissible.Pi.lam-cong.

  lam-cong :
    Γ ∙ A ⊢ B →
    Γ ∙ A ⊢ t ∷ B →
    Γ ∙ A ⊢ u ∷ B →
    Γ ∙ A ⊢ t ≡ u ∷ B →
    Π-allowed p q →
    Γ ⊢ lam p t ≡ lam p u ∷ Π p , q ▷ A ▹ B
  lam-cong {Γ} {A} {B} {t} {u} {p} ⊢B ⊢t ⊢u t≡u ok =
    η-eq ⊢B (lamⱼ ⊢B ⊢t ok) (lamⱼ ⊢B ⊢u ok)
      (wk1 (lam p t) ∘⟨ p ⟩ var x0        ≡⟨ lemma ⊢t ⟩⊢
       wk (lift (step id)) t [ var x0 ]₀  ≡⟨ PE.subst₂ (_ ⊢_≡_∷ _) (PE.sym (wkSingleSubstId _)) (PE.sym (wkSingleSubstId _))
                                             t≡u ⟩⊢
       wk (lift (step id)) u [ var x0 ]₀  ≡⟨ sym ⊢B (lemma ⊢u) ⟩⊢∎
       wk1 (lam p u) ∘⟨ p ⟩ var x0        ∎)
      ok
    where
    lemma :
      Γ ∙ A ⊢ v ∷ B →
      Γ ∙ A ⊢
        wk1 (lam p v) ∘⟨ p ⟩ var x0 ≡
        wk (lift (step id)) v [ var x0 ]₀ ∷ B
    lemma ⊢v =
      let ⊢A  = ⊢∙→⊢ (wf ⊢B)
          ⊢A′ = wk₁ ⊢A ⊢A
          ρ   = liftʷ (step id) ⊢A′
      in
      PE.subst (_ ⊢ _ ≡ _ ∷_) (wkSingleSubstId _) $
      β-red (W.wk ρ ⊢B) (wkTerm ρ ⊢v) (var₀ ⊢A) PE.refl ok

------------------------------------------------------------------------
-- Well-formed substitutions

-- Well-formed substitutions.

data _⊢ˢ_∷_ (Δ : Con Term m) : Subst m n → Con Term n → Set a where
  id  : Δ ⊢ˢ σ ∷ ε
  _,_ : Δ ⊢ˢ tail σ ∷ Γ →
        Δ ⊢  head σ ∷ A [ tail σ ] →
        Δ ⊢ˢ σ      ∷ Γ ∙ A

opaque

  infix  _⊢ˢʷ_∷_

  -- A variant of _⊢ˢ_∷_. The letter W stands for "well-formed": the
  -- target context must be well-formed.

  _⊢ˢʷ_∷_ : Con Term m → Subst m n → Con Term n → Set a
  Δ ⊢ˢʷ σ ∷ Γ = ⊢ Δ × Δ ⊢ˢ σ ∷ Γ

opaque
  unfolding _⊢ˢʷ_∷_

  -- A characterisation lemma for _⊢ˢʷ_∷_.

  ⊢ˢʷ∷⇔ : Δ ⊢ˢʷ σ ∷ Γ ⇔ (⊢ Δ × Δ ⊢ˢ σ ∷ Γ)
  ⊢ˢʷ∷⇔ = id⇔

opaque
  unfolding _⊢ˢʷ_∷_

  -- A characterisation lemma for _⊢ˢʷ_∷_.

  ⊢ˢʷ∷ε⇔ : Δ ⊢ˢʷ σ ∷ ε ⇔ ⊢ Δ
  ⊢ˢʷ∷ε⇔ = proj₁ , (_, id)

opaque
  unfolding _⊢ˢʷ_∷_

  -- A characterisation lemma for _⊢ˢʷ_∷_.

  ⊢ˢʷ∷∙⇔ :
    Δ ⊢ˢʷ σ ∷ Γ ∙ A ⇔
    (Δ ⊢ˢʷ tail σ ∷ Γ × Δ ⊢ head σ ∷ A [ tail σ ])
  ⊢ˢʷ∷∙⇔ =
    (λ { (⊢Δ , (⊢σ₊ , ⊢σ₀)) → (⊢Δ , ⊢σ₊) , ⊢σ₀ }) ,
    (λ ((⊢Δ , ⊢σ₊) , ⊢σ₀) → ⊢Δ , (⊢σ₊ , ⊢σ₀))

opaque

  -- An introduction lemma for _⊢ˢʷ_∷_.

  →⊢ˢʷ∷∙ :
    Δ ⊢ˢʷ tail σ ∷ Γ → Δ ⊢ head σ ∷ A [ tail σ ] →
    Δ ⊢ˢʷ σ ∷ Γ ∙ A
  →⊢ˢʷ∷∙ ⊢σ₊ ⊢σ₀ = ⊢ˢʷ∷∙⇔ .proj₂ (⊢σ₊ , ⊢σ₀)

opaque
  unfolding _⊢ˢʷ_∷_

  -- A well-formedness lemma for _⊢ˢʷ_∷_.

  wf-⊢ˢʷ∷ : Δ ⊢ˢʷ σ ∷ Γ → ⊢ Δ
  wf-⊢ˢʷ∷ (⊢Δ , _) = ⊢Δ

------------------------------------------------------------------------
-- Well-formed equality of substitutions

-- Well-formed equality of substitutions.

data _⊢ˢ_≡_∷_ (Δ : Con Term m) :
       (_ _ : Subst m n) → Con Term n → Set a where
  id  : Δ ⊢ˢ σ₁ ≡ σ₂ ∷ ε
  _,_ : Δ ⊢ˢ tail σ₁ ≡ tail σ₂ ∷ Γ
      → Δ ⊢  head σ₁ ≡ head σ₂ ∷ A [ tail σ₁ ]
      → Δ ⊢ˢ σ₁      ≡ σ₂      ∷ Γ ∙ A

opaque

  infix  _⊢ˢʷ_≡_∷_

  -- A variant of _⊢ˢ_≡_∷_.

  _⊢ˢʷ_≡_∷_ : Con Term m → Subst m n → Subst m n → Con Term n → Set a
  Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ =
    ⊢ Δ × Δ ⊢ˢ σ₁ ∷ Γ × Δ ⊢ˢ σ₂ ∷ Γ × Δ ⊢ˢ σ₁ ≡ σ₂ ∷ Γ

opaque
  unfolding _⊢ˢʷ_≡_∷_

  -- A characterisation lemma for _⊢ˢʷ_≡_∷_.

  ⊢ˢʷ≡∷⇔ :
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ ⇔
    (⊢ Δ × Δ ⊢ˢ σ₁ ∷ Γ × Δ ⊢ˢ σ₂ ∷ Γ × Δ ⊢ˢ σ₁ ≡ σ₂ ∷ Γ)
  ⊢ˢʷ≡∷⇔ = id⇔

opaque
  unfolding _⊢ˢʷ_≡_∷_

  -- A characterisation lemma for _⊢ˢʷ_≡_∷_.

  ⊢ˢʷ≡∷ε⇔ : Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ ε ⇔ ⊢ Δ
  ⊢ˢʷ≡∷ε⇔ = proj₁ , (_, (id , id , id))

opaque
  unfolding _⊢ˢʷ_≡_∷_

  -- A characterisation lemma for _⊢ˢʷ_≡_∷_.

  ⊢ˢʷ≡∷∙⇔ :
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ ∙ A ⇔
    (Δ ⊢ˢʷ tail σ₁ ≡ tail σ₂ ∷ Γ ×
     Δ ⊢ head σ₁ ∷ A [ tail σ₁ ] ×
     Δ ⊢ head σ₂ ∷ A [ tail σ₂ ] ×
     Δ ⊢ head σ₁ ≡ head σ₂ ∷ A [ tail σ₁ ])
  ⊢ˢʷ≡∷∙⇔ =
    (λ { (⊢Δ , (⊢σ₁₊ , ⊢σ₁₀) , (⊢σ₂₊ , ⊢σ₂₀) , (σ₁₊≡σ₂₊ , σ₁₀≡σ₂₀)) →
         (⊢Δ , (⊢σ₁₊ , ⊢σ₂₊ , σ₁₊≡σ₂₊)) , ⊢σ₁₀ , ⊢σ₂₀ , σ₁₀≡σ₂₀ }) ,
    (λ ((⊢Δ , (⊢σ₁₊ , ⊢σ₂₊ , σ₁₊≡σ₂₊)) , ⊢σ₁₀ , ⊢σ₂₀ , σ₁₀≡σ₂₀) →
       (⊢Δ , (⊢σ₁₊ , ⊢σ₁₀) , (⊢σ₂₊ , ⊢σ₂₀) , (σ₁₊≡σ₂₊ , σ₁₀≡σ₂₀)))

opaque
  unfolding _⊢ˢʷ_∷_ _⊢ˢʷ_≡_∷_

  -- A well-formedness lemma for _⊢ˢʷ_≡_∷_.

  wf-⊢ˢʷ≡∷ :
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    ⊢ Δ × Δ ⊢ˢʷ σ₁ ∷ Γ × Δ ⊢ˢʷ σ₂ ∷ Γ
  wf-⊢ˢʷ≡∷ (⊢Δ , ⊢σ₁ , ⊢σ₂ , _) =
    ⊢Δ , (⊢Δ , ⊢σ₁) , (⊢Δ , ⊢σ₂)

------------------------------------------------------------------------
-- Some lemmas related to _⊢ˢʷ_∷_ and _⊢ˢʷ_≡_∷_

private opaque

  -- Reflexivity for _⊢ˢ_≡_∷_.

  refl-⊢ˢ≡∷ :
    Δ ⊢ˢ σ ∷ Γ →
    Δ ⊢ˢ σ ≡ σ ∷ Γ
  refl-⊢ˢ≡∷ id        = id
  refl-⊢ˢ≡∷ (⊢σ , ⊢t) = refl-⊢ˢ≡∷ ⊢σ , refl ⊢t

opaque
  unfolding _⊢ˢʷ_∷_ _⊢ˢʷ_≡_∷_

  -- Reflexivity for _⊢ˢʷ_≡_∷_.

  refl-⊢ˢʷ≡∷ :
    Δ ⊢ˢʷ σ ∷ Γ →
    Δ ⊢ˢʷ σ ≡ σ ∷ Γ
  refl-⊢ˢʷ≡∷ (⊢Δ , ⊢σ) = ⊢Δ , ⊢σ , ⊢σ , refl-⊢ˢ≡∷ ⊢σ

opaque

  -- A lemma relating _⊢ˢʷ_∷_ and _⊢ˢʷ_≡_∷_.

  ⊢ˢʷ∷⇔⊢ˢʷ≡∷ :
    Δ ⊢ˢʷ σ ∷ Γ ⇔ Δ ⊢ˢʷ σ ≡ σ ∷ Γ
  ⊢ˢʷ∷⇔⊢ˢʷ≡∷ = refl-⊢ˢʷ≡∷ , proj₁ ∘→ proj₂ ∘→ wf-⊢ˢʷ≡∷

opaque

  -- A lemma related to _•ₛ_.

  ⊢ˢʷ≡∷-•ₛ :
    ρ ∷ʷ Η ⊇ Δ →
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    Η ⊢ˢʷ ρ •ₛ σ₁ ≡ ρ •ₛ σ₂ ∷ Γ
  ⊢ˢʷ≡∷-•ₛ {Γ = ε} ρ⊇ _ =
    ⊢ˢʷ≡∷ε⇔ .proj₂ (wf-∷ʷ⊇ ρ⊇)
  ⊢ˢʷ≡∷-•ₛ {Γ = _ ∙ A} ρ⊇ σ₁≡σ₂ =
    let σ₁₊≡σ₂₊ , ⊢σ₁₀ , ⊢σ₂₀ , σ₁₀≡σ₂₀ = ⊢ˢʷ≡∷∙⇔ .proj₁ σ₁≡σ₂ in
    ⊢ˢʷ≡∷∙⇔ .proj₂
      ( ⊢ˢʷ≡∷-•ₛ ρ⊇ σ₁₊≡σ₂₊
      , PE.subst (_⊢_∷_ _ _)     (wk-subst A) (wkTerm   ρ⊇ ⊢σ₁₀)
      , PE.subst (_⊢_∷_ _ _)     (wk-subst A) (wkTerm   ρ⊇ ⊢σ₂₀)
      , PE.subst (_⊢_≡_∷_ _ _ _) (wk-subst A) (wkEqTerm ρ⊇ σ₁₀≡σ₂₀)
      )

opaque

  -- A lemma related to _•ₛ_.

  ⊢ˢʷ∷-•ₛ :
    ρ ∷ʷ Η ⊇ Δ →
    Δ ⊢ˢʷ σ ∷ Γ →
    Η ⊢ˢʷ ρ •ₛ σ ∷ Γ
  ⊢ˢʷ∷-•ₛ ρ⊇ =
    ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₂ ∘→ ⊢ˢʷ≡∷-•ₛ ρ⊇ ∘→ ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₁

opaque

  -- A lemma related to wk1Subst.

  ⊢ˢʷ∷-wk1Subst :
    Δ ⊢ A →
    Δ ⊢ˢʷ σ ∷ Γ →
    Δ ∙ A ⊢ˢʷ wk1Subst σ ∷ Γ
  ⊢ˢʷ∷-wk1Subst ⊢A =
    ⊢ˢʷ∷-•ₛ (stepʷ id ⊢A)

opaque

  -- A lemma related to wk1Subst.

  ⊢ˢʷ≡∷-wk1Subst :
    Δ ⊢ A →
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    Δ ∙ A ⊢ˢʷ wk1Subst σ₁ ≡ wk1Subst σ₂ ∷ Γ
  ⊢ˢʷ≡∷-wk1Subst ⊢A =
    ⊢ˢʷ≡∷-•ₛ (stepʷ id ⊢A)

opaque

  -- A lemma related to wkSubst.

  ⊢ˢʷ≡∷-wkSubst :
    ⊢ Δ →
    drop k Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    Δ ⊢ˢʷ wkSubst k σ₁ ≡ wkSubst k σ₂ ∷ Γ
  ⊢ˢʷ≡∷-wkSubst {k = }    _      σ₁≡σ₂ = σ₁≡σ₂
  ⊢ˢʷ≡∷-wkSubst {k = 1+ _} (∙ ⊢A) σ₁≡σ₂ =
    ⊢ˢʷ≡∷-wk1Subst ⊢A (⊢ˢʷ≡∷-wkSubst (wf ⊢A) σ₁≡σ₂)

opaque

  -- A lemma related to wkSubst.

  ⊢ˢʷ∷-wkSubst :
    ⊢ Δ →
    drop k Δ ⊢ˢʷ σ ∷ Γ →
    Δ ⊢ˢʷ wkSubst k σ ∷ Γ
  ⊢ˢʷ∷-wkSubst ⊢Δ =
    ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₂ ∘→ ⊢ˢʷ≡∷-wkSubst ⊢Δ ∘→ ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₁

opaque

  -- A lemma related to idSubst.

  ⊢ˢʷ∷-idSubst :
    ⊢ Γ →
    Γ ⊢ˢʷ idSubst ∷ Γ
  ⊢ˢʷ∷-idSubst ε =
    ⊢ˢʷ∷ε⇔ .proj₂ ε
  ⊢ˢʷ∷-idSubst (∙ ⊢A) =
    →⊢ˢʷ∷∙ (⊢ˢʷ∷-wk1Subst ⊢A (⊢ˢʷ∷-idSubst (wf ⊢A)))
      (PE.subst (_⊢_∷_ _ _) (wk1-tailId _) (var₀ ⊢A))

opaque

  -- A lemma related to sgSubst.

  ⊢ˢʷ≡∷-sgSubst :
    Γ ⊢ t₁ ∷ A →
    Γ ⊢ t₂ ∷ A →
    Γ ⊢ t₁ ≡ t₂ ∷ A →
    Γ ⊢ˢʷ sgSubst t₁ ≡ sgSubst t₂ ∷ Γ ∙ A
  ⊢ˢʷ≡∷-sgSubst ⊢t₁ ⊢t₂ t₁≡t₂ =
    ⊢ˢʷ≡∷∙⇔ .proj₂
      ( refl-⊢ˢʷ≡∷ (⊢ˢʷ∷-idSubst (wfEqTerm t₁≡t₂))
      , PE.subst (_⊢_∷_ _ _) (PE.sym $ subst-id _) ⊢t₁
      , PE.subst (_⊢_∷_ _ _) (PE.sym $ subst-id _) ⊢t₂
      , PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ subst-id _) t₁≡t₂
      )

opaque

  -- A lemma related to sgSubst.

  ⊢ˢʷ∷-sgSubst :
    Γ ⊢ t ∷ A →
    Γ ⊢ˢʷ sgSubst t ∷ Γ ∙ A
  ⊢ˢʷ∷-sgSubst ⊢t =
    ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₂ (⊢ˢʷ≡∷-sgSubst ⊢t ⊢t (refl ⊢t))

opaque

  -- A lemma related to _⇑.

  ⊢ˢʷ≡∷-⇑ :
    Δ ⊢ A [ σ₁ ] →
    Δ ⊢ A [ σ₁ ] ≡ A [ σ₂ ] →
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    Δ ∙ A [ σ₁ ] ⊢ˢʷ σ₁ ⇑ ≡ σ₂ ⇑ ∷ Γ ∙ A
  ⊢ˢʷ≡∷-⇑ {A} ⊢A[σ₁] A[σ₁]≡A[σ₂] σ₁≡σ₂ =
    let ⊢0 = PE.subst (_⊢_∷_ _ _) (PE.sym $ wk1Subst-wk1 A)
               (var₀ ⊢A[σ₁])
    in
    ⊢ˢʷ≡∷∙⇔ .proj₂
      (⊢ˢʷ≡∷-wk1Subst ⊢A[σ₁] σ₁≡σ₂ ,
       ⊢0 ,
       PE.subst (_⊢_∷_ _ _) (PE.sym $ wk1Subst-wk1 A)
         (conv (var₀ ⊢A[σ₁]) (wkEq₁ ⊢A[σ₁] A[σ₁]≡A[σ₂])) ,
       refl ⊢0)

opaque

  -- A lemma related to _⇑.

  ⊢ˢʷ∷-⇑ :
    Δ ⊢ A [ σ ] →
    Δ ⊢ˢʷ σ ∷ Γ →
    Δ ∙ A [ σ ] ⊢ˢʷ σ ⇑ ∷ Γ ∙ A
  ⊢ˢʷ∷-⇑ ⊢A[σ] =
    ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₂ ∘→ ⊢ˢʷ≡∷-⇑ ⊢A[σ] (refl ⊢A[σ]) ∘→
    ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₁

opaque

  -- A cast lemma for _⊢ˢʷ_≡_∷_.

  cast-⊢ˢʷ≡∷ :
    (∀ x → σ₁₁ x PE.≡ σ₂₁ x) →
    (∀ x → σ₁₂ x PE.≡ σ₂₂ x) →
    Δ ⊢ˢʷ σ₁₁ ≡ σ₁₂ ∷ Γ → Δ ⊢ˢʷ σ₂₁ ≡ σ₂₂ ∷ Γ
  cast-⊢ˢʷ≡∷ {Γ = ε} _ _ σ₁₁≡σ₁₂ =
    ⊢ˢʷ≡∷ε⇔ .proj₂ (⊢ˢʷ≡∷ε⇔ .proj₁ σ₁₁≡σ₁₂)
  cast-⊢ˢʷ≡∷ {Γ = _ ∙ A} σ₁₁≡σ₂₁ σ₁₂≡σ₂₂ σ₁₁≡σ₁₂ =
    let σ₁₁₊≡σ₁₂₊ , ⊢σ₁₁₀ , ⊢σ₁₂₀ , σ₁₁₀≡σ₁₂₀ =
          ⊢ˢʷ≡∷∙⇔ .proj₁ σ₁₁≡σ₁₂
        σ₁₁₊≡σ₂₁₊ = σ₁₁≡σ₂₁ ∘→ _+1
        σ₁₂₊≡σ₂₂₊ = σ₁₂≡σ₂₂ ∘→ _+1
        σ₂₁₊≡σ₂₂₊ = cast-⊢ˢʷ≡∷ σ₁₁₊≡σ₂₁₊ σ₁₂₊≡σ₂₂₊ σ₁₁₊≡σ₁₂₊
    in
    ⊢ˢʷ≡∷∙⇔ .proj₂
      ( σ₂₁₊≡σ₂₂₊
      , PE.subst₂ (_⊢_∷_ _) (σ₁₁≡σ₂₁ x0)
          (substVar-to-subst σ₁₁₊≡σ₂₁₊ A) ⊢σ₁₁₀
      , PE.subst₂ (_⊢_∷_ _) (σ₁₂≡σ₂₂ x0)
          (substVar-to-subst σ₁₂₊≡σ₂₂₊ A) ⊢σ₁₂₀
      , PE.subst₃ (_⊢_≡_∷_ _) (σ₁₁≡σ₂₁ x0) (σ₁₂≡σ₂₂ x0)
          (substVar-to-subst σ₁₁₊≡σ₂₁₊ A) σ₁₁₀≡σ₁₂₀
      )

opaque

  -- A cast lemma for _⊢ˢʷ_∷_.

  cast-⊢ˢʷ∷ :
    (∀ x → σ₁ x PE.≡ σ₂ x) →
    Δ ⊢ˢʷ σ₁ ∷ Γ → Δ ⊢ˢʷ σ₂ ∷ Γ
  cast-⊢ˢʷ∷ σ₁≡σ₂ =
    ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₂ ∘→ cast-⊢ˢʷ≡∷ σ₁≡σ₂ σ₁≡σ₂ ∘→ ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₁

opaque

  -- If ρ is a well-formed weakening, then toSubst ρ is a well-formed
  -- substitution.

  ⊢ˢʷ-toSubst : ρ ∷ʷ Δ ⊇ Γ → Δ ⊢ˢʷ toSubst ρ ∷ Γ
  ⊢ˢʷ-toSubst ρ⊇ = ⊢ˢʷ-toSubst′ (wf-∷ʷ⊇ ρ⊇) (∷ʷ⊇→∷⊇ ρ⊇)
    where
    ⊢ˢʷ-toSubst′ : ⊢ Δ → ρ ∷ Δ ⊇ Γ → Δ ⊢ˢʷ toSubst ρ ∷ Γ
    ⊢ˢʷ-toSubst′ ⊢Δ id =
      ⊢ˢʷ∷-idSubst ⊢Δ
    ⊢ˢʷ-toSubst′ (∙ ⊢A) (step ρ⊇) =
      ⊢ˢʷ∷-wk1Subst ⊢A (⊢ˢʷ-toSubst′ (wf ⊢A) ρ⊇)
    ⊢ˢʷ-toSubst′ (∙ ⊢A) (lift ρ⊇) =
      cast-⊢ˢʷ∷ (PE.sym ∘→ toSubst-liftn ) $
      PE.subst₃ _⊢ˢʷ_∷_
        (PE.cong (_∙_ _) (PE.sym $ wk≡subst _ _)) PE.refl PE.refl $
      ⊢ˢʷ∷-⇑ (PE.subst (_⊢_ _) (wk≡subst _ _) ⊢A) $
      ⊢ˢʷ-toSubst′ (wf ⊢A) ρ⊇

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

opaque

  -- A substitution lemma for _∷_∈_.

  subst-∷∈→⊢∷ : x ∷ A ∈ Γ → Δ ⊢ˢʷ σ ∷ Γ → Δ ⊢ σ x ∷ A [ σ ]
  subst-∷∈→⊢∷ (here {A}) ⊢σ =
    PE.subst (_⊢_∷_ _ _) (PE.sym $ wk1-tail A) $
    ⊢ˢʷ∷∙⇔ .proj₁ ⊢σ .proj₂
  subst-∷∈→⊢∷ (there {A} x∈) ⊢σ =
    PE.subst (_⊢_∷_ _ _) (PE.sym $ wk1-tail A) $
    subst-∷∈→⊢∷ x∈ (⊢ˢʷ∷∙⇔ .proj₁ ⊢σ .proj₁)

opaque

  -- A substitution lemma for _∷_∈_.

  subst-∷∈→⊢≡∷ :
    x ∷ A ∈ Γ → Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ → Δ ⊢ σ₁ x ≡ σ₂ x ∷ A [ σ₁ ]
  subst-∷∈→⊢≡∷ (here {A}) σ₁≡σ₂ =
    PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ wk1-tail A) $
    ⊢ˢʷ≡∷∙⇔ .proj₁ σ₁≡σ₂ .proj₂ .proj₂ .proj₂
  subst-∷∈→⊢≡∷ (there {A} x∈) σ₁≡σ₂ =
    PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ wk1-tail A) $
    subst-∷∈→⊢≡∷ x∈ (⊢ˢʷ≡∷∙⇔ .proj₁ σ₁≡σ₂ .proj₁)

private

  -- Below several properties are proved simultaneously using
  -- well-founded induction. The properties are collected in the
  -- record type P.

  record P (s : Size) : Set a where
    no-eta-equality
    field
      sym-⊢ˢʷ≡∷ :
        (⊢Γ : ⊢ Γ) →
        size-⊢′ ⊢Γ PE.≡ s →
        Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
        Δ ⊢ˢʷ σ₂ ≡ σ₁ ∷ Γ
      subst-⊢ :
        Δ ⊢ˢʷ σ ∷ Γ →
        (⊢A : Γ ⊢ A) →
        size-⊢ ⊢A PE.≡ s →
        Δ ⊢ A [ σ ]
      subst-⊢→⊢≡ :
        Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
        (⊢A : Γ ⊢ A) →
        size-⊢ ⊢A PE.≡ s →
        Δ ⊢ A [ σ₁ ] ≡ A [ σ₂ ]
      subst-⊢≡ :
        Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
        (A₁≡A₂ : Γ ⊢ A₁ ≡ A₂) →
        size-⊢≡ A₁≡A₂ PE.≡ s →
        Δ ⊢ A₁ [ σ₁ ] ≡ A₂ [ σ₂ ]
      subst-⊢∷ :
        Δ ⊢ˢʷ σ ∷ Γ →
        (⊢t : Γ ⊢ t ∷ A) →
        size-⊢∷ ⊢t PE.≡ s →
        Δ ⊢ t [ σ ] ∷ A [ σ ]
      subst-⊢∷→⊢≡∷ :
        Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
        (⊢t : Γ ⊢ t ∷ A) →
        size-⊢∷ ⊢t PE.≡ s →
        Δ ⊢ t [ σ₁ ] ≡ t [ σ₂ ] ∷ A [ σ₁ ]
      subst-⊢≡∷ :
        Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
        (t₁≡t₂ : Γ ⊢ t₁ ≡ t₂ ∷ A) →
        size-⊢≡∷ t₁≡t₂ PE.≡ s →
        Δ ⊢ t₁ [ σ₁ ] ≡ t₂ [ σ₂ ] ∷ A [ σ₁ ]

-- Variants of the fields of P, along with some derived lemmas.

private module Lemmas (hyp : ∀ {s₁} → s₁ <ˢ s₂ → P s₁) where

  opaque

    -- Variants of the fields of P.

    sym-⊢ˢʷ≡∷ :
      (⊢Γ : ⊢ Γ) →
      ⦃ lt : size-⊢′ ⊢Γ <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      Δ ⊢ˢʷ σ₂ ≡ σ₁ ∷ Γ
    sym-⊢ˢʷ≡∷ ⊢Γ ⦃ lt ⦄ = P.sym-⊢ˢʷ≡∷ (hyp lt) ⊢Γ PE.refl

    subst-⊢ :
      (⊢A : Γ ⊢ A)
      ⦃ lt : size-⊢ ⊢A <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ Γ → Δ ⊢ A [ σ ]
    subst-⊢ ⊢A ⦃ lt ⦄ ⊢σ = P.subst-⊢ (hyp lt) ⊢σ ⊢A PE.refl

    subst-⊢→⊢≡ :
      (⊢A : Γ ⊢ A)
      ⦃ lt : size-⊢ ⊢A <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ → Δ ⊢ A [ σ₁ ] ≡ A [ σ₂ ]
    subst-⊢→⊢≡ ⊢A ⦃ lt ⦄ σ₁≡σ₂ = P.subst-⊢→⊢≡ (hyp lt) σ₁≡σ₂ ⊢A PE.refl

    subst-⊢≡ :
      (A₁≡A₂ : Γ ⊢ A₁ ≡ A₂)
      ⦃ lt : size-⊢≡ A₁≡A₂ <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ → Δ ⊢ A₁ [ σ₁ ] ≡ A₂ [ σ₂ ]
    subst-⊢≡ A₁≡A₂ ⦃ lt ⦄ σ₁≡σ₂ =
      P.subst-⊢≡ (hyp lt) σ₁≡σ₂ A₁≡A₂ PE.refl

    subst-⊢∷ :
      (⊢t : Γ ⊢ t ∷ A)
      ⦃ lt : size-⊢∷ ⊢t <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ Γ → Δ ⊢ t [ σ ] ∷ A [ σ ]
    subst-⊢∷ ⊢t ⦃ lt ⦄ ⊢σ = P.subst-⊢∷ (hyp lt) ⊢σ ⊢t PE.refl

    subst-⊢∷→⊢≡∷ :
      (⊢t : Γ ⊢ t ∷ A)
      ⦃ lt : size-⊢∷ ⊢t <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ → Δ ⊢ t [ σ₁ ] ≡ t [ σ₂ ] ∷ A [ σ₁ ]
    subst-⊢∷→⊢≡∷ ⊢t ⦃ lt ⦄ σ₁≡σ₂ =
      P.subst-⊢∷→⊢≡∷ (hyp lt) σ₁≡σ₂ ⊢t PE.refl

    subst-⊢≡∷ :
      (t₁≡t₂ : Γ ⊢ t₁ ≡ t₂ ∷ A)
      ⦃ lt : size-⊢≡∷ t₁≡t₂ <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      Δ ⊢ t₁ [ σ₁ ] ≡ t₂ [ σ₂ ] ∷ A [ σ₁ ]
    subst-⊢≡∷ t₁≡t₂ ⦃ lt ⦄ σ₁≡σ₂ =
      P.subst-⊢≡∷ (hyp lt) σ₁≡σ₂ t₁≡t₂ PE.refl

  opaque

    -- Variants of some of the variants.

    sym-⊢ˢʷ≡∷-<ˢ :
      (∃ λ (⊢Γ : ⊢ Γ) → size-⊢′ ⊢Γ <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      Δ ⊢ˢʷ σ₂ ≡ σ₁ ∷ Γ
    sym-⊢ˢʷ≡∷-<ˢ (⊢Γ , lt) = sym-⊢ˢʷ≡∷ ⊢Γ ⦃ lt = <ˢ-trans lt ! ⦄

    subst-⊢-<ˢ :
      (∃ λ (⊢A : Γ ⊢ A) → size-⊢ ⊢A <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ Γ → Δ ⊢ A [ σ ]
    subst-⊢-<ˢ (⊢A , lt) = subst-⊢ ⊢A ⦃ lt = <ˢ-trans lt ! ⦄

    subst-⊢→⊢≡-<ˢ :
      (∃ λ (⊢A : Γ ⊢ A) → size-⊢ ⊢A <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ → Δ ⊢ A [ σ₁ ] ≡ A [ σ₂ ]
    subst-⊢→⊢≡-<ˢ (⊢A , lt) = subst-⊢→⊢≡ ⊢A ⦃ lt = <ˢ-trans lt ! ⦄

    subst-⊢∷-<ˢ :
      (∃ λ (⊢t : Γ ⊢ t ∷ A) → size-⊢∷ ⊢t <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ Γ → Δ ⊢ t [ σ ] ∷ A [ σ ]
    subst-⊢∷-<ˢ (⊢t , lt) = subst-⊢∷ ⊢t ⦃ lt = <ˢ-trans lt ! ⦄

    subst-⊢∷→⊢≡∷-<ˢ :
      (∃ λ (⊢t : Γ ⊢ t ∷ A) → size-⊢∷ ⊢t <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ → Δ ⊢ t [ σ₁ ] ≡ t [ σ₂ ] ∷ A [ σ₁ ]
    subst-⊢∷→⊢≡∷-<ˢ (⊢t , lt) = subst-⊢∷→⊢≡∷ ⊢t ⦃ lt = <ˢ-trans lt ! ⦄

  opaque

    -- A variant of ⊢ˢʷ∷-⇑.

    ⊢ˢʷ∷-⇑-<ˢ :
      (∃ λ (⊢A : Γ ⊢ A) → size-⊢ ⊢A <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ Γ →
      Δ ∙ A [ σ ] ⊢ˢʷ σ ⇑ ∷ Γ ∙ A
    ⊢ˢʷ∷-⇑-<ˢ ⊢A ⊢σ = ⊢ˢʷ∷-⇑ (subst-⊢-<ˢ ⊢A ⊢σ) ⊢σ

  opaque

    -- A variant of ⊢ˢʷ≡∷-⇑-<ˢ.

    ⊢ˢʷ≡∷-⇑-<ˢ :
      (∃ λ (⊢A : Γ ⊢ A) → size-⊢ ⊢A <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      Δ ∙ A [ σ₁ ] ⊢ˢʷ σ₁ ⇑ ≡ σ₂ ⇑ ∷ Γ ∙ A
    ⊢ˢʷ≡∷-⇑-<ˢ ⊢A σ₁≡σ₂ =
      let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
      ⊢ˢʷ≡∷-⇑ (subst-⊢-<ˢ ⊢A ⊢σ₁) (subst-⊢→⊢≡-<ˢ ⊢A σ₁≡σ₂) σ₁≡σ₂

  opaque
    unfolding size-⊢′

    -- A variant of ⊢ˢʷ≡∷-⇑.

    ⊢ˢʷ≡∷-⇑[]-<ˢ :
      (∃ λ (⊢Γ : ⊢ Γ) → size-⊢′ ⊢Γ <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ˢʷ σ₁ ⇑[ k ] ≡ σ₂ ⇑[ k ] ∷ Γ
    ⊢ˢʷ≡∷-⇑[]-<ˢ {k = }    (_ , _)     = idᶠ
    ⊢ˢʷ≡∷-⇑[]-<ˢ {k = 1+ _} (∙ ⊢A , lt) =
      let lt = ⊕≤ˢ→<ˢˡ (<ˢ→≤ˢ lt) in
      ⊢ˢʷ≡∷-⇑-<ˢ (⊢A , lt) ∘→
      ⊢ˢʷ≡∷-⇑[]-<ˢ (wf-<ˢ ⊢A) ⦃ lt = <ˢ-trans lt ! ⦄

  opaque

    -- A variant of ⊢ˢʷ∷-⇑.

    ⊢ˢʷ∷-⇑[]-<ˢ :
      (∃ λ (⊢Γ : ⊢ Γ) → size-⊢′ ⊢Γ <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ ] ⊢ˢʷ σ ⇑[ k ] ∷ Γ
    ⊢ˢʷ∷-⇑[]-<ˢ ⊢Γ =
      ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₂ ∘→ ⊢ˢʷ≡∷-⇑[]-<ˢ ⊢Γ ∘→ ⊢ˢʷ∷⇔⊢ˢʷ≡∷ .proj₁

  opaque

    -- Some substitution lemmas that use ⊢ˢʷ∷-⇑[]-<ˢ or ⊢ˢʷ≡∷-⇑[]-<ˢ.

    subst-⊢-⇑ :
      (⊢A : Γ ⊢ A)
      ⦃ lt : size-⊢ ⊢A <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ ] ⊢ A [ σ ⇑[ k ] ]
    subst-⊢-⇑ ⊢A = subst-⊢ ⊢A ∘→ ⊢ˢʷ∷-⇑[]-<ˢ (wf-<ˢ ⊢A)

    subst-⊢→⊢≡-⇑ :
      (⊢A : Γ ⊢ A)
      ⦃ lt : size-⊢ ⊢A <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ A [ σ₁ ⇑[ k ] ] ≡ A [ σ₂ ⇑[ k ] ]
    subst-⊢→⊢≡-⇑ ⊢A = subst-⊢→⊢≡ ⊢A ∘→ ⊢ˢʷ≡∷-⇑[]-<ˢ (wf-<ˢ ⊢A)

    subst-⊢→⊢≡-⇑-<ˢ :
      (∃ λ (⊢A : Γ ⊢ A) → size-⊢ ⊢A <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ A [ σ₁ ⇑[ k ] ] ≡ A [ σ₂ ⇑[ k ] ]
    subst-⊢→⊢≡-⇑-<ˢ (⊢A , lt) = subst-⊢→⊢≡-⇑ ⊢A ⦃ lt = <ˢ-trans lt ! ⦄

    subst-⊢≡-⇑ :
      (A₁≡A₂ : Γ ⊢ A₁ ≡ A₂)
      ⦃ lt : size-⊢≡ A₁≡A₂ <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ A₁ [ σ₁ ⇑[ k ] ] ≡ A₂ [ σ₂ ⇑[ k ] ]
    subst-⊢≡-⇑ A₁≡A₂ = subst-⊢≡ A₁≡A₂ ∘→ ⊢ˢʷ≡∷-⇑[]-<ˢ (wfEq-<ˢ A₁≡A₂)

    subst-⊢∷-⇑ :
      (⊢t : Γ ⊢ t ∷ A)
      ⦃ lt : size-⊢∷ ⊢t <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ ] ⊢ t [ σ ⇑[ k ] ] ∷ A [ σ ⇑[ k ] ]
    subst-⊢∷-⇑ ⊢t = subst-⊢∷ ⊢t ∘→ ⊢ˢʷ∷-⇑[]-<ˢ (wfTerm-<ˢ ⊢t)

    subst-⊢∷→⊢≡∷-⇑ :
      (⊢t : Γ ⊢ t ∷ A)
      ⦃ lt : size-⊢∷ ⊢t <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ t [ σ₁ ⇑[ k ] ] ≡ t [ σ₂ ⇑[ k ] ] ∷
        A [ σ₁ ⇑[ k ] ]
    subst-⊢∷→⊢≡∷-⇑ ⊢t = subst-⊢∷→⊢≡∷ ⊢t ∘→ ⊢ˢʷ≡∷-⇑[]-<ˢ (wfTerm-<ˢ ⊢t)

    subst-⊢≡∷-⇑ :
      (t₁≡t₂ : Γ ⊢ t₁ ≡ t₂ ∷ A)
      ⦃ lt : size-⊢≡∷ t₁≡t₂ <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
      Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ t₁ [ σ₁ ⇑[ k ] ] ≡ t₂ [ σ₂ ⇑[ k ] ] ∷
        A [ σ₁ ⇑[ k ] ]
    subst-⊢≡∷-⇑ t₁≡t₂ =
      subst-⊢≡∷ t₁≡t₂ ∘→ ⊢ˢʷ≡∷-⇑[]-<ˢ (wfEqTerm-<ˢ t₁≡t₂)

  opaque

    -- A lemma related to consSubst.

    ⊢ˢʷ≡∷-consSubst-[] :
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      (⊢t : Γ ⊢ t ∷ A)
      ⦃ lt : size-⊢∷ ⊢t <ˢ s₂ ⦄ →
      Δ ⊢ˢʷ consSubst σ₁ (t [ σ₁ ]) ≡ consSubst σ₂ (t [ σ₂ ]) ∷ Γ ∙ A
    ⊢ˢʷ≡∷-consSubst-[] σ₁≡σ₂ ⊢t =
      let _ , ⊢σ₁ , ⊢σ₂ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
      ⊢ˢʷ≡∷∙⇔ .proj₂
        ( σ₁≡σ₂
        , subst-⊢∷ ⊢t ⊢σ₁
        , subst-⊢∷ ⊢t ⊢σ₂
        , subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂
        )

-- The type P s is inhabited for every s.

private module Inhabited where

  opaque
    unfolding size-⊢′

    -- Symmetry for _⊢ˢʷ_≡_∷_.

    sym-⊢ˢʷ≡∷′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      (⊢Γ : ⊢ Γ) →
      size-⊢′ ⊢Γ PE.≡ s₂ →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      Δ ⊢ˢʷ σ₂ ≡ σ₁ ∷ Γ
    sym-⊢ˢʷ≡∷′ {Δ} {σ₁} {σ₂} _ ε _ =
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ ε  ⇔⟨ ⊢ˢʷ≡∷ε⇔ ⟩→
      ⊢ Δ                ⇔˘⟨ ⊢ˢʷ≡∷ε⇔ ⟩→
      Δ ⊢ˢʷ σ₂ ≡ σ₁ ∷ ε  □
    sym-⊢ˢʷ≡∷′ {Γ = Γ ∙ A} {Δ} {σ₁} {σ₂} hyp (∙ ⊢A) PE.refl =
      let ⊢Γ , Γ< = wf-<ˢ ⊢A in

      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ ∙ A                    ⇔⟨ ⊢ˢʷ≡∷∙⇔ ⟩→

      (Δ ⊢ˢʷ tail σ₁ ≡ tail σ₂ ∷ Γ ×
       Δ ⊢ head σ₁ ∷ A [ tail σ₁ ] ×
       Δ ⊢ head σ₂ ∷ A [ tail σ₂ ] ×
       Δ ⊢ head σ₁ ≡ head σ₂ ∷ A [ tail σ₁ ])  →⟨ (λ (σ₁₊≡σ₂₊ , ⊢σ₁₀ , ⊢σ₂₀ , σ₁₀≡σ₂₀) →
                                                     sym-⊢ˢʷ≡∷ ⊢Γ ⦃ lt = ↙ <ˢ→≤ˢ Γ< ⦄ σ₁₊≡σ₂₊ , ⊢σ₂₀ , ⊢σ₁₀ ,
                                                     conv (sym (subst-⊢ ⊢A (wf-⊢ˢʷ≡∷ σ₁₊≡σ₂₊ .proj₂ .proj₁)) σ₁₀≡σ₂₀)
                                                       (subst-⊢→⊢≡ ⊢A σ₁₊≡σ₂₊))
                                                ⟩
      (Δ ⊢ˢʷ tail σ₂ ≡ tail σ₁ ∷ Γ ×
       Δ ⊢ head σ₂ ∷ A [ tail σ₂ ] ×
       Δ ⊢ head σ₁ ∷ A [ tail σ₁ ] ×
       Δ ⊢ head σ₂ ≡ head σ₁ ∷ A [ tail σ₂ ])  ⇔˘⟨ ⊢ˢʷ≡∷∙⇔ ⟩→

      Δ ⊢ˢʷ σ₂ ≡ σ₁ ∷ Γ ∙ A                    □
      where
      open Lemmas hyp

  opaque
    unfolding size-⊢

    -- A substitution lemma for _⊢_.

    subst-⊢′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      Δ ⊢ˢʷ σ ∷ Γ →
      (⊢A : Γ ⊢ A) →
      size-⊢ ⊢A PE.≡ s₂ →
      Δ ⊢ A [ σ ]
    subst-⊢′ hyp ⊢σ = let open Lemmas hyp in λ where
      (Uⱼ _) _ →
        Uⱼ (wf-⊢ˢʷ∷ ⊢σ)
      (univ ⊢A) PE.refl →
        univ (subst-⊢∷ ⊢A ⊢σ)
      (ΠΣⱼ ⊢B ok) PE.refl →
        ΠΣⱼ (subst-⊢-⇑ ⊢B ⊢σ) ok
      (Emptyⱼ _) _ →
        Emptyⱼ (wf-⊢ˢʷ∷ ⊢σ)
      (Unitⱼ _ ok) _ →
        Unitⱼ (wf-⊢ˢʷ∷ ⊢σ) ok
      (ℕⱼ _) _ →
        ℕⱼ (wf-⊢ˢʷ∷ ⊢σ)
      (Idⱼ ⊢A ⊢t ⊢u) PE.refl →
        Idⱼ (subst-⊢ ⊢A ⊢σ) (subst-⊢∷ ⊢t ⊢σ) (subst-⊢∷ ⊢u ⊢σ)

  opaque
    unfolding size-⊢

    -- A substitution lemma for _⊢_ and _⊢_≡_.

    subst-⊢→⊢≡′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      (⊢A : Γ ⊢ A) →
      size-⊢ ⊢A PE.≡ s₂ →
      Δ ⊢ A [ σ₁ ] ≡ A [ σ₂ ]
    subst-⊢→⊢≡′ hyp σ₁≡σ₂ = let open Lemmas hyp in λ where
      (Uⱼ _) _ →
        refl (Uⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁))
      (univ ⊢A) PE.refl →
        univ (subst-⊢∷→⊢≡∷ ⊢A σ₁≡σ₂)
      (ΠΣⱼ ⊢B ok) PE.refl →
        let _ , ⊢A = ∙⊢→⊢-<ˢ ⊢B in
        ΠΣ-cong (subst-⊢→⊢≡-<ˢ ⊢A σ₁≡σ₂) (subst-⊢→⊢≡-⇑ ⊢B σ₁≡σ₂) ok
      (Emptyⱼ _) _ →
        refl (Emptyⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁))
      (Unitⱼ _ ok) _ →
        refl (Unitⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁) ok)
      (ℕⱼ _) _ →
        refl (ℕⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁))
      (Idⱼ ⊢A ⊢t ⊢u) PE.refl →
        Id-cong (subst-⊢→⊢≡ ⊢A σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂)

  opaque
    unfolding size-⊢≡

    -- A substitution lemma for _⊢_≡_.

    subst-⊢≡′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      (A₁≡A₂ : Γ ⊢ A₁ ≡ A₂) →
      size-⊢≡ A₁≡A₂ PE.≡ s₂ →
      Δ ⊢ A₁ [ σ₁ ] ≡ A₂ [ σ₂ ]
    subst-⊢≡′ hyp σ₁≡σ₂ = let open Lemmas hyp in λ where
      (univ A₁≡A₂) PE.refl →
        univ (subst-⊢≡∷ A₁≡A₂ σ₁≡σ₂)
      (refl ⊢A) PE.refl →
        subst-⊢→⊢≡ ⊢A σ₁≡σ₂
      (sym A₂≡A₁) PE.refl →
        let ⊢Γ = wfEq-<ˢ A₂≡A₁ in
        sym (subst-⊢≡ A₂≡A₁ (sym-⊢ˢʷ≡∷-<ˢ ⊢Γ σ₁≡σ₂))
      (trans A₁≡A₂ A₂≡A₃) PE.refl →
        trans (subst-⊢≡ A₁≡A₂ σ₁≡σ₂)
          (subst-⊢≡ A₂≡A₃ (refl-⊢ˢʷ≡∷ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₂ .proj₂)))
      (ΠΣ-cong A₁≡A₂ B₁≡B₂ ok) PE.refl →
        ΠΣ-cong (subst-⊢≡ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡-⇑ B₁≡B₂ σ₁≡σ₂) ok
      (Id-cong A₁≡A₂ t₁≡t₂ u₁≡u₂) PE.refl →
        Id-cong (subst-⊢≡ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂)

  opaque
    unfolding size-⊢∷

    -- A substitution lemma for _⊢_∷_.

    subst-⊢∷′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      Δ ⊢ˢʷ σ ∷ Γ →
      (⊢t : Γ ⊢ t ∷ A) →
      size-⊢∷ ⊢t PE.≡ s₂ →
      Δ ⊢ t [ σ ] ∷ A [ σ ]
    subst-⊢∷′ hyp ⊢σ = let open Lemmas hyp in λ where
      (conv ⊢t B≡A) PE.refl →
        conv (subst-⊢∷ ⊢t ⊢σ)
          (subst-⊢≡ B≡A (refl-⊢ˢʷ≡∷ ⊢σ))
      (var _ x∈) _ →
        subst-∷∈→⊢∷ x∈ ⊢σ
      (Uⱼ _) _ →
        Uⱼ (wf-⊢ˢʷ∷ ⊢σ)
      (ΠΣⱼ ⊢A ⊢B ok) PE.refl →
        ΠΣⱼ (subst-⊢∷ ⊢A ⊢σ) (subst-⊢∷-⇑ ⊢B ⊢σ) ok
      (lamⱼ ⊢B ⊢t ok) PE.refl →
        lamⱼ (subst-⊢-⇑ ⊢B ⊢σ) (subst-⊢∷-⇑ ⊢t ⊢σ) ok
      (_∘ⱼ_ {G = B} ⊢t ⊢u) PE.refl →
        PE.subst (_⊢_∷_ _ _) (PE.sym $ singleSubstLift B _)
          (subst-⊢∷ ⊢t ⊢σ ∘ⱼ subst-⊢∷ ⊢u ⊢σ)
      (prodⱼ {G = B} ⊢B ⊢t ⊢u ok) PE.refl →
        prodⱼ (subst-⊢-⇑ ⊢B ⊢σ) (subst-⊢∷ ⊢t ⊢σ)
          (PE.subst (_⊢_∷_ _ _) (singleSubstLift B _) $
           subst-⊢∷ ⊢u ⊢σ)
          ok
      (fstⱼ ⊢B ⊢t) PE.refl →
        fstⱼ (subst-⊢-⇑ ⊢B ⊢σ) (subst-⊢∷ ⊢t ⊢σ)
      (sndⱼ {G = B} ⊢B ⊢t) PE.refl →
        PE.subst (_⊢_∷_ _ _) (PE.sym $ singleSubstLift B _) $
        sndⱼ (subst-⊢-⇑ ⊢B ⊢σ) (subst-⊢∷ ⊢t ⊢σ)
      (prodrecⱼ {A = C} ⊢C ⊢t ⊢u ok) PE.refl →
        PE.subst (_⊢_∷_ _ _) (PE.sym $ singleSubstLift C _) $
        prodrecⱼ (subst-⊢-⇑ ⊢C ⊢σ) (subst-⊢∷ ⊢t ⊢σ)
          (PE.subst (_⊢_∷_ _ _) (subst-β-prodrec C _) $
           subst-⊢∷-⇑ ⊢u ⊢σ)
          ok
      (Emptyⱼ _) _ →
        Emptyⱼ (wf-⊢ˢʷ∷ ⊢σ)
      (emptyrecⱼ ⊢A ⊢t) PE.refl →
        emptyrecⱼ (subst-⊢ ⊢A ⊢σ) (subst-⊢∷ ⊢t ⊢σ)
      (starⱼ _ ok) _ →
        starⱼ (wf-⊢ˢʷ∷ ⊢σ) ok
      (unitrecⱼ {A} ⊢A ⊢t ⊢u ok) PE.refl →
        PE.subst (_⊢_∷_ _ _) (PE.sym $ singleSubstLift A _) $
        unitrecⱼ (subst-⊢-⇑ ⊢A ⊢σ) (subst-⊢∷ ⊢t ⊢σ)
          (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
           subst-⊢∷ ⊢u ⊢σ)
          ok
      (Unitⱼ _ ok) _ →
        Unitⱼ (wf-⊢ˢʷ∷ ⊢σ) ok
      (ℕⱼ _) _ →
        ℕⱼ (wf-⊢ˢʷ∷ ⊢σ)
      (zeroⱼ _) _ →
        zeroⱼ (wf-⊢ˢʷ∷ ⊢σ)
      (sucⱼ ⊢t) PE.refl →
        sucⱼ (subst-⊢∷ ⊢t ⊢σ)
      (natrecⱼ {A} ⊢t ⊢u ⊢v) PE.refl →
        PE.subst (_⊢_∷_ _ _) (PE.sym $ singleSubstLift A _) $
        natrecⱼ
          (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
           subst-⊢∷ ⊢t ⊢σ)
          (PE.subst (_⊢_∷_ _ _) (natrecSucCase _ A) $
           subst-⊢∷-⇑ ⊢u ⊢σ)
          (subst-⊢∷ ⊢v ⊢σ)
      (Idⱼ ⊢A ⊢t ⊢u) PE.refl →
        Idⱼ (subst-⊢∷ ⊢A ⊢σ) (subst-⊢∷ ⊢t ⊢σ) (subst-⊢∷ ⊢u ⊢σ)
      (rflⱼ ⊢t) PE.refl →
        rflⱼ (subst-⊢∷ ⊢t ⊢σ)
      (Jⱼ {t} {A} {B} ⊢t ⊢B ⊢u ⊢v ⊢w) PE.refl →
        PE.subst (_⊢_∷_ _ _) (PE.sym $ [,]-[]-commute B) $
        Jⱼ (subst-⊢∷ ⊢t ⊢σ)
          (PE.subst₂ _⊢_
             (PE.cong (_∙_ _) $
              PE.cong₃ Id (wk1-liftSubst A) (wk1-liftSubst t) PE.refl)
             PE.refl $
           subst-⊢-⇑ ⊢B ⊢σ)
          (PE.subst (_⊢_∷_ _ _) ([,]-[]-commute B) $
           subst-⊢∷ ⊢u ⊢σ)
          (subst-⊢∷ ⊢v ⊢σ) (subst-⊢∷ ⊢w ⊢σ)
      (Kⱼ {B} ⊢B ⊢u ⊢v ok) PE.refl →
        PE.subst (_⊢_∷_ _ _) (PE.sym $ singleSubstLift B _) $
        Kⱼ (subst-⊢-⇑ ⊢B ⊢σ)
          (PE.subst (_⊢_∷_ _ _) (singleSubstLift B _) $
           subst-⊢∷ ⊢u ⊢σ)
          (subst-⊢∷ ⊢v ⊢σ) ok
      ([]-congⱼ ⊢A ⊢t ⊢u ⊢v ok) PE.refl →
        []-congⱼ (subst-⊢ ⊢A ⊢σ) (subst-⊢∷ ⊢t ⊢σ) (subst-⊢∷ ⊢u ⊢σ)
          (subst-⊢∷ ⊢v ⊢σ) ok

  opaque
    unfolding size-⊢∷

    -- A substitution lemma for _⊢_∷_ and _⊢_≡_∷_.

    subst-⊢∷→⊢≡∷′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      (⊢t : Γ ⊢ t ∷ A) →
      size-⊢∷ ⊢t PE.≡ s₂ →
      Δ ⊢ t [ σ₁ ] ≡ t [ σ₂ ] ∷ A [ σ₁ ]
    subst-⊢∷→⊢≡∷′ {σ₁} {σ₂} hyp σ₁≡σ₂ = let open Lemmas hyp in λ where
      (conv ⊢t B≡A) PE.refl →
        conv (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (subst-⊢≡ B≡A $
           refl-⊢ˢʷ≡∷ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₂ .proj₁))
      (var _ x∈) _ →
        subst-∷∈→⊢≡∷ x∈ σ₁≡σ₂
      (Uⱼ _) _ →
        refl (Uⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁))
      (ΠΣⱼ ⊢A ⊢B ok) PE.refl →
        ΠΣ-cong (subst-⊢∷→⊢≡∷ ⊢A σ₁≡σ₂) (subst-⊢∷→⊢≡∷-⇑ ⊢B σ₁≡σ₂) ok
      (lamⱼ ⊢B ⊢t ok) PE.refl →
        let _ , ⊢A      = ∙⊢∷→⊢-<ˢ ⊢t
            _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
            _ , _ , σ₂⇑ = wf-⊢ˢʷ≡∷ (⊢ˢʷ≡∷-⇑-<ˢ ⊢A σ₁≡σ₂)
        in
        lam-cong (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷-⇑ ⊢t ⊢σ₁)
          (_⊢_∷_.conv (subst-⊢∷ ⊢t σ₂⇑) $
           _⊢_≡_.sym (subst-⊢→⊢≡-⇑ ⊢B σ₁≡σ₂))
          (subst-⊢∷→⊢≡∷-⇑ ⊢t σ₁≡σ₂) ok
      (_∘ⱼ_ {G = B} ⊢t ⊢u) PE.refl →
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B _)
          (app-cong (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂))
      (prodⱼ {G = B} ⊢B ⊢t ⊢u ok) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        prod-cong (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift B _) $
           subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂)
          ok
      (fstⱼ ⊢B ⊢t) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        fst-cong (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
      (sndⱼ {G = B} ⊢B ⊢t) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B _) $
        snd-cong (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
      (prodrecⱼ {A = C} ⊢C ⊢t ⊢u ok) PE.refl →
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift C _) $
        prodrec-cong (subst-⊢→⊢≡-⇑ ⊢C σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (subst-β-prodrec C _) $
           subst-⊢∷→⊢≡∷-⇑ ⊢u σ₁≡σ₂)
          ok
      (Emptyⱼ _) _ →
        refl (Emptyⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁))
      (emptyrecⱼ ⊢A ⊢t) PE.refl →
        emptyrec-cong (subst-⊢→⊢≡ ⊢A σ₁≡σ₂)
          (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
      (starⱼ _ ok) _ →
        refl (starⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁) ok)
      (unitrecⱼ {l} {A} {t} {u} {p} {q} ⊢A ⊢t ⊢u ok) PE.refl →
        let ⊢Δ , ⊢σ₁ , ⊢σ₂  = wf-⊢ˢʷ≡∷ σ₁≡σ₂
            u[σ₁]≡u[σ₂]     = PE.subst (_⊢_≡_∷_ _ _ _)
                                (singleSubstLift A _) $
                              subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂
        in
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift A _) $
        case Unitʷ-η? of λ where
          (no no-η) →
            unitrec-cong (subst-⊢→⊢≡-⇑ ⊢A σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
              u[σ₁]≡u[σ₂] ok no-η
          (yes η) →
            let ⊢t[σ₁] = subst-⊢∷ ⊢t ⊢σ₁ in
            unitrec l p q A t u [ σ₁ ]  ≡⟨ unitrec-β-η (subst-⊢-⇑ ⊢A ⊢σ₁) ⊢t[σ₁]
                                             (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
                                              subst-⊢∷ ⊢u ⊢σ₁)
                                             ok η ⟩⊢
            u [ σ₁ ]                    ≡⟨ _⊢_≡_∷_.conv u[σ₁]≡u[σ₂] $
                                           PE.subst₂ (_⊢_≡_ _)
                                             (PE.sym $ singleSubstComp _ _ A)
                                             (PE.sym $ singleSubstComp _ _ A) $
                                           subst-⊢→⊢≡ ⊢A $
                                           ⊢ˢʷ≡∷∙⇔ .proj₂
                                             ( refl-⊢ˢʷ≡∷ ⊢σ₁ , starⱼ ⊢Δ ok , ⊢t[σ₁]
                                             , η-unit (starⱼ ⊢Δ ok) ⊢t[σ₁] (inj₂ η)
                                             ) ⟩⊢
            u [ σ₂ ]                    ≡⟨ _⊢_≡_∷_.sym
                                             (PE.subst (_⊢_ _) (PE.sym $ singleSubstComp _ _ A) $
                                              subst-⊢ ⊢A (→⊢ˢʷ∷∙ ⊢σ₁ ⊢t[σ₁])) $
                                           _⊢_≡_∷_.conv
                                             (unitrec-β-η (subst-⊢-⇑ ⊢A ⊢σ₂) (subst-⊢∷ ⊢t ⊢σ₂)
                                                (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
                                                 subst-⊢∷ ⊢u ⊢σ₂)
                                                ok η)
                                             (PE.subst₂ (_⊢_≡_ _)
                                                (PE.sym $ singleSubstComp _ _ A)
                                                (PE.sym $ singleSubstComp _ _ A) $
                                              sym (subst-⊢→⊢≡ ⊢A (⊢ˢʷ≡∷-consSubst-[] σ₁≡σ₂ ⊢t))) ⟩⊢∎
            unitrec l p q A t u [ σ₂ ]  ∎
      (Unitⱼ _ ok) _ →
        refl (Unitⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁) ok)
      (ℕⱼ _) _ →
        refl (ℕⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁))
      (zeroⱼ _) _ →
        refl (zeroⱼ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₁))
      (sucⱼ ⊢t) PE.refl →
        suc-cong (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
      (natrecⱼ {A} ⊢t ⊢u ⊢v) PE.refl →
        let _ , ⊢A = ∙⊢∷→⊢-<ˢ ⊢u in
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift A _) $
        natrec-cong (subst-⊢→⊢≡-⇑-<ˢ ⊢A σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift A _) $
           subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (natrecSucCase _ A) $
           subst-⊢∷→⊢≡∷-⇑ ⊢u σ₁≡σ₂)
          (subst-⊢∷→⊢≡∷ ⊢v σ₁≡σ₂)
      (Idⱼ ⊢A ⊢t ⊢u) PE.refl →
        Id-cong (subst-⊢∷→⊢≡∷ ⊢A σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂)
      (rflⱼ ⊢t) PE.refl →
        _⊢_≡_∷_.refl $
        rflⱼ (subst-⊢∷ ⊢t (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₂ .proj₁))
      (Jⱼ {t} {A} {B} ⊢t ⊢B ⊢u ⊢v ⊢w) PE.refl →
        let _ , ⊢A , _  = ∙∙⊢→⊢-<ˢ ⊢B
            _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
        in
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ [,]-[]-commute B) $
        J-cong (subst-⊢→⊢≡-<ˢ ⊢A σ₁≡σ₂) (subst-⊢∷ ⊢t ⊢σ₁)
          (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (PE.subst₃ _⊢_≡_
             (PE.cong (_∙_ _) $
              PE.cong₃ Id (wk1-liftSubst A) (wk1-liftSubst t) PE.refl)
             PE.refl PE.refl $
           subst-⊢→⊢≡-⇑ ⊢B σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) ([,]-[]-commute B) $
           subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂)
          (subst-⊢∷→⊢≡∷ ⊢v σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢w σ₁≡σ₂)
      (Kⱼ {B} ⊢B ⊢u ⊢v ok) PE.refl →
        let _ , ⊢Id     = ∙⊢→⊢-<ˢ ⊢B
            ⊢A , ⊢t , _ = inversion-Id-⊢-<ˢ ⊢Id
        in
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B _) $
        K-cong (subst-⊢→⊢≡-<ˢ ⊢A σ₁≡σ₂) (subst-⊢∷→⊢≡∷-<ˢ ⊢t σ₁≡σ₂)
          (subst-⊢→⊢≡-⇑ ⊢B σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift B _) $
           subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂)
          (subst-⊢∷→⊢≡∷ ⊢v σ₁≡σ₂) ok
      ([]-congⱼ ⊢A ⊢t ⊢u ⊢v ok) PE.refl →
        []-cong-cong (subst-⊢→⊢≡ ⊢A σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
          (subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂) (subst-⊢∷→⊢≡∷ ⊢v σ₁≡σ₂) ok

  opaque
    unfolding size-⊢≡∷

    -- A substitution lemma for _⊢_≡_∷_.

    subst-⊢≡∷′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
      (t₁≡t₂ : Γ ⊢ t₁ ≡ t₂ ∷ A) →
      size-⊢≡∷ t₁≡t₂ PE.≡ s₂ →
      Δ ⊢ t₁ [ σ₁ ] ≡ t₂ [ σ₂ ] ∷ A [ σ₁ ]
    subst-⊢≡∷′ {σ₁} {σ₂} hyp σ₁≡σ₂ = let open Lemmas hyp in λ where
      (refl ⊢t) PE.refl →
        subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂
      (sym ⊢A t₂≡t₁) PE.refl →
        let ⊢Γ    = wfEqTerm-<ˢ t₂≡t₁
            σ₂≡σ₁ = sym-⊢ˢʷ≡∷-<ˢ ⊢Γ σ₁≡σ₂
        in
        conv
          (sym (subst-⊢ ⊢A (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₂ .proj₂))
             (subst-⊢≡∷ t₂≡t₁ σ₂≡σ₁))
          (sym (subst-⊢→⊢≡ ⊢A σ₁≡σ₂))
      (trans t₁≡t₂ t₂≡t₃) PE.refl →
        trans
          (subst-⊢≡∷ t₁≡t₂ $
           refl-⊢ˢʷ≡∷ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₂ .proj₁))
          (subst-⊢≡∷ t₂≡t₃ σ₁≡σ₂)
      (conv t₁≡t₂ B≡A) PE.refl →
        conv (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (subst-⊢≡ B≡A $
           refl-⊢ˢʷ≡∷ (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₂ .proj₁))
      (ΠΣ-cong A₁≡A₂ B₁≡B₂ ok) PE.refl →
        ΠΣ-cong (subst-⊢≡∷ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡∷-⇑ B₁≡B₂ σ₁≡σ₂) ok
      (app-cong {G = B} t₁≡t₂ u₁≡u₂) PE.refl →
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B _) $
        app-cong (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂) (subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂)
      (β-red {G = B} {t} {a = u} {p} ⊢B ⊢t ⊢u PE.refl ok) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
                                             ∷ B [ u ]₀ [ σ₁ ]            ⟨ singleSubstLift B _ ⟩≡∷≡
        lam p (t [ σ₁ ⇑ ]) ∘⟨ p ⟩ (u [ σ₁ ]) ∷ B [ σ₁ ⇑ ] [ u [ σ₁ ] ]₀  ≡⟨ β-red (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷-⇑ ⊢t ⊢σ₁)
                                                                              (subst-⊢∷ ⊢u ⊢σ₁) PE.refl ok ⟩⊢∷
        t [ σ₁ ⇑ ] [ u [ σ₁ ] ]₀                                         ≡⟨ singleSubstComp _ _ t ⟩⊢≡
                                                                          ⟨ singleSubstComp _ _ B ⟩≡≡
        t [ consSubst σ₁ (u [ σ₁ ]) ] ∷ B [ consSubst σ₁ (u [ σ₁ ]) ]    ≡⟨ subst-⊢∷→⊢≡∷ ⊢t $
                                                                            ⊢ˢʷ≡∷-consSubst-[] σ₁≡σ₂ ⊢u ⟩⊢∷∎≡
        t [ consSubst σ₂ (u [ σ₂ ]) ]                                    ≡˘⟨ PE.trans (singleSubstLift t _) (singleSubstComp _ _ t) ⟩
        t [ u ]₀ [ σ₂ ]                                                  ∎
      (η-eq {f = t₁} {g = t₂} ⊢B ⊢t₁ ⊢t₂ t₁0≡t₂0 ok) PE.refl →
        let _ , ⊢A        = ∙⊢≡∷→⊢-<ˢ t₁0≡t₂0
            _ , ⊢σ₁ , ⊢σ₂ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
        in
        η-eq (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷ ⊢t₁ ⊢σ₁)
          (_⊢_∷_.conv (subst-⊢∷ ⊢t₂ ⊢σ₂) $
           _⊢_≡_.sym $
           ΠΣ-cong (subst-⊢→⊢≡-<ˢ ⊢A σ₁≡σ₂) (subst-⊢→⊢≡-⇑ ⊢B σ₁≡σ₂) ok)
          (PE.subst₃ (_⊢_≡_∷_ _)
             (PE.cong (_∘⟨ _ ⟩ _) (wk1-liftSubst t₁))
             (PE.cong (_∘⟨ _ ⟩ _) (wk1-liftSubst t₂))
             PE.refl $
           subst-⊢≡∷-⇑ t₁0≡t₂0 σ₁≡σ₂)
          ok
      (fst-cong ⊢B t₁≡t₂) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        fst-cong (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
      (snd-cong {G = B} ⊢B t₁≡t₂) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B _) $
        snd-cong (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
      (Σ-β₁ {G = B} {t} {u} {p} ⊢B ⊢t ⊢u PE.refl ok) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        fst p (prodˢ p t u) [ σ₁ ]  ≡⟨ Σ-β₁ (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷ ⊢t ⊢σ₁)
                                         (PE.subst (_⊢_∷_ _ _) (singleSubstLift B _) $
                                          subst-⊢∷ ⊢u ⊢σ₁)
                                         PE.refl ok ⟩⊢
        t [ σ₁ ]                    ≡⟨ subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂ ⟩⊢∎
        t [ σ₂ ]                    ∎
      (Σ-β₂ {G = B} {t} {u} {p} ⊢B ⊢t ⊢u PE.refl ok) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
            ⊢B[σ₁⇑]     = subst-⊢-⇑ ⊢B ⊢σ₁
            ⊢t[σ₁]      = subst-⊢∷ ⊢t ⊢σ₁
            ⊢u[σ₁]      = PE.subst (_⊢_∷_ _ _) (singleSubstLift B _) $
                          subst-⊢∷ ⊢u ⊢σ₁
        in
        snd p (prodˢ p t u) [ σ₁ ] ∷ B [ fst p (prodˢ p t u) ]₀ [ σ₁ ]  ≡⟨ PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B _) $
                                                                           Σ-β₂ ⊢B[σ₁⇑] ⊢t[σ₁] ⊢u[σ₁] PE.refl ok ⟩⊢∷
                                                                         ⟨ PE.subst₂ (_⊢_≡_ _)
                                                                             (PE.sym $ substCompEq B) (PE.sym $ substCompEq B) $
                                                                           subst-⊢→⊢≡ ⊢B $
                                                                           ⊢ˢʷ≡∷∙⇔ .proj₂
                                                                             ( refl-⊢ˢʷ≡∷ ⊢σ₁
                                                                             , fstⱼ ⊢B[σ₁⇑] (prodⱼ ⊢B[σ₁⇑] ⊢t[σ₁] ⊢u[σ₁] ok)
                                                                             , ⊢t[σ₁]
                                                                             , Σ-β₁ ⊢B[σ₁⇑] ⊢t[σ₁] ⊢u[σ₁] PE.refl ok
                                                                             ) ⟩≡
        u [ σ₁ ] ∷ B [ t ]₀ [ σ₁ ]                                      ≡⟨ subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂ ⟩⊢∷∎
        u [ σ₂ ]                                                        ∎
      (Σ-η {G = B} ⊢B ⊢t₁ ⊢t₂ fst-t₁≡fst-t₂ snd-t₁≡snd-t₂ ok) PE.refl →
        let _ , ⊢A        = ∙⊢→⊢-<ˢ ⊢B
            _ , ⊢σ₁ , ⊢σ₂ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
        in
        Σ-η (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢∷ ⊢t₁ ⊢σ₁)
          (_⊢_∷_.conv (subst-⊢∷ ⊢t₂ ⊢σ₂) $
           _⊢_≡_.sym $
           ΠΣ-cong (subst-⊢→⊢≡-<ˢ ⊢A σ₁≡σ₂) (subst-⊢→⊢≡-⇑ ⊢B σ₁≡σ₂) ok)
          (subst-⊢≡∷ fst-t₁≡fst-t₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift B _) $
           subst-⊢≡∷ snd-t₁≡snd-t₂ σ₁≡σ₂)
          ok
      (prod-cong {G = B} ⊢B t₁≡t₂ u₁≡u₂ ok) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        prod-cong (subst-⊢-⇑ ⊢B ⊢σ₁) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift B _) $
           subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂)
          ok
      (prodrec-cong {A = C} C₁≡C₂ t₁≡t₂ u₁≡u₂ ok) PE.refl →
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift C _) $
        prodrec-cong (subst-⊢≡-⇑ C₁≡C₂ σ₁≡σ₂) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (subst-β-prodrec C _) $
           subst-⊢≡∷-⇑ u₁≡u₂ σ₁≡σ₂)
          ok
      (prodrec-β
         {p} {G = B} {A = C} {t} {t′ = u} {u = v} {r} {q}
         ⊢C ⊢t ⊢u ⊢v PE.refl ok)
        PE.refl →
        let _ , ⊢σ₁ , ⊢σ₂ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
          ∷ C [ prodʷ p t u ]₀ [ σ₁ ]                       ⟨ singleSubstLift C _ ⟩≡∷≡

        prodrec r p q C (prodʷ p t u) v [ σ₁ ]
          ∷ C [ σ₁ ⇑ ] [ prodʷ p (t [ σ₁ ]) (u [ σ₁ ]) ]₀  ≡⟨ prodrec-β (subst-⊢-⇑ ⊢C ⊢σ₁) (subst-⊢∷ ⊢t ⊢σ₁)
                                                                (PE.subst (_⊢_∷_ _ _) (singleSubstLift B _) $
                                                                 subst-⊢∷ ⊢u ⊢σ₁)
                                                                (PE.subst (_⊢_∷_ _ _) (subst-β-prodrec C _) $
                                                                 subst-⊢∷-⇑ ⊢v ⊢σ₁)
                                                                PE.refl ok ⟩⊢∷

        v [ σ₁ ⇑[  ] ] [ t [ σ₁ ] , u [ σ₁ ] ]₁₀          ≡˘⟨ [,]-[]-commute v ⟩⊢≡

        v [ t , u ]₁₀ [ σ₁ ]                               ≡⟨ PE.subst₃ (_⊢_≡_∷_ _)
                                                                (PE.sym $ [,]-[]-fusion v) (PE.sym $ [,]-[]-fusion v)
                                                                (PE.sym $ substCompProdrec C _ _ _) $
                                                              subst-⊢∷→⊢≡∷ ⊢v $
                                                              ⊢ˢʷ≡∷∙⇔ .proj₂
                                                                ( ⊢ˢʷ≡∷-consSubst-[] σ₁≡σ₂ ⊢t
                                                                , PE.subst (_⊢_∷_ _ _) (PE.sym $ substConsId B)
                                                                    (subst-⊢∷ ⊢u ⊢σ₁)
                                                                , PE.subst (_⊢_∷_ _ _) (PE.sym $ substConsId B)
                                                                    (subst-⊢∷ ⊢u ⊢σ₂)
                                                                , PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ substConsId B)
                                                                    (subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂)
                                                                ) ⟩⊢∎
        v [ t , u ]₁₀ [ σ₂ ]                               ∎
      (emptyrec-cong A₁≡A₂ t₁≡t₂) PE.refl →
        emptyrec-cong (subst-⊢≡ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
      (unitrec-cong {A = A₁} A₁≡A₂ t₁≡t₂ u₁≡u₂ ok no-η) PE.refl →
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift A₁ _) $
        unitrec-cong (subst-⊢≡-⇑ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift A₁ _) $
           subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂)
          ok no-η
      (unitrec-β {l} {A} {u = t} {p} {q} ⊢A ⊢t ok no-η) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        unitrec l p q A (starʷ l) t [ σ₁ ]  ≡⟨ PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift A _) $
                                               unitrec-β (subst-⊢-⇑ ⊢A ⊢σ₁)
                                                 (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
                                                  subst-⊢∷ ⊢t ⊢σ₁)
                                                 ok no-η ⟩⊢
        t [ σ₁ ]                            ≡⟨ subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂ ⟩⊢∎
        t [ σ₂ ]                            ∎
      (unitrec-β-η {l} {A} {t} {u} {p} {q} ⊢A ⊢t ⊢u ok no-η) PE.refl →
        let ⊢Δ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
            ⊢t[σ₁]       = subst-⊢∷ ⊢t ⊢σ₁
        in
        unitrec l p q A t u [ σ₁ ] ∷ A [ t ]₀ [ σ₁ ]  ≡⟨ PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift A _) $
                                                         unitrec-β-η (subst-⊢-⇑ ⊢A ⊢σ₁) ⊢t[σ₁]
                                                           (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
                                                            subst-⊢∷ ⊢u ⊢σ₁)
                                                           ok no-η ⟩⊢∷
                                                       ⟨ PE.subst₂ (_⊢_≡_ _)
                                                           (PE.sym $ substCompEq A) (PE.sym $ substCompEq A) $
                                                         subst-⊢→⊢≡ ⊢A $
                                                         ⊢ˢʷ≡∷∙⇔ .proj₂
                                                           ( refl-⊢ˢʷ≡∷ ⊢σ₁ , ⊢t[σ₁] , starⱼ ⊢Δ ok
                                                           , η-unit ⊢t[σ₁] (starⱼ ⊢Δ ok) (inj₂ no-η)
                                                           ) ⟩≡
        u [ σ₁ ] ∷ A [ starʷ l ]₀ [ σ₁ ]              ≡⟨ subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂ ⟩⊢∷∎
        u [ σ₂ ]                                      ∎
      (η-unit ⊢t₁ ⊢t₂ η) PE.refl →
        let _ , ⊢σ₁ , ⊢σ₂ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        η-unit (subst-⊢∷ ⊢t₁ ⊢σ₁) (subst-⊢∷ ⊢t₂ ⊢σ₂) η
      (suc-cong t₁≡t₂) PE.refl →
        suc-cong (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
      (natrec-cong {A = A₁} A₁≡A₂ t₁≡t₂ u₁≡u₂ v₁≡v₂) PE.refl →
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift A₁ _) $
        natrec-cong (subst-⊢≡-⇑ A₁≡A₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift A₁ _) $
           subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (natrecSucCase _ A₁) $
           subst-⊢≡∷-⇑ u₁≡u₂ σ₁≡σ₂)
          (subst-⊢≡∷ v₁≡v₂ σ₁≡σ₂)
      (natrec-zero {z = t} {A} {s = u} {p} {q} {r} ⊢t ⊢u) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        natrec p q r A t u zero [ σ₁ ]  ≡⟨ PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift A _) $
                                           natrec-zero
                                             (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
                                              subst-⊢∷ ⊢t ⊢σ₁)
                                             (PE.subst (_⊢_∷_ _ _) (natrecSucCase _ A) $
                                              subst-⊢∷-⇑ ⊢u ⊢σ₁) ⟩⊢
        t [ σ₁ ]                        ≡⟨ subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂ ⟩⊢∎
        t [ σ₂ ]                        ∎
      (natrec-suc {z = t} {A} {s = u} {p} {q} {r} {n = v} ⊢t ⊢u ⊢v)
        PE.refl →
        let _ , ⊢A        = ∙⊢∷→⊢-<ˢ ⊢u
            _ , ⊢σ₁ , ⊢σ₂ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
            ⊢t[σ₁]        = PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
                            subst-⊢∷ ⊢t ⊢σ₁
            ⊢u[σ₁⇑²]      = PE.subst (_⊢_∷_ _ _) (natrecSucCase _ A) $
                            subst-⊢∷-⇑ ⊢u ⊢σ₁
            ⊢v[σ₁]        = subst-⊢∷ ⊢v ⊢σ₁
        in
                                          ∷ A [ suc v ]₀ [ σ₁ ]            ⟨ singleSubstLift A _ ⟩≡∷≡

        natrec p q r A t u (suc v) [ σ₁ ] ∷ A [ σ₁ ⇑ ] [ suc v [ σ₁ ] ]₀  ≡⟨ natrec-suc ⊢t[σ₁] ⊢u[σ₁⇑²] ⊢v[σ₁] ⟩⊢∷

        u [ σ₁ ⇑[  ] ] [ v [ σ₁ ] , natrec p q r A t u v [ σ₁ ] ]₁₀      ≡⟨ doubleSubstComp u _ _ _ ⟩⊢≡
                                                                           ⟨ PE.trans (singleSubstComp _ _ A) (substComp↑² A _) ⟩≡≡
        u [ consSubst (consSubst σ₁ (v [ σ₁ ]))
              (natrec p q r A t u v [ σ₁ ])
          ]
          ∷ A [ suc (var x1) ]↑²
              [ consSubst (consSubst σ₁ (v [ σ₁ ]))
                  (natrec p q r A t u v [ σ₁ ]) ]                         ≡⟨ subst-⊢∷→⊢≡∷ ⊢u $
                                                                             ⊢ˢʷ≡∷∙⇔ .proj₂
                                                                               ( ⊢ˢʷ≡∷-consSubst-[] σ₁≡σ₂ ⊢v
                                                                               , PE.subst (_⊢_∷_ _ _) (singleSubstComp _ _ A)
                                                                                   (natrecⱼ ⊢t[σ₁] ⊢u[σ₁⇑²] ⊢v[σ₁])
                                                                               , PE.subst (_⊢_∷_ _ _) (singleSubstComp _ _ A)
                                                                                   (natrecⱼ
                                                                                      (PE.subst (_⊢_∷_ _ _) (singleSubstLift A _) $
                                                                                       subst-⊢∷ ⊢t ⊢σ₂)
                                                                                      (PE.subst (_⊢_∷_ _ _) (natrecSucCase _ A) $
                                                                                       subst-⊢∷-⇑ ⊢u ⊢σ₂)
                                                                                      (subst-⊢∷ ⊢v ⊢σ₂))
                                                                               , PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstComp _ _ A)
                                                                                   (natrec-cong (subst-⊢→⊢≡-⇑-<ˢ ⊢A σ₁≡σ₂)
                                                                                      (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift A _) $
                                                                                       subst-⊢∷→⊢≡∷ ⊢t σ₁≡σ₂)
                                                                                      (PE.subst (_⊢_≡_∷_ _ _ _) (natrecSucCase _ A) $
                                                                                       subst-⊢∷→⊢≡∷-⇑ ⊢u σ₁≡σ₂)
                                                                                      (subst-⊢∷→⊢≡∷ ⊢v σ₁≡σ₂))
                                                                               ) ⟩⊢∷∎≡
        u [ consSubst (consSubst σ₂ (v [ σ₂ ]))
              (natrec p q r A t u v [ σ₂ ]) ]                             ≡˘⟨ [,]-[]-fusion u ⟩

        u [ v , natrec p q r A t u v ]₁₀ [ σ₂ ]                           ∎
      (Id-cong A₁≡A₂ t₁≡t₂ u₁≡u₂) PE.refl →
        Id-cong (subst-⊢≡∷ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂)
      (J-cong {A₁} {t₁} {B₁} A₁≡A₂ ⊢t₁ t₁≡t₂ B₁≡B₂ u₁≡u₂ v₁≡v₂ w₁≡w₂)
        PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ [,]-[]-commute B₁) $
        J-cong (subst-⊢≡ A₁≡A₂ σ₁≡σ₂) (subst-⊢∷ ⊢t₁ ⊢σ₁)
          (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (PE.subst₃ _⊢_≡_
             (PE.cong (_∙_ _) $
              PE.cong₃ Id (wk1-liftSubst A₁) (wk1-liftSubst t₁) PE.refl)
             PE.refl PE.refl $
           subst-⊢≡-⇑ B₁≡B₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) ([,]-[]-commute B₁) $
           subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂)
          (subst-⊢≡∷ v₁≡v₂ σ₁≡σ₂) (subst-⊢≡∷ w₁≡w₂ σ₁≡σ₂)
      (J-β {t} {A} {B} {u} {p} {q} ⊢t ⊢B ⊢u PE.refl) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        J p q A t B u t rfl [ σ₁ ]  ≡⟨ PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ [,]-[]-commute B) $
                                       J-β (subst-⊢∷ ⊢t ⊢σ₁)
                                         (PE.subst₂ _⊢_
                                            (PE.cong (_∙_ _) $
                                             PE.cong₃ Id (wk1-liftSubst A) (wk1-liftSubst t) PE.refl)
                                            PE.refl $
                                          subst-⊢-⇑ ⊢B ⊢σ₁)
                                         (PE.subst (_⊢_∷_ _ _) ([,]-[]-commute B) $
                                          subst-⊢∷ ⊢u ⊢σ₁)
                                         PE.refl ⟩⊢
        u [ σ₁ ]                    ≡⟨ subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂ ⟩⊢∎
        u [ σ₂ ]                    ∎
      (K-cong {B₁} A₁≡A₂ t₁≡t₂ B₁≡B₂ u₁≡u₂ v₁≡v₂ ok) PE.refl →
        PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B₁ _) $
        K-cong (subst-⊢≡ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (subst-⊢≡-⇑ B₁≡B₂ σ₁≡σ₂)
          (PE.subst (_⊢_≡_∷_ _ _ _) (singleSubstLift B₁ _) $
           subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂)
          (subst-⊢≡∷ v₁≡v₂ σ₁≡σ₂) ok
      (K-β {A} {t} {B} {u} {p} ⊢B ⊢u ok) PE.refl →
        let _ , ⊢σ₁ , _ = wf-⊢ˢʷ≡∷ σ₁≡σ₂ in
        K p A t B u rfl [ σ₁ ]  ≡⟨ PE.subst (_⊢_≡_∷_ _ _ _) (PE.sym $ singleSubstLift B _) $
                                   K-β (subst-⊢-⇑ ⊢B ⊢σ₁)
                                     (PE.subst (_⊢_∷_ _ _) (singleSubstLift B _) $
                                      subst-⊢∷ ⊢u ⊢σ₁)
                                     ok ⟩⊢
        u [ σ₁ ]                ≡⟨ subst-⊢∷→⊢≡∷ ⊢u σ₁≡σ₂ ⟩⊢∎
        u [ σ₂ ]                ∎
      ([]-cong-cong A₁≡A₂ t₁≡t₂ u₁≡u₂ v₁≡v₂ ok) PE.refl →
        []-cong-cong (subst-⊢≡ A₁≡A₂ σ₁≡σ₂) (subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂)
          (subst-⊢≡∷ u₁≡u₂ σ₁≡σ₂) (subst-⊢≡∷ v₁≡v₂ σ₁≡σ₂) ok
      ([]-cong-β ⊢t PE.refl ok) PE.refl →
        []-cong-β (subst-⊢∷ ⊢t (wf-⊢ˢʷ≡∷ σ₁≡σ₂ .proj₂ .proj₁)) PE.refl
          ok
      (equality-reflection ok ⊢Id ⊢v) PE.refl →
        let ⊢A , ⊢t , ⊢u  = inversion-Id-⊢ ⊢Id
            _ , ⊢σ₁ , ⊢σ₂ = wf-⊢ˢʷ≡∷ σ₁≡σ₂
            ⊢A[σ₁]        = subst-⊢-<ˢ ⊢A ⊢σ₁
            ⊢t[σ₁]        = subst-⊢∷-<ˢ ⊢t ⊢σ₁
        in
        equality-reflection ok
          (Idⱼ ⊢A[σ₁] ⊢t[σ₁] $
           conv (subst-⊢∷-<ˢ ⊢u ⊢σ₂) (sym (subst-⊢→⊢≡-<ˢ ⊢A σ₁≡σ₂)))
          (_⊢_∷_.conv (subst-⊢∷ ⊢v ⊢σ₁) $
           Id-cong (refl ⊢A[σ₁]) (refl ⊢t[σ₁])
             (subst-⊢∷→⊢≡∷-<ˢ ⊢u σ₁≡σ₂))

  opaque

    -- The type P s is inhabited for every s.

    P-inhabited : P s
    P-inhabited =
      well-founded-induction P
        (λ _ hyp →
           record
             { sym-⊢ˢʷ≡∷    = sym-⊢ˢʷ≡∷′    hyp
             ; subst-⊢      = subst-⊢′      hyp
             ; subst-⊢→⊢≡   = subst-⊢→⊢≡′   hyp
             ; subst-⊢≡     = subst-⊢≡′     hyp
             ; subst-⊢∷     = subst-⊢∷′     hyp
             ; subst-⊢∷→⊢≡∷ = subst-⊢∷→⊢≡∷′ hyp
             ; subst-⊢≡∷    = subst-⊢≡∷′    hyp
             })
        _

private
  module L {s} = Lemmas {s₂ = s} (λ _ → Inhabited.P-inhabited)

opaque

  -- A substitution lemma for _⊢_.

  subst-⊢ : Γ ⊢ A → Δ ⊢ˢʷ σ ∷ Γ → Δ ⊢ A [ σ ]
  subst-⊢ ⊢A ⊢σ = P.subst-⊢ Inhabited.P-inhabited ⊢σ ⊢A PE.refl

opaque

  -- A substitution lemma for _⊢_≡_.

  subst-⊢≡ : Γ ⊢ A₁ ≡ A₂ → Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ → Δ ⊢ A₁ [ σ₁ ] ≡ A₂ [ σ₂ ]
  subst-⊢≡ A₁≡A₂ σ₁≡σ₂ =
    P.subst-⊢≡ Inhabited.P-inhabited σ₁≡σ₂ A₁≡A₂ PE.refl

opaque

  -- A substitution lemma for _⊢_∷_.

  subst-⊢∷ : Γ ⊢ t ∷ A → Δ ⊢ˢʷ σ ∷ Γ → Δ ⊢ t [ σ ] ∷ A [ σ ]
  subst-⊢∷ ⊢t ⊢σ = P.subst-⊢∷ Inhabited.P-inhabited ⊢σ ⊢t PE.refl

opaque

  -- A substitution lemma for _⊢_≡_∷_.

  subst-⊢≡∷ :
    Γ ⊢ t₁ ≡ t₂ ∷ A → Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    Δ ⊢ t₁ [ σ₁ ] ≡ t₂ [ σ₂ ] ∷ A [ σ₁ ]
  subst-⊢≡∷ t₁≡t₂ σ₁≡σ₂ =
    P.subst-⊢≡∷ Inhabited.P-inhabited σ₁≡σ₂ t₁≡t₂ PE.refl

opaque

  -- A substitution lemma related to _⇑[_].

  subst-⊢-⇑ :
    Γ ⊢ A → Δ ⊢ˢʷ σ ∷ drop k Γ → Δ ∙[ k ][ Γ ][ σ ] ⊢ A [ σ ⇑[ k ] ]
  subst-⊢-⇑ ⊢A = L.subst-⊢-⇑ ⊢A ⦃ lt = ∃-<ˢ .proj₂ ⦄

opaque

  -- A substitution lemma related to _⇑[_].

  subst-⊢∷-⇑ :
    Γ ⊢ t ∷ A → Δ ⊢ˢʷ σ ∷ drop k Γ →
    Δ ∙[ k ][ Γ ][ σ ] ⊢ t [ σ ⇑[ k ] ] ∷ A [ σ ⇑[ k ] ]
  subst-⊢∷-⇑ ⊢t = L.subst-⊢∷-⇑ ⊢t ⦃ lt = ∃-<ˢ .proj₂ ⦄

opaque

  -- A substitution lemma related to _⇑[_].

  subst-⊢≡-⇑ :
    Γ ⊢ A ≡ B → Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
    Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ A [ σ₁ ⇑[ k ] ] ≡ B [ σ₂ ⇑[ k ] ]
  subst-⊢≡-⇑ A≡B = L.subst-⊢≡-⇑ A≡B ⦃ lt = ∃-<ˢ .proj₂ ⦄

opaque

  -- A substitution lemma related to _⇑[_].

  subst-⊢≡∷-⇑ :
    Γ ⊢ t ≡ u ∷ A → Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
    Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ t [ σ₁ ⇑[ k ] ] ≡ u [ σ₂ ⇑[ k ] ] ∷
      A [ σ₁ ⇑[ k ] ]
  subst-⊢≡∷-⇑ t≡u = L.subst-⊢≡∷-⇑ t≡u ⦃ lt = ∃-<ˢ .proj₂ ⦄

------------------------------------------------------------------------
-- More lemmas related to _⊢ˢʷ_∷_ and _⊢ˢʷ_≡_∷_

opaque

  -- Symmetry for _⊢ˢʷ_≡_∷_.

  sym-⊢ˢʷ≡∷ :
    ⊢ Γ →
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    Δ ⊢ˢʷ σ₂ ≡ σ₁ ∷ Γ
  sym-⊢ˢʷ≡∷ ⊢Γ = P.sym-⊢ˢʷ≡∷ Inhabited.P-inhabited ⊢Γ PE.refl

opaque

  -- A variant of ⊢ˢʷ∷-⇑.

  ⊢ˢʷ∷-⇑′ :
    Γ ⊢ A →
    Δ ⊢ˢʷ σ ∷ Γ →
    Δ ∙ A [ σ ] ⊢ˢʷ σ ⇑ ∷ Γ ∙ A
  ⊢ˢʷ∷-⇑′ ⊢A =
    L.⊢ˢʷ∷-⇑-<ˢ (⊢A , ∃-<ˢ .proj₂) ⦃ lt = ∃-<ˢ .proj₂ ⦄

opaque

  -- A variant of ⊢ˢʷ≡∷-⇑.

  ⊢ˢʷ≡∷-⇑′ :
    Γ ⊢ A →
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ Γ →
    Δ ∙ A [ σ₁ ] ⊢ˢʷ σ₁ ⇑ ≡ σ₂ ⇑ ∷ Γ ∙ A
  ⊢ˢʷ≡∷-⇑′ ⊢A =
    L.⊢ˢʷ≡∷-⇑-<ˢ (⊢A , ∃-<ˢ .proj₂) ⦃ lt = ∃-<ˢ .proj₂ ⦄

opaque

  -- A variant of ⊢ˢʷ∷-⇑.

  ⊢ˢʷ∷-⇑[] :
    ⊢ Γ →
    Δ ⊢ˢʷ σ ∷ drop k Γ →
    Δ ∙[ k ][ Γ ][ σ ] ⊢ˢʷ σ ⇑[ k ] ∷ Γ
  ⊢ˢʷ∷-⇑[] ⊢Γ =
    L.⊢ˢʷ∷-⇑[]-<ˢ (⊢Γ , ∃-<ˢ .proj₂) ⦃ lt = ∃-<ˢ .proj₂ ⦄

opaque

  -- A variant of ⊢ˢʷ≡∷-⇑.

  ⊢ˢʷ≡∷-⇑[] :
    ⊢ Γ →
    Δ ⊢ˢʷ σ₁ ≡ σ₂ ∷ drop k Γ →
    Δ ∙[ k ][ Γ ][ σ₁ ] ⊢ˢʷ σ₁ ⇑[ k ] ≡ σ₂ ⇑[ k ] ∷ Γ
  ⊢ˢʷ≡∷-⇑[] ⊢Γ =
    L.⊢ˢʷ≡∷-⇑[]-<ˢ (⊢Γ , ∃-<ˢ .proj₂) ⦃ lt = ∃-<ˢ .proj₂ ⦄