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

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

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

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
import Definition.Typed.Substitution.Primitive.Primitive R as P
open import Definition.Typed.Weakening R
open import Definition.Typed.Well-formed R

open import Definition.Untyped M as U hiding (wk)
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 P public
  hiding (lam-cong; lift-cong; βŠ’Λ’Κ·β‰‘βˆ·-⇑; βŠ’Λ’Κ·β‰‘βˆ·-sgSubst; βŠ’Λ’Κ·β‰‘βˆ·-[][]↑)

private variable
  βˆ‡                                             : DCon (Term 0) _
  k n                                           : Nat
  Ξ” Ξ— Ξ¦                                         : Con Term _
  Ξ“                                             : Cons _ _
  𝓙                                             : Judgement _
  A B B₁ Bβ‚‚ C C₁ Cβ‚‚ D E t t₁ tβ‚‚ u u₁ uβ‚‚ v v₁ vβ‚‚ : Term _
  Οƒ σ₁ σ₁₁ σ₁₂ Οƒβ‚‚ σ₂₁ Οƒβ‚‚β‚‚ σ₃                    : Subst _ _
  s                                             : Strength
  p q                                           : M

------------------------------------------------------------------------
-- Lemmas related to _⊒˒ʷ_∷_ and _⊒˒ʷ_≑_∷_

opaque

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

  βŠ’Λ’Κ·β‰‘βˆ·β‡”β€² :
    βˆ‡ »⊒ Ξ” β†’ βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ Οƒβ‚‚ ∷ Ξ” ⇔ (βˆ‡ »⊒ Ξ— Γ— βˆ‡ Β» Ξ— ⊒˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ”)
  βŠ’Λ’Κ·β‰‘βˆ·β‡”β€² {βˆ‡} {Ξ”} {Ξ—} {σ₁} {Οƒβ‚‚} βŠ’Ξ” =
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ Οƒβ‚‚ ∷ Ξ”                                              β‡”βŸ¨ βŠ’Λ’Κ·β‰‘βˆ·β‡” ⟩
    βˆ‡ »⊒ Ξ— Γ— βˆ‡ Β» Ξ— ⊒˒ σ₁ ∷ Ξ” Γ— βˆ‡ Β» Ξ— ⊒˒ Οƒβ‚‚ ∷ Ξ” Γ— βˆ‡ Β» Ξ— ⊒˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ”  β‡”βŸ¨ (Ξ» (βŠ’Ξ— , _ , _ , σ₁≑σ₂) β†’ βŠ’Ξ— , σ₁≑σ₂)
                                                                        , (Ξ» (βŠ’Ξ— , σ₁≑σ₂) β†’
                                                                              let βŠ’Οƒβ‚ , βŠ’Οƒβ‚‚ = wf-βŠ’Λ’β‰‘βˆ· βŠ’Ξ” σ₁≑σ₂ in
                                                                              βŠ’Ξ— , βŠ’Οƒβ‚ , βŠ’Οƒβ‚‚ , σ₁≑σ₂)
                                                                        ⟩
    βˆ‡ »⊒ Ξ— Γ— βˆ‡ Β» Ξ— ⊒˒ σ₁ ≑ Οƒβ‚‚ ∷ Ξ”                                      ░⇔

opaque

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

  βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡”β€² :
    βˆ‡ Β» Ξ” ⊒ A β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ Οƒβ‚‚ ∷ Ξ” βˆ™ A ⇔
    (βˆ‡ Β» Ξ— ⊒˒ʷ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ” Γ—
     βˆ‡ Β» Ξ— ⊒ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ])
  βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡”β€² {βˆ‡} {Ξ”} {A} {Ξ—} {σ₁} {Οƒβ‚‚} ⊒A =
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ Οƒβ‚‚ ∷ Ξ” βˆ™ A                    β‡”βŸ¨ βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡” ⟩

    βˆ‡ Β» Ξ— ⊒˒ʷ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ” Γ—
    βˆ‡ Β» Ξ— ⊒ head σ₁ ∷ A [ tail σ₁ ] Γ—
    βˆ‡ Β» Ξ— ⊒ head Οƒβ‚‚ ∷ A [ tail Οƒβ‚‚ ] Γ—
    βˆ‡ Β» Ξ— ⊒ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]    β‡”βŸ¨ (Ξ» (Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š , _ , _ , σ₁₀≑σ₂₀) β†’
                                                        Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š , σ₁₀≑σ₂₀)
                                                  , (Ξ» (Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š , σ₁₀≑σ₂₀) β†’
                                                        let _ , βŠ’Οƒβ‚β‚€ , βŠ’Οƒβ‚‚β‚€ = wf-⊒ σ₁₀≑σ₂₀ in
                                                        Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š , βŠ’Οƒβ‚β‚€ , conv βŠ’Οƒβ‚‚β‚€ (subst-βŠ’β‰‘ (refl ⊒A) Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š) , σ₁₀≑σ₂₀)
                                                  ⟩

    βˆ‡ Β» Ξ— ⊒˒ʷ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ” Γ—
      βˆ‡ Β» Ξ— ⊒ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ]  ░⇔

