```------------------------------------------------------------------------
-- Some simple substitution combinators
------------------------------------------------------------------------

-- Given a term type which supports weakening and transformation of
-- variables to terms various substitutions are defined and various
-- lemmas proved.

open import Universe

module deBruijn.Substitution.Function.Simple
{i u e} {Uni : Indexed-universe i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Function.Basics
open import deBruijn.Substitution.Function.Map
open import Function as F using (_\$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- Simple substitutions.

record Simple {t} (T : Term-like t) : Set (i ⊔ u ⊔ e ⊔ t) where

open Term-like T

field

-- Weakens terms.
weaken : ∀ {Γ} {σ : Type Γ} → [ T ⟶ T ] ŵk[ σ ]

-- A synonym.

weaken[_] : ∀ {Γ} (σ : Type Γ) → [ T ⟶ T ] ŵk[ σ ]
weaken[_] _ = weaken

field

-- Takes variables to terms.
var : [ Var ⟶⁼ T ]

-- A property relating weaken and var.
weaken-var : ∀ {Γ σ τ} (x : Γ ∋ τ) →
weaken[ σ ] · (var · x) ≅-⊢ var · suc[ σ ] x

-- Weakens substitutions.

wk-subst : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk[ σ ])
wk-subst ρ = map weaken ρ

wk-subst[_] : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk[ σ ])
wk-subst[ _ ] = wk-subst

-- N-ary weakening of substitutions.

wk-subst⁺ : ∀ {Γ Δ} Δ⁺ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk⁺ Δ⁺)
wk-subst⁺ ε        ρ = ρ
wk-subst⁺ (Δ⁺ ▻ σ) ρ = wk-subst (wk-subst⁺ Δ⁺ ρ)

wk-subst₊ : ∀ {Γ Δ} Δ₊ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk₊ Δ₊)
wk-subst₊ ε        ρ = ρ
wk-subst₊ (σ ◅ Δ₊) ρ = wk-subst₊ Δ₊ (wk-subst ρ)

-- Lifting.

infixl 10 _↑_
infix  10 _↑

_↑_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ σ → Sub T (ρ̂ ↑̂ σ)
ρ ↑ _ =
P.subst (Sub T)
(≅-⇨̂-⇒-≡ \$ ▻̂-cong P.refl P.refl
(P.sym \$ corresponds var zero))
(wk-subst ρ ▻⇨ var · zero)

_↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ↑̂ σ)
ρ ↑ = ρ ↑ _

-- N-ary lifting.

infixl 10 _↑⁺_ _↑₊_

_↑⁺_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ Γ⁺ → Sub T (ρ̂ ↑̂⁺ Γ⁺)
ρ ↑⁺ ε        = ρ
ρ ↑⁺ (Γ⁺ ▻ σ) = (ρ ↑⁺ Γ⁺) ↑

_↑₊_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ Γ₊ → Sub T (ρ̂ ↑̂₊ Γ₊)
ρ ↑₊ ε        = ρ
ρ ↑₊ (σ ◅ Γ₊) = ρ ↑ ↑₊ Γ₊

-- The identity substitution.

id[_] : ∀ Γ → Sub T îd[ Γ ]
id[ ε     ] = ε⇨
id[ Γ ▻ σ ] = id[ Γ ] ↑

id : ∀ {Γ} → Sub T îd[ Γ ]
id = id[ _ ]

-- N-ary weakening.

wk⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Sub T (ŵk⁺ Γ⁺)
wk⁺ ε        = id
wk⁺ (Γ⁺ ▻ σ) = wk-subst (wk⁺ Γ⁺)

wk₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Sub T (ŵk₊ Γ₊)
wk₊ Γ₊ = wk-subst₊ Γ₊ id

-- Weakening.

wk[_] : ∀ {Γ} (σ : Type Γ) → Sub T ŵk[ σ ]
wk[ σ ] = wk⁺ (ε ▻ σ)

wk : ∀ {Γ} {σ : Type Γ} → Sub T ŵk[ σ ]
wk = wk[ _ ]

private

-- Three possible definitions of wk coincide definitionally.

coincide₁ : ∀ {Γ} {σ : Type Γ} → wk⁺ (ε ▻ σ) ≡ wk₊ (σ ◅ ε)
coincide₁ = P.refl

coincide₂ : ∀ {Γ} {σ : Type Γ} → wk⁺ (ε ▻ σ) ≡ wk-subst id
coincide₂ = P.refl

-- A substitution which only replaces the first variable.

sub : ∀ {Γ σ} (t : Γ ⊢ σ) → Sub T (ŝub ⟦ t ⟧)
sub t = id ▻⇨ t

abstract

-- Unfolding lemma for _↑.

unfold-↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) →
ρ ↑ σ ≅-⇨ wk-subst[ σ / ρ ] ρ ▻⇨[ σ ] var · zero
unfold-↑ _ =
drop-subst-Sub F.id
(≅-⇨̂-⇒-≡ \$ ▻̂-cong P.refl P.refl (P.sym \$ corresponds var zero))

-- Some congruence lemmas.

weaken-cong : ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ⊢ τ₁}
{Γ₂ σ₂ τ₂} {t₂ : Γ₂ ⊢ τ₂} →
σ₁ ≅-Type σ₂ → t₁ ≅-⊢ t₂ →
weaken[ σ₁ ] · t₁ ≅-⊢ weaken[ σ₂ ] · t₂
weaken-cong P.refl P.refl = P.refl

var-cong : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
{Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
x₁ ≅-∋ x₂ → var · x₁ ≅-⊢ var · x₂
var-cong P.refl = P.refl

wk-subst-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
σ₁ ≅-Type σ₂ → ρ₁ ≅-⇨ ρ₂ →
wk-subst[ σ₁ ] ρ₁ ≅-⇨ wk-subst[ σ₂ ] ρ₂
wk-subst-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
[ P.refl ]

abstract

wk-subst⁺-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ≅-⇨ ρ₂ →
wk-subst⁺ Γ⁺₁ ρ₁ ≅-⇨ wk-subst⁺ Γ⁺₂ ρ₂
wk-subst⁺-cong {Γ⁺₁ = ε} {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
[ P.refl ]
wk-subst⁺-cong {Γ⁺₁ = Γ⁺₁ ▻ σ} P.refl ρ₁≅ρ₂ =
wk-subst-cong (P.refl {x = [ σ ]})
(wk-subst⁺-cong (P.refl {x = [ Γ⁺₁ ]}) ρ₁≅ρ₂)

wk-subst₊-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ≅-⇨ ρ₂ →
wk-subst₊ Γ₊₁ ρ₁ ≅-⇨ wk-subst₊ Γ₊₂ ρ₂
wk-subst₊-cong {Γ₊₁ = ε} {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
[ P.refl ]
wk-subst₊-cong {Γ₊₁ = σ ◅ Γ₊₁} P.refl ρ₁≅ρ₂ =
wk-subst₊-cong (P.refl {x = [ Γ₊₁ ]}) (wk-subst-cong P.refl ρ₁≅ρ₂)

↑-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {σ₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {σ₂} →
ρ₁ ≅-⇨ ρ₂ → σ₁ ≅-Type σ₂ → ρ₁ ↑ σ₁ ≅-⇨ ρ₂ ↑ σ₂
↑-cong {ρ₁ = ρ₁} {σ₁} {ρ₂ = ρ₂} {σ₂} ρ₁≅ρ₂ σ₁≅σ₂ =
let lemma = /-cong σ₁≅σ₂ ρ₁≅ρ₂ in
ρ₁ ↑ σ₁                               ≅-⟶⟨ unfold-↑ ρ₁ ⟩
wk-subst ρ₁ ▻⇨ var · zero[ σ₁ / ρ₁ ]  ≅-⟶⟨ ▻⇨-cong σ₁≅σ₂ (wk-subst-cong lemma ρ₁≅ρ₂) (var-cong (zero-cong lemma)) ⟩
wk-subst ρ₂ ▻⇨ var · zero[ σ₂ / ρ₂ ]  ≅-⟶⟨ sym-⟶ \$ unfold-↑ ρ₂ ⟩
ρ₂ ↑ σ₂                               ∎-⟶

↑⁺-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ⁺₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ⁺₂} →
ρ₁ ≅-⇨ ρ₂ → Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ↑⁺ Γ⁺₁ ≅-⇨ ρ₂ ↑⁺ Γ⁺₂
↑⁺-cong {ρ₁ = _ , _} {Γ⁺₁ = ε} {ρ₂ = ._ , _} [ P.refl ] P.refl =
[ P.refl ]
↑⁺-cong {Γ⁺₁ = Γ⁺ ▻ σ} ρ₁≅ρ₂ P.refl =
↑-cong (↑⁺-cong ρ₁≅ρ₂ (P.refl {x = [ Γ⁺ ]})) P.refl

↑₊-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ₊₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ₊₂} →
ρ₁ ≅-⇨ ρ₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ↑₊ Γ₊₁ ≅-⇨ ρ₂ ↑₊ Γ₊₂
↑₊-cong {ρ₁ = _ , _} {Γ₊₁ = ε} {ρ₂ = ._ , _} [ P.refl ] P.refl =
[ P.refl ]
↑₊-cong {Γ₊₁ = σ ◅ Γ₊} ρ₁≅ρ₂ P.refl =
↑₊-cong (↑-cong ρ₁≅ρ₂ P.refl) (P.refl {x = [ Γ₊ ]})

id-cong : ∀ {Γ₁ Γ₂} → Γ₁ ≅-Ctxt Γ₂ → id[ Γ₁ ] ≅-⇨ id[ Γ₂ ]
id-cong P.refl = [ P.refl ]

wk⁺-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁} {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → wk⁺ Γ⁺₁ ≅-⇨ wk⁺ Γ⁺₂
wk⁺-cong P.refl = [ P.refl ]

wk₊-cong : ∀ {Γ₁} {Γ₊₁ : Ctxt₊ Γ₁} {Γ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
Γ₊₁ ≅-Ctxt₊ Γ₊₂ → wk₊ Γ₊₁ ≅-⇨ wk₊ Γ₊₂
wk₊-cong P.refl = [ P.refl ]

wk-cong : ∀ {Γ₁} {σ₁ : Type Γ₁} {Γ₂} {σ₂ : Type Γ₂} →
σ₁ ≅-Type σ₂ → wk[ σ₁ ] ≅-⇨ wk[ σ₂ ]
wk-cong P.refl = [ P.refl ]

sub-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
t₁ ≅-⊢ t₂ → sub t₁ ≅-⇨ sub t₂
sub-cong P.refl = [ P.refl ]

abstract

-- Some lemmas relating variables to lifting.

/∋-↑ : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ▻ σ ∋ τ) (ρ : Sub T ρ̂) →
x /∋ ρ ↑ ≅-⊢ x /∋ (wk-subst[ σ / ρ ] ρ ▻⇨ var · zero)
/∋-↑ x ρ = /∋-cong (P.refl {x = [ x ]}) (unfold-↑ ρ)

zero-/∋-↑ : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) →
zero[ σ ] /∋ ρ ↑ ≅-⊢ var · zero[ σ / ρ ]
zero-/∋-↑ σ ρ = begin
[ zero[ σ ] /∋ ρ ↑                        ]  ≡⟨ /∋-↑ zero[ σ ] ρ ⟩
[ zero[ σ ] /∋ (wk-subst ρ ▻⇨ var · zero) ]  ≡⟨ P.refl ⟩
[ var · zero                              ]  ∎

suc-/∋-↑ : ∀ {Γ Δ τ} σ {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ τ) (ρ : Sub T ρ̂) →
suc[ σ ] x /∋ ρ ↑ ≅-⊢ x /∋ wk-subst[ σ / ρ ] ρ
suc-/∋-↑ σ x ρ = begin
[ suc[ σ ] x /∋ ρ ↑                        ]  ≡⟨ /∋-↑ (suc[ σ ] x) ρ ⟩
[ suc[ σ ] x /∋ (wk-subst ρ ▻⇨ var · zero) ]  ≡⟨ P.refl ⟩
[ x /∋ wk-subst ρ                          ]  ∎

-- One can weaken either before or after looking up a variable.
-- (Note that this lemma holds definitionally, unlike the
-- corresponding lemma in deBruijn.Substitution.Data.Simple.)

/∋-wk-subst : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ τ) (ρ : Sub T ρ̂) →
x /∋ wk-subst[ σ ] ρ ≅-⊢ weaken[ σ ] · (x /∋ ρ)
/∋-wk-subst x ρ = P.refl

abstract

-- A corollary.

/∋-wk-subst-var :
∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ}
(ρ : Sub T ρ̂) (x : Γ ∋ τ) (y : Δ ∋ τ / ρ) →
x /∋               ρ ≅-⊢ var ·          y →
x /∋ wk-subst[ σ ] ρ ≅-⊢ var · suc[ σ ] y
/∋-wk-subst-var ρ x y hyp = begin
[ x /∋ wk-subst ρ    ]  ≡⟨ P.refl ⟩
[ weaken · (x /∋ ρ)  ]  ≡⟨ weaken-cong P.refl hyp ⟩
[ weaken · (var · y) ]  ≡⟨ weaken-var y ⟩
[ var · suc y        ]  ∎

-- The identity substitution has no effect.

/-id : ∀ {Γ} (σ : Type Γ) → σ / id ≅-Type σ
/-id σ = P.refl

/⁺-id : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ⁺ /⁺ id ≅-Ctxt⁺ Γ⁺
/⁺-id Γ⁺ = begin
[ Γ⁺ /⁺ id ]  ≡⟨ P.refl ⟩
[ Γ⁺ /̂⁺ îd ]  ≡⟨ /̂⁺-îd Γ⁺ ⟩
[ Γ⁺       ]  ∎

/₊-id : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ₊ /₊ id ≅-Ctxt₊ Γ₊
/₊-id Γ₊ = begin
[ Γ₊ /₊ id ]  ≡⟨ P.refl ⟩
[ Γ₊ /̂₊ îd ]  ≡⟨ /̂₊-îd Γ₊ ⟩
[ Γ₊       ]  ∎

mutual

/∋-id : ∀ {Γ σ} (x : Γ ∋ σ) → x /∋ id ≅-⊢ var · x
/∋-id {Γ = ε}     ()
/∋-id {Γ = Γ ▻ σ} x = begin
[ x /∋ id ↑               ]  ≡⟨ /∋-↑ x id ⟩
[ x /∋ (wk ▻⇨ var · zero) ]  ≡⟨ lemma x ⟩
[ var · x                 ]  ∎
where
lemma : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
x /∋ (wk[ σ ] ▻⇨ var · zero) ≅-⊢ var · x
lemma zero    = P.refl
lemma (suc x) = /∋-wk x

-- Weakening a variable is equivalent to incrementing it.

/∋-wk : ∀ {Γ σ τ} (x : Γ ∋ τ) →
x /∋ wk[ σ ] ≅-⊢ var · suc[ σ ] x
/∋-wk x = /∋-wk-subst-var id x x (/∋-id x)

-- The n-ary lifting of the identity substitution is the identity
-- substitution.

id-↑⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → id ↑⁺ Γ⁺ ≅-⇨ id[ Γ ++⁺ Γ⁺ ]
id-↑⁺ ε        = id ∎-⟶
id-↑⁺ (Γ⁺ ▻ σ) =
(id ↑⁺ Γ⁺) ↑  ≅-⟶⟨ ↑-cong (id-↑⁺ Γ⁺) P.refl ⟩
id ↑          ∎-⟶

id-↑₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → id ↑₊ Γ₊ ≅-⇨ id[ Γ ++₊ Γ₊ ]
id-↑₊ ε        = id ∎-⟶
id-↑₊ (σ ◅ Γ₊) =
id ↑ ↑₊ Γ₊  ≅-⟶⟨ [ P.refl ] ⟩
id   ↑₊ Γ₊  ≅-⟶⟨ id-↑₊ Γ₊ ⟩
id          ∎-⟶

-- The identity substitution has no effect even if lifted.

/∋-id-↑⁺ : ∀ {Γ} Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
x /∋ id ↑⁺ Γ⁺ ≅-⊢ var · x
/∋-id-↑⁺ Γ⁺ x = begin
[ x /∋ id ↑⁺ Γ⁺ ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (id-↑⁺ Γ⁺) ⟩
[ x /∋ id       ]  ≡⟨ /∋-id x ⟩
[ var · x       ]  ∎

/∋-id-↑₊ : ∀ {Γ} Γ₊ {σ} (x : Γ ++₊ Γ₊ ∋ σ) →
x /∋ id ↑₊ Γ₊ ≅-⊢ var · x
/∋-id-↑₊ Γ₊ x = begin
[ x /∋ id ↑₊ Γ₊ ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (id-↑₊ Γ₊) ⟩
[ x /∋ id       ]  ≡⟨ /∋-id x ⟩
[ var · x       ]  ∎

-- If ρ is morally a renaming, then "deep application" of ρ to a
-- variable is still a variable.

/∋-↑⁺ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
(ρ : Sub T ρ̂) (f : [ Var ⟶ Var ] ρ̂) →
(∀ {σ} (x : Γ ∋ σ) → x /∋ ρ ≅-⊢ var · (f · x)) →
∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
x /∋ ρ ↑⁺ Γ⁺ ≅-⊢ var · (lift f Γ⁺ · x)
/∋-↑⁺ ρ f hyp ε        x    = hyp x
/∋-↑⁺ ρ f hyp (Γ⁺ ▻ σ) zero = begin
[ zero[ σ ] /∋ (ρ ↑⁺ Γ⁺) ↑ ]  ≡⟨ zero-/∋-↑ σ (ρ ↑⁺ Γ⁺) ⟩
[ var · zero               ]  ∎
/∋-↑⁺ ρ f hyp (Γ⁺ ▻ σ) (suc x) = begin
[ suc[ σ ] x /∋ (ρ ↑⁺ Γ⁺) ↑        ]  ≡⟨ suc-/∋-↑ σ x (ρ ↑⁺ Γ⁺) ⟩
[ x /∋ wk-subst (ρ ↑⁺ Γ⁺)          ]  ≡⟨ P.refl ⟩
[ weaken · (x /∋ ρ ↑⁺ Γ⁺)          ]  ≡⟨ weaken-cong P.refl (/∋-↑⁺ ρ f hyp Γ⁺ x) ⟩
[ weaken · (var · (lift f Γ⁺ · x)) ]  ≡⟨ weaken-var (lift f Γ⁺ · x) ⟩
[ var · suc (lift f Γ⁺ · x)        ]  ∎

-- "Deep weakening" of a variable can be expressed without
-- reference to the weaken function.

/∋-wk-↑⁺ : ∀ {Γ σ} Γ⁺ {τ} (x : Γ ++⁺ Γ⁺ ∋ τ) →
x /∋ wk[ σ ] ↑⁺ Γ⁺ ≅-⊢
var · (lift weaken∋[ σ ] Γ⁺ · x)
/∋-wk-↑⁺ = /∋-↑⁺ wk weaken∋ /∋-wk

/∋-wk-↑⁺-↑⁺ : ∀ {Γ σ} Γ⁺ Γ⁺⁺ {τ} (x : Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ∋ τ) →
x /∋ wk[ σ ] ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺ ≅-⊢
var · (lift (lift weaken∋[ σ ] Γ⁺) Γ⁺⁺ · x)
/∋-wk-↑⁺-↑⁺ Γ⁺ = /∋-↑⁺ (wk ↑⁺ Γ⁺) (lift weaken∋ Γ⁺) (/∋-wk-↑⁺ Γ⁺)

-- Two n-ary liftings can be merged into one.

↑⁺-⁺++⁺ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) Γ⁺ Γ⁺⁺ →
ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) ≅-⇨ ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺
↑⁺-⁺++⁺ ρ Γ⁺ ε         = ρ ↑⁺ Γ⁺ ∎-⟶
↑⁺-⁺++⁺ ρ Γ⁺ (Γ⁺⁺ ▻ σ) =
(ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺)) ↑  ≅-⟶⟨ ↑-cong (↑⁺-⁺++⁺ ρ Γ⁺ Γ⁺⁺)
(drop-subst-Type F.id (++⁺-++⁺ Γ⁺ Γ⁺⁺)) ⟩
(ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺) ↑      ∎-⟶

↑₊-₊++₊ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) Γ₊ Γ₊₊ →
ρ ↑₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨ ρ ↑₊ Γ₊ ↑₊ Γ₊₊
↑₊-₊++₊ ρ ε        Γ₊₊ = ρ ↑₊ Γ₊₊ ∎-⟶
↑₊-₊++₊ ρ (σ ◅ Γ₊) Γ₊₊ =
ρ ↑ ↑₊ (Γ₊ ₊++₊ Γ₊₊)  ≅-⟶⟨ ↑₊-₊++₊ (ρ ↑) Γ₊ Γ₊₊ ⟩
ρ ↑ ↑₊ Γ₊ ↑₊ Γ₊₊      ∎-⟶
```