opaque

  -- An introduction lemma for _⊒˒ʷ_≑_∷_.

  β†’βŠ’Λ’Κ·β‰‘βˆ·βˆ™ :
    βˆ‡ Β» Ξ” ⊒ A β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ tail σ₁ ≑ tail Οƒβ‚‚ ∷ Ξ” β†’
    βˆ‡ Β» Ξ— ⊒ head σ₁ ≑ head Οƒβ‚‚ ∷ A [ tail σ₁ ] β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ Οƒβ‚‚ ∷ Ξ” βˆ™ A
  β†’βŠ’Λ’Κ·β‰‘βˆ·βˆ™ ⊒A Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š σ₁₀≑σ₂₀ =
    βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡”β€² ⊒A .projβ‚‚ (Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š , σ₁₀≑σ₂₀)

opaque

  -- Transitivity for _⊒˒ʷ_≑_∷_.

  trans-⊒˒ʷ :
    βˆ‡ »⊒ Ξ” β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ Οƒβ‚‚ ∷ Ξ” β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ Οƒβ‚‚ ≑ σ₃ ∷ Ξ” β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ σ₃ ∷ Ξ”
  trans-⊒˒ʷ (Ξ΅ Β»βˆ‡) σ₁≑σ₂ _ =
    βŠ’Λ’Κ·β‰‘βˆ·Ξ΅β‡” .projβ‚‚ (βŠ’Λ’Κ·β‰‘βˆ·Ξ΅β‡” .proj₁ σ₁≑σ₂)
  trans-⊒˒ʷ (βˆ™ ⊒A) σ₁≑σ₂ σ₂≑σ₃ =
    let βŠ’Ξ”                = wf ⊒A
        Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š , σ₁₀≑σ₂₀ = βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡”β€² ⊒A .proj₁ σ₁≑σ₂
        Οƒβ‚‚β‚Šβ‰‘Οƒβ‚ƒβ‚Š , σ₂₀≑σ₃₀ = βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡”β€² ⊒A .proj₁ σ₂≑σ₃
    in
    β†’βŠ’Λ’Κ·β‰‘βˆ·βˆ™ ⊒A (trans-⊒˒ʷ βŠ’Ξ” Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š Οƒβ‚‚β‚Šβ‰‘Οƒβ‚ƒβ‚Š)
      (trans σ₁₀≑σ₂₀
         (conv σ₂₀≑σ₃₀ (subst-βŠ’β‰‘ (refl ⊒A) (sym-βŠ’Λ’Κ·β‰‘βˆ· βŠ’Ξ” Οƒβ‚β‚Šβ‰‘Οƒβ‚‚β‚Š))))

opaque

  -- A lemma related to _⇑.

  βŠ’Λ’Κ·β‰‘βˆ·-⇑ :
    βˆ‡ Β» Ξ— ⊒ A [ σ₁ ] ≑ A [ Οƒβ‚‚ ] β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₁ ≑ Οƒβ‚‚ ∷ Ξ” β†’
    βˆ‡ Β» Ξ— βˆ™ A [ σ₁ ] ⊒˒ʷ σ₁ ⇑ ≑ Οƒβ‚‚ ⇑ ∷ Ξ” βˆ™ A
  βŠ’Λ’Κ·β‰‘βˆ·-⇑ A[σ₁]≑A[Οƒβ‚‚] =
    P.βŠ’Λ’Κ·β‰‘βˆ·-⇑ (wf-⊒ A[σ₁]≑A[Οƒβ‚‚] .proj₁) A[σ₁]≑A[Οƒβ‚‚]

opaque

  -- A lemma related to sgSubst.
  --
  -- See also Definition.Typed.Substitution.Primitive.⊒˒ʷ∷-sgSubst,
  -- which is re-exported from this module.

  βŠ’Λ’Κ·β‰‘βˆ·-sgSubst :
    βˆ‡ Β» Ξ” ⊒ t₁ ≑ tβ‚‚ ∷ A β†’
    βˆ‡ Β» Ξ” ⊒˒ʷ sgSubst t₁ ≑ sgSubst tβ‚‚ ∷ Ξ” βˆ™ A
  βŠ’Λ’Κ·β‰‘βˆ·-sgSubst t₁≑tβ‚‚ =
    let _ , ⊒t₁ , ⊒tβ‚‚ = wf-⊒ t₁≑tβ‚‚ in
    P.βŠ’Λ’Κ·β‰‘βˆ·-sgSubst ⊒t₁ ⊒tβ‚‚ t₁≑tβ‚‚

opaque

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

  βŠ’Λ’β‰‘βˆ·-β‚›β€’β‚› :
    βˆ‡ Β» Ξ¦ ⊒˒ʷ σ₁₁ ≑ σ₁₂ ∷ Ξ— β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ σ₂₁ ≑ Οƒβ‚‚β‚‚ ∷ Ξ” β†’
    βˆ‡ Β» Ξ¦ ⊒˒ʷ σ₁₁ β‚›β€’β‚› σ₂₁ ≑ σ₁₂ β‚›β€’β‚› Οƒβ‚‚β‚‚ ∷ Ξ”
  βŠ’Λ’β‰‘βˆ·-β‚›β€’β‚› {Ξ” = Ξ΅} σ₁₁≑σ₁₂ _ =
    βŠ’Λ’Κ·β‰‘βˆ·Ξ΅β‡” .projβ‚‚ (wf-βŠ’Λ’Κ·β‰‘βˆ· σ₁₁≑σ₁₂ .proj₁)
  βŠ’Λ’β‰‘βˆ·-β‚›β€’β‚› {Ξ” = _ βˆ™ A} σ₁₁≑σ₁₂ σ₂₁≑σ₂₂ =
    let _ , βŠ’Οƒβ‚β‚ , βŠ’Οƒβ‚β‚‚                       = wf-βŠ’Λ’Κ·β‰‘βˆ· σ₁₁≑σ₁₂
        Οƒβ‚‚β‚β‚Šβ‰‘Οƒβ‚‚β‚‚β‚Š , βŠ’Οƒβ‚‚β‚β‚€ , βŠ’Οƒβ‚‚β‚‚β‚€ , σ₂₁₀≑σ₂₂₀ = βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡” .proj₁ σ₂₁≑σ₂₂
    in
    βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡” .projβ‚‚
      ( βŠ’Λ’β‰‘βˆ·-β‚›β€’β‚› σ₁₁≑σ₁₂ Οƒβ‚‚β‚β‚Šβ‰‘Οƒβ‚‚β‚‚β‚Š
      , PE.subst (_⊒_∷_ _ _) (substCompEq A) (subst-⊒ βŠ’Οƒβ‚‚β‚β‚€ βŠ’Οƒβ‚β‚)
      , PE.subst (_⊒_∷_ _ _) (substCompEq A) (subst-⊒ βŠ’Οƒβ‚‚β‚‚β‚€ βŠ’Οƒβ‚β‚‚)
      , PE.subst (_⊒_≑_∷_ _ _ _) (substCompEq A) (subst-βŠ’β‰‘ σ₂₁₀≑σ₂₂₀ σ₁₁≑σ₁₂)
      )

opaque

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

  ⊒˒∷-β‚›β€’β‚› :
    βˆ‡ Β» Ξ¦ ⊒˒ʷ σ₁ ∷ Ξ— β†’
    βˆ‡ Β» Ξ— ⊒˒ʷ Οƒβ‚‚ ∷ Ξ” β†’
    βˆ‡ Β» Ξ¦ ⊒˒ʷ σ₁ β‚›β€’β‚› Οƒβ‚‚ ∷ Ξ”
  ⊒˒∷-β‚›β€’β‚› βŠ’Οƒβ‚ βŠ’Οƒβ‚‚ =
    βŠ’Λ’Κ·βˆ·β‡”βŠ’Λ’Κ·β‰‘βˆ· .projβ‚‚
      (βŠ’Λ’β‰‘βˆ·-β‚›β€’β‚› (βŠ’Λ’Κ·βˆ·β‡”βŠ’Λ’Κ·β‰‘βˆ· .proj₁ βŠ’Οƒβ‚) (βŠ’Λ’Κ·βˆ·β‡”βŠ’Λ’Κ·β‰‘βˆ· .proj₁ βŠ’Οƒβ‚‚))

opaque

  -- A lemma related to _[_][_]↑.

  βŠ’Λ’Κ·β‰‘βˆ·-[][]↑ :
    βˆ‡ Β» Ξ” ⊒ t₁ ≑ tβ‚‚ ∷ wk[ k ] A β†’
    βˆ‡ Β» Ξ” ⊒˒ʷ consSubst (wkSubst k idSubst) t₁ ≑
      consSubst (wkSubst k idSubst) tβ‚‚ ∷ drop k Ξ” βˆ™ A
  βŠ’Λ’Κ·β‰‘βˆ·-[][]↑ t₁≑tβ‚‚ =
    let _ , ⊒t₁ , ⊒tβ‚‚ = wf-⊒ t₁≑tβ‚‚ in
    P.βŠ’Λ’Κ·β‰‘βˆ·-[][]↑ ⊒t₁ ⊒tβ‚‚ t₁≑tβ‚‚

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

opaque

  -- A substitution lemma for several kinds of judgements.

  subst-βŠ’β‰‘β‚€ :
    Ξ“ Β»βˆ™ A ⊒[ 𝓙 ] β†’ Ξ“ ⊒ t ≑ u ∷ A β†’
    Ξ“ ⊒[ 𝓙 [ sgSubst t ≑ sgSubst u ]J ]
  subst-βŠ’β‰‘β‚€ βŠ’π“™ = subst-βŠ’β‰‘ βŠ’π“™ βˆ˜β†’ βŠ’Λ’Κ·β‰‘βˆ·-sgSubst

opaque

  -- A substitution lemma related toΒ Ξ .

  substTypeΞ  : Ξ“ ⊒ Ξ  p , q β–· A β–Ή B β†’ Ξ“ ⊒ t ∷ A β†’ Ξ“ ⊒ B [ t ]β‚€
  substTypeΠ ⊒ΠAB ⊒t =
    let _ , ⊒B , _ = inversion-ΠΣ ⊒ΠAB in
    subst-βŠ’β‚€ ⊒B ⊒t

opaque

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

  subst-⊒-↑ :
    βˆ‡ Β» drop k Ξ” βˆ™ A ⊒[ 𝓙 ] β†’ βˆ‡ Β» Ξ” ⊒ t ∷ wk[ k ] A β†’
    βˆ‡ Β» Ξ” ⊒[ 𝓙 [ replace₁ k t ]J ]
  subst-⊒-↑ βŠ’π“™ = subst-⊒ βŠ’π“™ βˆ˜β†’ ⊒˒ʷ∷-[][]↑

opaque

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

  subst-βŠ’β‰‘-↑ :
    βˆ‡ Β» drop k Ξ” βˆ™ A ⊒[ 𝓙 ] β†’ βˆ‡ Β» Ξ” ⊒ t ≑ u ∷ wk[ k ] A β†’
    βˆ‡ Β» Ξ” ⊒[ 𝓙 [ replace₁ k t ≑ replace₁ k u ]J ]
  subst-βŠ’β‰‘-↑ βŠ’π“™ = subst-βŠ’β‰‘ βŠ’π“™ βˆ˜β†’ βŠ’Λ’Κ·β‰‘βˆ·-[][]↑

opaque

  -- A substitution lemma related to _[_]↑².

  subst↑²TypeEq-prod :
    Ξ“ Β»βˆ™ Σ⟨ s ⟩ p , q β–· A β–Ή B ⊒ C ≑ D β†’
    Ξ“ Β»βˆ™ A Β»βˆ™ B ⊒
      C [ prod s p (var x1) (var x0) ]↑² ≑
      D [ prod s p (var x1) (var x0) ]↑²
  subst↑²TypeEq-prod {B} C≑D =
    let ⊒A , ⊒B , ok = inversion-Ξ Ξ£ (βŠ’βˆ™β†’βŠ’ (wf C≑D))
        ⊒Aβ€²          = wk₁ ⊒A ⊒A
    in
    subst-βŠ’β‰‘ C≑D $ βŠ’Λ’Κ·β‰‘βˆ·-[][]↑ $ _⊒_≑_∷_.refl $
    prodβ±Ό
      (wk (liftΚ· (step id) (wk₁ ⊒B ⊒Aβ€²)) (wk (liftΚ· (step id) ⊒Aβ€²) ⊒B))
      (var₁ ⊒B)
      (PE.subst (_⊒_∷_ _ _)
         (PE.trans (PE.cong wk1 $ PE.sym $ wkSingleSubstId _) $
          wk-Ξ² (U.wk _ B)) $
       varβ‚€ ⊒B)
      ok

opaque

  -- A substitution lemma related to _[_]↑².

  subst↑²Type-prod :
    Ξ“ Β»βˆ™ Σ⟨ s ⟩ p , q β–· A β–Ή B ⊒ C β†’
    Ξ“ Β»βˆ™ A Β»βˆ™ B ⊒ C [ prod s p (var x1) (var x0) ]↑²
  subst↑²Type-prod = proj₁ βˆ˜β†’ wf-⊒ βˆ˜β†’ subst↑²TypeEq-prod βˆ˜β†’ refl

opaque

  -- A substitution lemma related to _[_,_]₁₀.

  subst-βŠ’β‚β‚€ :
    Ξ“ Β»βˆ™ A Β»βˆ™ B ⊒[ 𝓙 ] β†’
    Ξ“ ⊒ t ∷ A β†’
    Ξ“ ⊒ u ∷ B [ t ]β‚€ β†’
    Ξ“ ⊒[ 𝓙 [ consSubst (sgSubst t) u ]J ]
  subst-βŠ’β‚β‚€ βŠ’π“™ ⊒t ⊒u = subst-⊒ βŠ’π“™ (β†’βŠ’Λ’Κ·βˆ·βˆ™ (⊒˒ʷ∷-sgSubst ⊒t) ⊒u)

opaque

  -- A substitution lemma related to _[_,_]₁₀.

  subst-βŠ’β‰‘β‚β‚€ :
    Ξ“ Β»βˆ™ A Β»βˆ™ B ⊒[ 𝓙 ] β†’
    Ξ“ ⊒ t₁ ≑ tβ‚‚ ∷ A β†’
    Ξ“ ⊒ u₁ ≑ uβ‚‚ ∷ B [ t₁ ]β‚€ β†’
    Ξ“ ⊒[ 𝓙 [ consSubst (sgSubst t₁) u₁ ≑ consSubst (sgSubst tβ‚‚) uβ‚‚ ]J ]
  subst-βŠ’β‰‘β‚β‚€ βŠ’π“™ t₁≑tβ‚‚ u₁≑uβ‚‚ =
    subst-βŠ’β‰‘ βŠ’π“™ $
    βŠ’Λ’Κ·β‰‘βˆ·βˆ™β‡”β€² (βŠ’βˆ™β†’βŠ’ (wf βŠ’π“™)) .projβ‚‚
      (βŠ’Λ’Κ·β‰‘βˆ·-sgSubst t₁≑tβ‚‚ , u₁≑uβ‚‚)

opaque

  -- A variant of subst-βŠ’β‰‘-↑.

  [][]↑-cong :
    βˆ‡ Β» drop k Ξ” βˆ™ A ⊒[ 𝓙 ] β†’
    βˆ‡ Β» Ξ” ⊒ t₁ ≑ tβ‚‚ ∷ A [ wkSubst k idSubst ] β†’
    βˆ‡ Β» Ξ” ⊒[ 𝓙 [ replace₁ k t₁ ≑ replace₁ k tβ‚‚ ]J ]
  [][]↑-cong {k} B₁≑Bβ‚‚ =
    subst-βŠ’β‰‘-↑ B₁≑Bβ‚‚ βˆ˜β†’
    PE.subst (_⊒_≑_∷_ _ _ _) (PE.sym $ wk[]≑[] k)

opaque

  -- A variant of subst-⊒-↑.

  ⊒[][]↑ :
    βˆ‡ Β» drop k Ξ” βˆ™ A ⊒[ 𝓙 ] β†’
    βˆ‡ Β» Ξ” ⊒ t ∷ A [ wkSubst k idSubst ] β†’
    βˆ‡ Β» Ξ” ⊒[ 𝓙 [ replace₁ k t ]J ]
  ⊒[][]↑ {k} ⊒B =
    subst-⊒-↑ ⊒B βˆ˜β†’
    PE.subst (_⊒_∷_ _ _) (PE.sym $ wk[]≑[] k)