{-|
This module proves the substitution properties.
-}

{-# OPTIONS --safe #-}
module CtxTyp.Substitution.Properties where

open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Data.Nat.Properties as ℕ
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)

open import CtxTyp.Context
open import CtxTyp.Term
open import CtxTyp.Term.Properties
open import CtxTyp.Depth
open import CtxTyp.Substitution

private module _ where
  cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {x x′ y y′ z z′} → x ≡ x′ → y ≡ y′ → z ≡ z′ → f x y z ≡ f x′ y′ z′
  cong₃ f refl refl refl = refl

private variable
  d d′ d″ : ℕ
  σ σ′ σ″ σ₁ σ₂ : Γ′ ⊩ Γ

-- | The depth argument `d` in substᵈ, substSubstᵈ, useItemᵈ, substSubstItemᵈ does not affect the result of substitution.
useItemᵈ-constant : ∀ (item : Γ ⊩[ Δ ⊢ A ^ ≤‴-refl ]) {itemᵈ : item ≤ᵈ″ d} {itemᵈ′ : item ≤ᵈ″ d′} (σ : Γ ⊩ Δ) → useItemᵈ itemᵈ σ ≡ useItemᵈ itemᵈ′ σ
substᵈ-constant : ∀ (σ : Γ′ ⊩ Γ) {σᵈ : σ ≤ᵈ′ d} {σᵈ′ : σ ≤ᵈ′ d′} (e : Term n Γ A) → substᵈ σᵈ e ≡ substᵈ σᵈ′ e
substSubstᵈ-constant : ∀ (σ : Γ′ ⊩ Γ) {σᵈ : σ ≤ᵈ′ d} {σᵈ′ : σ ≤ᵈ′ d′} (σ₁ : Γ ⊩ Δ) → substSubstᵈ σᵈ σ₁ ≡ substSubstᵈ σᵈ′ σ₁
substSubstItemᵈ-constant : ∀ (σ : Γ′ ⊩ Γ) {σᵈ : σ ≤ᵈ′ d} {σᵈ′ : σ ≤ᵈ′ d′} (item : Γ ⊩[ Δ ⊢ A ^ m≥n ]) → substSubstItemᵈ σᵈ item ≡ substSubstItemᵈ σᵈ′ item

useItemᵈ-constant (var x) σ = refl
useItemᵈ-constant {d = suc _} {d′ = suc _} (term e) σ = substᵈ-constant (lift id ++ˢ σ) e

substᵈ-constant σ {σᵈ = σᵈ} {σᵈ′ = σᵈ′} (` x `with σ₁) = trans (useItemᵈ-constant (lookup σ x) (substSubstᵈ σᵈ σ₁)) (cong (useItemᵈ (lookupᵈ σᵈ′ x)) (substSubstᵈ-constant σ σ₁))
substᵈ-constant σ `true = refl
substᵈ-constant σ `false = refl
substᵈ-constant σ (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (substᵈ-constant σ e₁) (substᵈ-constant σ e₂) (substᵈ-constant σ e₃)
substᵈ-constant σ (`λ⟨ Δ ⟩ e) = cong (`λ⟨ Δ ⟩_) (substᵈ-constant (exts σ) e)
substᵈ-constant σ (e₁ · e₂) = cong₂ _·_ (substᵈ-constant σ e₁) (substᵈ-constant (exts++ _ σ) e₂)
substᵈ-constant σ ⟨ e ⟩ = cong ⟨_⟩ (substᵈ-constant (exts↾ σ) e)
substᵈ-constant σ (`let⟨ Δ ⟩ e₁ e₂) = cong₂ (`let⟨ Δ ⟩) (substᵈ-constant (exts++ _ σ) e₁) (substᵈ-constant (exts σ) e₂)
substᵈ-constant σ (`wrap Δ e) = cong (`wrap Δ) (substᵈ-constant (exts++ _ σ) e)
substᵈ-constant σ (`letwrap Δ e e₁) = cong₂ (`letwrap Δ) (substᵈ-constant σ e) (substᵈ-constant (exts σ) e₁)

substSubstᵈ-constant σ ∅ = refl
substSubstᵈ-constant σ (σ₁ , item) = cong₂ _,_ (substSubstᵈ-constant σ σ₁) (substSubstItemᵈ-constant σ item)
substSubstᵈ-constant σ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (substSubstᵈ-constant σ σ₁) (substSubstᵈ-constant σ σ₂)

substSubstItemᵈ-constant σ (term e) = cong term (substᵈ-constant _ e)
substSubstItemᵈ-constant σ (var x) = refl

-- Some helpers for the casting with equalities.
≤ᵈ′-castˡ :  ∀ {d} {σ σ′ : Γ′ ⊩ Γ} → σ ≡ σ′ → σ ≤ᵈ′ d → σ′ ≤ᵈ′ d
≤ᵈ′-castˡ refl σᵈ = σᵈ

≤ᵈ″-castˡ :  ∀ {d} {item item′ : Γ ⊩[ Δ ⊢ A ^ ≤‴-refl ]} → item ≡ item′ → item ≤ᵈ″ d → item′ ≤ᵈ″ d
≤ᵈ″-castˡ refl itemᵈ = itemᵈ

substᵈ-cong : ∀ {σ σ′ : Γ′ ⊩ Γ}
  → (eq : σ ≡ σ′) → ∀ {d} {σᵈ : σ ≤ᵈ′ d} → (e : Γ ⊢ A ^ n) → substᵈ {d = d} σᵈ e ≡ substᵈ {d = d} (≤ᵈ′-castˡ eq σᵈ) e
substᵈ-cong refl _ = refl

useItemᵈ-cong₂ : ∀ {item item′ : Γ ⊩[ Δ ⊢ A ^ ≤‴-refl ]} {σ σ′ : Γ ⊩ Δ} {d} {itemᵈ : item ≤ᵈ″ d}
  → (eq : item ≡ item′) → σ ≡ σ′ → useItemᵈ itemᵈ σ ≡ useItemᵈ (≤ᵈ″-castˡ eq itemᵈ) σ′
useItemᵈ-cong₂ refl refl = refl

substSubstᵈ-cong : ∀ {σ σ′ : Γ′ ⊩ Γ}
  → (eq : σ ≡ σ′) → ∀ {d} {σᵈ : σ ≤ᵈ′ d} → (σ₁ : Γ ⊩ Δ) → substSubstᵈ {d = d} σᵈ σ₁ ≡ substSubstᵈ {d = d} (≤ᵈ′-castˡ eq σᵈ) σ₁
substSubstᵈ-cong refl _ = refl

-- | Substituting by a lifted renaming function is equivalent to just renaming the term.
subst-lift : ∀ {Γ Γ′} (ρ : Rename Γ Γ′) (e : Term n Γ A) → subst (lift ρ) e ≡ rename ρ e
substSubst-lift : ∀ {Γ Γ′} (ρ : Rename Γ Γ′) (σ : Γ ⊩ Δ) → substSubst (lift ρ) σ ≡ renameSubst ρ σ
subst-lift ρ (` x `with σ) = useItemᵈ-cong₂ (lookup-lift ρ x) (substSubst-lift ρ σ)
subst-lift ρ `true = refl
subst-lift ρ `false = refl
subst-lift ρ (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (subst-lift ρ e₁) (subst-lift ρ e₂) (subst-lift ρ e₃)
subst-lift ρ (`λ⟨ Δ ⟩ e) = cong (`λ⟨ Δ ⟩_) (trans (trans (substᵈ-constant _ e) (cong (λ σ → subst σ e) (exts-lift ρ))) (subst-lift (ext ρ) e))
subst-lift ρ (e₁ · e₂) = cong₂ _·_ (subst-lift ρ e₁) (trans (trans (substᵈ-constant _ e₂) (cong (λ σ → subst σ e₂) (exts++-lift _ ρ))) (subst-lift (ext++ _ ρ) e₂))
subst-lift ρ ⟨ e ⟩ = cong ⟨_⟩ (trans (trans (substᵈ-constant _ e) ((cong (λ σ → subst σ e) (exts↾-lift ρ)))) (subst-lift (ext↾ ρ) e))
subst-lift ρ (`let⟨ Δ ⟩ e₁ e₂) =
  cong₂ (`let⟨ Δ ⟩)
    (trans (trans (substᵈ-constant _ e₁) (cong (λ σ → subst σ e₁) (exts++-lift _ ρ))) (subst-lift (ext++ _ ρ) e₁))
    (trans (trans (substᵈ-constant _ e₂) (cong (λ σ → subst σ e₂) (exts-lift ρ))) (subst-lift (ext ρ) e₂))
subst-lift ρ (`wrap Δ e) = cong (`wrap Δ) (trans (trans (substᵈ-constant _ e) (cong (λ σ → subst σ e) (exts++-lift _ ρ))) (subst-lift (ext++ _ ρ) e))
subst-lift ρ (`letwrap Δ e₁ e₂) =
  cong₂ (`letwrap Δ) (subst-lift ρ e₁)
    (trans (trans (substᵈ-constant _ e₂) (cong (λ σ → subst σ e₂) (exts-lift ρ))) (subst-lift (ext ρ) e₂))

substSubst-lift ρ ∅ = refl
substSubst-lift ρ (_,_ {m≥n = m≥n} σ (term e)) = cong₂ _,_ (substSubst-lift ρ σ) (cong term (trans (trans (substᵈ-constant _ e) (cong (λ σ → subst σ e) (trans (cong (exts++ _) (exts↾≥-lift m≥n ρ)) (exts++-lift _ (ext↾≥ m≥n ρ))))) (subst-lift (ext++ _ (ext↾≥ m≥n ρ)) e)))
substSubst-lift ρ (σ , var x) = cong₂ _,_ (substSubst-lift ρ σ) (lookup-lift ρ x)
substSubst-lift ρ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (substSubst-lift ρ σ₁) (substSubst-lift ρ σ₂)

-- | The identity property for substitution on terms.
subst-lift-id : (e : Γ ⊢ A ^ n) → subst (lift id) e ≡ e
subst-lift-id e = trans (subst-lift id e) (rename-id e)

-- | The (left) identity property for substitution on substitutions.
substSubst-lift-id : (σ : Γ ⊩ Δ) → substSubst (lift id) σ ≡ σ
substSubst-lift-id σ = trans (substSubst-lift id σ) (renameSubst-id σ)

-- | The (left) identity property for substitution on substitutions with depth.
substSubstᵈ-liftᵈ-id : (σ : Γ ⊩ Δ) → substSubstᵈ {d = d} (liftᵈ id) σ ≡ σ
substSubstᵈ-liftᵈ-id σ = trans (substSubstᵈ-constant (lift id) σ) (substSubst-lift-id σ)

-- | lookup distributes over substSubstᵈ.
lookup-substSubstᵈ : ∀ {d} (σ′ᵈ : σ′ ≤ᵈ′ d) (σ : Γ′ ⊩ Γ) → lookup (substSubstᵈ σ′ᵈ σ) ≗ substSubstItemᵈ σ′ᵈ ∘ lookup σ
lookup-substSubstᵈ σ′ᵈ (_ , item) Z = refl
lookup-substSubstᵈ σ′ᵈ (σ , _) (S x) = lookup-substSubstᵈ σ′ᵈ σ x
lookup-substSubstᵈ σ′ᵈ (σ ++ˢ _) (L x) = lookup-substSubstᵈ σ′ᵈ σ x
lookup-substSubstᵈ σ′ᵈ (_ ++ˢ σ) (R x) = lookup-substSubstᵈ σ′ᵈ σ x

-- | The (right) identity property for substitution on substitutions with depth.
substSubstᵈ-lift-idʳ : {σ : Γ ⊩ Δ} (σᵈ : σ ≤ᵈ′ d)  → substSubstᵈ σᵈ (lift id) ≡ σ
substSubstᵈ-lift-idʳ _ = lookup-injective-≗ λ x → trans (lookup-substSubstᵈ _ (lift id) x) (cong (substSubstItemᵈ _) (lookup-lift id x))

-- | The (right) identity property for substitution on substitutions.
substSubst-lift-idʳ : (σ : Γ ⊩ Δ) → substSubst σ (lift id) ≡ σ
substSubst-lift-idʳ σ = substSubstᵈ-lift-idʳ (≤ᵈ′-refl σ)

-- Before we can prove properties about composing two substitutions, i.e. substSubst,
-- we need to prove the special case where the second substitution is a renaming function.
-- i.e. substSubst σ (lift ρ). We represent the result σ′ of this composition as
-- lookup σ ∘ ρ ≗ lookup σ′ to avoid circular reasoning.
-- In the following, we abuse notation and write σ ∘ ρ for substSubst σ (lift ρ).

-- | This basically says (lift ρ ++ˢ σ) ≡ (lift id ++ˢ σ) ∘ (ext++ Δ ρ)
lookup-lift-++ˢ : (ρ : Rename Γ Γ′) (σ : Γ′ ⊩ Δ) → lookup (lift ρ ++ˢ σ) ≗ lookup (lift id ++ˢ σ) ∘ (ext++ Δ ρ)
lookup-lift-++ˢ ρ σ (L x) = trans (lookup-lift ρ x) (sym (lookup-lift id (ρ x)))
lookup-lift-++ˢ ρ σ (R x) = refl

-- | exts σ ∘ ext ρ ≡ exts (σ ∘ ρ)
exts-ext : ∀ {σ : Γ″ ⊩ Γ′} {ρ : Rename Γ Γ′} {σ′ : Γ″ ⊩ Γ}
  → lookup σ ∘ ρ ≗ lookup σ′
  → lookup (exts {Δ = Δ} {A = A} {m≥n = m≥n} σ) ∘ ext ρ ≗ lookup (exts σ′)
exts-ext σ∘ρ≗σ′ Z = refl
exts-ext {σ = σ} {ρ = ρ} {σ′ = σ′} σ∘ρ≗σ′ (S x) =
  trans (lookup-renameSubst S σ (ρ x))
    (trans (cong (renameSubstItem S) (σ∘ρ≗σ′ x))
      (sym (lookup-renameSubst S σ′ x)))

-- | exts++ σ ∘ ext++ ρ ≡ exts++ (σ ∘ ρ) 
exts++-ext++ : ∀ {σ : Γ″ ⊩ Γ′} {ρ : Rename Γ Γ′} {σ′ : Γ″ ⊩ Γ}
  → lookup σ ∘ ρ ≗ lookup σ′
  → lookup (exts++ Δ σ) ∘ ext++ Δ ρ ≗ lookup (exts++ Δ σ′)
exts++-ext++ {σ = σ} {ρ = ρ} {σ′ = σ′} σ∘ρ≗σ′ (L x) =
  trans (lookup-renameSubst L σ (ρ x))
    (trans (cong (renameSubstItem L) (σ∘ρ≗σ′ x))
      (sym (lookup-renameSubst L σ′ x)))
exts++-ext++ σ∘ρ≗σ′ (R x) = refl

-- | exts↾ σ ∘ ext↾ ρ ≡ exts↾ (σ ∘ ρ)
exts↾-ext↾ : ∀ {σ : Γ″ ⊩ Γ′} {ρ : Rename Γ Γ′} {σ′ : Γ″ ⊩ Γ}
  → lookup σ ∘ ρ ≗ lookup σ′
  → lookup (exts↾ σ) ∘ ext↾ ρ ≗ lookup (exts↾ σ′)
exts↾-ext↾ {σ = σ} {ρ = ρ} {σ′ = σ′} σ∘ρ≗σ′ x =
  trans (lookup-exts↾ σ (ext↾ ρ x))
    (trans (cong (⊩[]-↾⁺ ∘ lookup σ) (∋-↾⁻-∋-↾⁺ (ρ (∋-↾⁻ x))))
      (trans (cong ⊩[]-↾⁺ (σ∘ρ≗σ′ (∋-↾⁻ x)))
        (sym (lookup-exts↾ σ′ x))))

-- | exts↾≥ m≥n σ ∘ ext↾≥ m≥n ρ ≡ exts↾≥ m≥n (σ ∘ ρ)
exts↾≥-ext↾≥ : ∀ (m≥n : m ≥‴ n) {σ : Γ″ ⊩ Γ′} {ρ : Rename Γ Γ′} {σ′ : Γ″ ⊩ Γ}
  → lookup σ ∘ ρ ≗ lookup σ′
  → lookup (exts↾≥ m≥n σ) ∘ ext↾≥ m≥n ρ ≗ lookup (exts↾≥ m≥n σ′)
exts↾≥-ext↾≥ ≤‴-refl σ∘ρ≗σ′ = σ∘ρ≗σ′
exts↾≥-ext↾≥ (≤‴-step m≥n) {σ = σ} {ρ = ρ} {σ′ = σ′} σ∘ρ≗σ′ = exts↾≥-ext↾≥ m≥n (exts↾-ext↾ {σ = σ} {ρ = ρ} {σ′ = σ′} σ∘ρ≗σ′)

-- | Special cases of the associativity properties where the second substitution is a renaming function.
substᵈ-rename-compose :  ∀ {d} {σ : Γ″ ⊩ Γ′} {σᵈ : σ ≤ᵈ′ d} {ρ : Rename Γ Γ′} {σ′ : Γ″ ⊩ Γ} {σ′ᵈ : σ′ ≤ᵈ′ d}
  → lookup σ ∘ ρ ≗ lookup σ′
  → ∀ (e : Γ ⊢ A ^ n) → substᵈ σᵈ (rename ρ e) ≡ substᵈ σ′ᵈ e
substSubstᵈ-renameSubst-compose :  ∀ {d} {σ : Γ″ ⊩ Γ′} {σᵈ : σ ≤ᵈ′ d} {ρ : Rename Γ Γ′} {σ′ : Γ″ ⊩ Γ} {σ′ᵈ : σ′ ≤ᵈ′ d}
  → lookup σ ∘ ρ ≗ lookup σ′
  → ∀ (σ₁ : Γ ⊩ Δ) → substSubstᵈ σᵈ (renameSubst ρ σ₁) ≡ substSubstᵈ σ′ᵈ σ₁
substᵈ-rename-compose {σ = σ} {σᵈ = σᵈ} {ρ = ρ} {σ′ = σ′} {σ′ᵈ = σ′ᵈ} σ∘ρ≗σ′ (` x `with σ₁) = useItemᵈ-cong₂ (σ∘ρ≗σ′ x) (substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ σ₁)
substᵈ-rename-compose σ∘ρ≗σ′ `true = refl
substᵈ-rename-compose σ∘ρ≗σ′ `false = refl
substᵈ-rename-compose σ∘ρ≗σ′ (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (substᵈ-rename-compose σ∘ρ≗σ′ e₁) (substᵈ-rename-compose σ∘ρ≗σ′ e₂) (substᵈ-rename-compose σ∘ρ≗σ′ e₃)
substᵈ-rename-compose σ∘ρ≗σ′ (`λ⟨ Δ ⟩ e) = cong `λ⟨ Δ ⟩_ (substᵈ-rename-compose (exts-ext σ∘ρ≗σ′) e)
substᵈ-rename-compose σ∘ρ≗σ′ (e₁ · e₂) = cong₂ _·_ (substᵈ-rename-compose σ∘ρ≗σ′ e₁) (substᵈ-rename-compose (exts++-ext++ σ∘ρ≗σ′) e₂)
substᵈ-rename-compose {σ = σ} {ρ = ρ} {σ′ = σ′} σ∘ρ≗σ′ ⟨ e ⟩ = cong ⟨_⟩ (substᵈ-rename-compose (exts↾-ext↾ {σ = σ} {ρ = ρ} {σ′ = σ′} σ∘ρ≗σ′) e)
substᵈ-rename-compose σ∘ρ≗σ′ (`let⟨ Δ ⟩ e₁ e₂) = cong₂ (`let⟨ Δ ⟩) (substᵈ-rename-compose (exts++-ext++ σ∘ρ≗σ′) e₁) (substᵈ-rename-compose (exts-ext σ∘ρ≗σ′) e₂)
substᵈ-rename-compose σ∘ρ≗σ′ (`wrap Δ e) = cong (`wrap Δ) (substᵈ-rename-compose (exts++-ext++ σ∘ρ≗σ′) e)
substᵈ-rename-compose σ∘ρ≗σ′ (`letwrap Δ e₁ e₂) = cong₂ (`letwrap Δ) (substᵈ-rename-compose σ∘ρ≗σ′ e₁) (substᵈ-rename-compose (exts-ext σ∘ρ≗σ′) e₂)

substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ ∅ = refl
substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ (_,_ {m≥n = m≥n} σ₁ (term e)) =
  cong₂ _,_ (substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ σ₁)
    (cong term (substᵈ-rename-compose (exts++-ext++ (exts↾≥-ext↾≥ m≥n σ∘ρ≗σ′)) e))
substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ (σ₁ , var x) = cong₂ _,_ (substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ σ₁) (σ∘ρ≗σ′ x)
substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ σ₁) (substSubstᵈ-renameSubst-compose σ∘ρ≗σ′ σ₂)

-- | Alternative definition of substᵈ-rename-compose using renameSubstʳᵈ.
substᵈ-renameSubstʳᵈ :  ∀ (ρ : Rename Γ Γ′) {σ : Γ″ ⊩ Γ′} {d} (σᵈ : σ ≤ᵈ′ d) (e : Term n Γ A) → substᵈ (renameSubstʳᵈ ρ σᵈ) e ≡ substᵈ σᵈ (rename ρ e)
substᵈ-renameSubstʳᵈ ρ {σ = σ} σᵈ e = sym (substᵈ-rename-compose (λ x → sym (lookup-lookup⁻¹ (lookup σ ∘ ρ) x)) e)

-- | A special case of the commutativity property where one of the substitutions is a renaming function.
substᵈ-lift-++ˢ : ∀ {d} (ρ : Rename Γ Γ′) {σ : Γ′ ⊩ Δ} (σᵈ : σ ≤ᵈ′ d) (e : Term n (Γ ++ Δ) A) →
  substᵈ (liftᵈ ρ ++ˢᵈ σᵈ) e ≡ substᵈ (liftᵈ id ++ˢᵈ σᵈ) (rename (ext++ Δ ρ) e)
substᵈ-lift-++ˢ ρ {σ = σ} σᵈ e = sym (substᵈ-rename-compose (≗-sym (lookup-lift-++ˢ ρ σ)) e)

-- | Special cases of the associativity properties where the first substitution is a renaming function.
substᵈ-renameSubstᵈ : ∀ (ρ : Rename Γ′ Γ″) {σ : Γ′ ⊩ Γ} {d} (σᵈ : σ ≤ᵈ′ d) (e : Term n Γ A) → substᵈ (renameSubstᵈ ρ σᵈ) e ≡ rename ρ (substᵈ σᵈ e)
substSubstᵈ-renameSubstᵈ : ∀ (ρ : Rename Γ′ Γ″) {σ : Γ′ ⊩ Γ} {d} (σᵈ : σ ≤ᵈ′ d) (σ₁ : Γ ⊩ Δ) → substSubstᵈ (renameSubstᵈ ρ σᵈ) σ₁ ≡ renameSubst ρ (substSubstᵈ σᵈ σ₁)

substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (` x `with σ₁) with lookup σ x | lookupᵈ σᵈ x | substSubstᵈ σᵈ σ₁
  | lookup (renameSubst ρ σ) x | lookupᵈ (renameSubstᵈ ρ σᵈ) x | substSubstᵈ (renameSubstᵈ ρ σᵈ) σ₁
  | lookup-renameSubst ρ σ x | substSubstᵈ-renameSubstᵈ ρ σᵈ σ₁
substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (` x `with σ₁) | var y | _ | σσ₁ | _ | _ | _ | refl | refl = refl
substᵈ-renameSubstᵈ ρ {σ = σ} {d = suc _} σᵈ (` x `with σ₁) | term e | term-Δ<d | σσ₁ | _ | _ | _ | refl | refl =
  trans (sym (trans (substᵈ-cong (cong (_++ˢ (renameSubst ρ σσ₁)) (trans (renameSubst-lift ρ id) (lift-resp-≗ (λ _ → refl)))) e)
    (substᵈ-lift-++ˢ ρ (renameSubstᵈ ρ σσ₁ᵈ) e))) (substᵈ-renameSubstᵈ ρ (liftᵈ id ++ˢᵈ σσ₁ᵈ) e)
  where σσ₁ᵈ = ≤ᵈ-dom σσ₁ (untermᵈ term-Δ<d)
substᵈ-renameSubstᵈ ρ σ `true = refl
substᵈ-renameSubstᵈ ρ σ `false = refl
substᵈ-renameSubstᵈ ρ σ (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (substᵈ-renameSubstᵈ ρ σ e₁) (substᵈ-renameSubstᵈ ρ σ e₂) (substᵈ-renameSubstᵈ ρ σ e₃)
substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (`λ⟨ Δ ⟩ e) =
  cong (`λ⟨ Δ ⟩_)
    (trans
      (substᵈ-cong (exts-renameSubst ρ σ) e)
      (substᵈ-renameSubstᵈ (ext ρ) (extsᵈ σᵈ) e))
substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (e₁ · e₂) =
  cong₂ _·_
    (substᵈ-renameSubstᵈ ρ σᵈ e₁)
    (trans (substᵈ-cong (exts++-renameSubst _ ρ σ) e₂)
      (substᵈ-renameSubstᵈ (ext++ _ ρ) (exts++ᵈ _ σᵈ) e₂))
substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ ⟨ e ⟩ =
  cong ⟨_⟩
    (trans (substᵈ-cong (exts↾-renameSubst ρ σ) e)
      (substᵈ-renameSubstᵈ (ext↾ ρ) (exts↾ᵈ σᵈ) e))
substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (`let⟨ Δ ⟩ e₁ e₂) =
  cong₂ (`let⟨ Δ ⟩)
    (trans (substᵈ-cong (exts++-renameSubst _ ρ σ) e₁)
      (substᵈ-renameSubstᵈ (ext++ _ ρ) (exts++ᵈ _ σᵈ) e₁))
    (trans (substᵈ-cong (exts-renameSubst ρ σ) e₂)
      (substᵈ-renameSubstᵈ (ext ρ) (extsᵈ σᵈ) e₂))
substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (`wrap Δ e) =
  cong (`wrap Δ)
    (trans (substᵈ-cong (exts++-renameSubst _ ρ σ) e)
      (substᵈ-renameSubstᵈ (ext++ _ ρ) (exts++ᵈ _ σᵈ) e))
substᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (`letwrap Δ e₁ e₂) =
  cong₂ (`letwrap Δ) (substᵈ-renameSubstᵈ ρ σᵈ e₁)
    (trans (substᵈ-cong (exts-renameSubst ρ σ) e₂)
      (substᵈ-renameSubstᵈ (ext ρ) (extsᵈ σᵈ) e₂))

substSubstᵈ-renameSubstᵈ ρ {σ = σ} σᵈ ∅ = refl
substSubstᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (_,_ {m≥n = m≥n} σ₁ (term e)) = cong₂ _,_ (substSubstᵈ-renameSubstᵈ ρ σᵈ σ₁)
  (cong term
    (trans (substᵈ-cong (trans (cong (exts++ _) (exts↾≥-renameSubst m≥n ρ σ)) (exts++-renameSubst _ (ext↾≥ m≥n ρ) (exts↾≥ m≥n σ))) e)
      (substᵈ-renameSubstᵈ (ext++ _ (ext↾≥ m≥n ρ)) (exts++ᵈ _ (exts↾≥ᵈ m≥n σᵈ)) e)))
substSubstᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (σ₁ , var x) = cong₂ _,_ (substSubstᵈ-renameSubstᵈ ρ σᵈ σ₁) (lookup-renameSubst ρ σ x)
substSubstᵈ-renameSubstᵈ ρ {σ = σ} σᵈ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (substSubstᵈ-renameSubstᵈ ρ σᵈ σ₁) (substSubstᵈ-renameSubstᵈ ρ σᵈ σ₂)

-- | exts distributes over substSubstᵈ.
exts-substSubstᵈ : ∀ {Γ″ Γ′ Γ} {σ′ : Γ″ ⊩ Γ′} (σ′ᵈ : σ′ ≤ᵈ′ d) (σ : Γ′ ⊩ Γ) →
  exts {Δ = Δ} {A = A} {m≥n = m≥n} (substSubstᵈ σ′ᵈ σ) ≡ substSubstᵈ (extsᵈ σ′ᵈ) (exts σ)
exts-substSubstᵈ {σ′ = σ′} σ′ᵈ σ = cong₂ _,_
  (sym (trans (substSubstᵈ-renameSubst-compose (lookup-exts-S σ′) σ) (substSubstᵈ-renameSubstᵈ S σ′ᵈ σ)))
  refl

-- | exts distributes over substSubst.
exts-substSubst : ∀ {Γ″ Γ′ Γ} (σ′ : Γ″ ⊩ Γ′) (σ : Γ′ ⊩ Γ) →
  exts {Δ = Δ} {A = A} {m≥n = m≥n} (substSubst σ′ σ) ≡ substSubst (exts σ′) (exts σ)
exts-substSubst σ′ σ = trans (exts-substSubstᵈ (≤ᵈ′-refl σ′) σ) (substSubstᵈ-constant (exts σ′) (exts σ))

-- | exts++ distributes over substSubstᵈ.
exts++-substSubstᵈ : ∀ {Γ″ Γ′ Γ} {σ′ : Γ″ ⊩ Γ′} (σ′ᵈ : σ′ ≤ᵈ′ d) (σ : Γ′ ⊩ Γ) → exts++ Δ (substSubstᵈ σ′ᵈ σ) ≡ substSubstᵈ (exts++ᵈ Δ σ′ᵈ) (exts++ Δ σ)
exts++-substSubstᵈ {σ′ = σ′} σ′ᵈ σ =
  cong₂ _++ˢ_
    (sym (trans (substSubstᵈ-renameSubst-compose (lookup-exts++-L σ′) σ) (substSubstᵈ-renameSubstᵈ L σ′ᵈ σ)))
    (lookup-injective-≗ λ x →
      (trans (sym (cong (substSubstItemᵈ _) (lookup-lift R x)))
          (sym (lookup-substSubstᵈ _ (lift R) x))))

-- | exts++ distributes over substSubst.
exts++-substSubst  : ∀ {Γ″ Γ′ Γ} (σ′ : Γ″ ⊩ Γ′) (σ : Γ′ ⊩ Γ) → exts++ Δ (substSubst σ′ σ) ≡ substSubst (exts++ Δ σ′) (exts++ Δ σ)
exts++-substSubst σ′ σ = trans (exts++-substSubstᵈ (≤ᵈ′-refl σ′) σ) (substSubstᵈ-constant (exts++ _ σ′) (exts++ _ σ))

-- | ⊩[]-↾⁺ distributes over substSubstItemᵈ. This is used to prove the next property.
⊩[]-↾⁺-substSubstItemᵈ : ∀ (σᵈ : σ ≤ᵈ′ d) (item : Γ ⊩[ Δ ⊢ A ^ ≤‴-step m≥n ])  → ⊩[]-↾⁺ (substSubstItemᵈ σᵈ item) ≡ substSubstItemᵈ (exts↾ᵈ σᵈ) (⊩[]-↾⁺ item)
⊩[]-↾⁺-substSubstItemᵈ σᵈ (term e) = refl
⊩[]-↾⁺-substSubstItemᵈ {σ = σ} σᵈ (var x) = sym (trans (lookup-exts↾ σ (∋-↾⁺ x)) (cong (⊩[]-↾⁺ ∘ lookup σ) (∋-↾⁻-∋-↾⁺ x)))

-- | exts↾ distributes over substSubstᵈ.
exts↾-substSubstᵈ : ∀ {Γ″ Γ′ Γ : Context n} {σ′ : Γ″ ⊩ Γ′} (σ′ᵈ : σ′ ≤ᵈ′ d) (σ : Γ′ ⊩ Γ) →
  exts↾ (substSubstᵈ σ′ᵈ σ) ≡ substSubstᵈ (exts↾ᵈ σ′ᵈ) (exts↾ σ)
exts↾-substSubstᵈ σ′ᵈ σ = lookup-injective-≗ λ x →
  trans (lookup-exts↾ (substSubstᵈ σ′ᵈ σ) x)
    (trans (cong  ⊩[]-↾⁺ (lookup-substSubstᵈ σ′ᵈ σ (∋-↾⁻ x)))
      (trans (⊩[]-↾⁺-substSubstItemᵈ σ′ᵈ (lookup σ (∋-↾⁻ x)))
        (trans (sym (cong (substSubstItemᵈ _ ) (lookup-exts↾ σ x)))
          (sym (lookup-substSubstᵈ (exts↾ᵈ σ′ᵈ) (exts↾ σ) x)))))

-- | exts↾≥ distributes over substSubstᵈ.
exts↾≥-substSubstᵈ : ∀ (m≥n : m ≥‴ n) {Γ″ Γ′ Γ : Context n} {σ′ : Γ″ ⊩ Γ′} (σ′ᵈ : σ′ ≤ᵈ′ d) (σ : Γ′ ⊩ Γ) →
  exts↾≥ m≥n (substSubstᵈ σ′ᵈ σ) ≡ substSubstᵈ (exts↾≥ᵈ m≥n σ′ᵈ) (exts↾≥ m≥n σ)
exts↾≥-substSubstᵈ ≤‴-refl σ′ᵈ σ = refl
exts↾≥-substSubstᵈ (≤‴-step m≥n) σ′ᵈ σ = trans (cong (exts↾≥ m≥n) (exts↾-substSubstᵈ σ′ᵈ σ)) (exts↾≥-substSubstᵈ m≥n (exts↾ᵈ σ′ᵈ) (exts↾ σ))

-- | ⊩[]-inject₁⁻ distributes over substSubstItem. This is used to prove the next property.
⊩[]-inject₁⁻-substSubstItem : {Γ′ Γ : Context (suc n)} (σ :  inject₁ Γ′ ⊩ inject₁ Γ) (item : inject₁ Γ ⊩[ Δ ⊢ A ^ ≤‴-step m≥n ]) → ⊩[]-inject₁⁻ (substSubstItem σ item) ≡ substSubstItem (⊩-inject₁⁻ σ) (⊩[]-inject₁⁻ item)
⊩[]-inject₁⁻-substSubstItem {m≥n = m≥n} σ (term e) = cong term (sym
  (trans (substᵈ-rename-compose {σ′ᵈ = exts++ᵈ _ (exts↾≥ᵈ m≥n (renameSubstʳᵈ (∋-inject₁⁻ ∘ ∋-↾⁻) (≤ᵈ′-refl (⊩-inject₁⁻ σ))))} (exts++-ext++ (exts↾≥-ext↾≥ m≥n (λ x → sym (lookup-renameSubstʳ (∋-inject₁⁻ ∘ ∋-↾⁻) (⊩-inject₁⁻ σ) x)))) e)
    (trans
      (substᵈ-cong (trans (cong (exts++ _) (cong (exts↾≥ m≥n) (⊩-inject₁⁻≡exts↾ σ)))
        (trans (cong (exts++ _) (exts↾≥-renameSubst m≥n (∋-inject₁⁻ ∘ ∋-↾⁻) (exts↾ σ)))
          (exts++-renameSubst _ (ext↾≥ m≥n (∋-inject₁⁻ ∘ ∋-↾⁻)) (exts↾≥ m≥n (exts↾ σ))))) e)
      (trans (substᵈ-constant _ e) (substᵈ-renameSubstᵈ _ _ e)))))
⊩[]-inject₁⁻-substSubstItem σ (var x) = ⊩[]-inject₁⁻-lookup σ x

-- | ⊩-inject₁⁻ distributes over substSubst.
⊩-inject₁⁻-substSubst : ∀ {Γ″ Γ′ Γ : Context (suc n)} (σ′ : inject₁ Γ″ ⊩ inject₁ Γ′) (σ : inject₁ Γ′ ⊩ inject₁ Γ) → ⊩-inject₁⁻ (substSubst σ′ σ) ≡ substSubst (⊩-inject₁⁻ σ′) (⊩-inject₁⁻ σ)
⊩-inject₁⁻-substSubst {Γ = ∅} σ′ ∅ = refl
⊩-inject₁⁻-substSubst {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} σ′ (σ , item) = cong₂ _,_ (⊩-inject₁⁻-substSubst σ′ σ) (⊩[]-inject₁⁻-substSubstItem σ′ item)
⊩-inject₁⁻-substSubst {Γ = Γ₁ ++ Γ₂} σ′ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (⊩-inject₁⁻-substSubst σ′ σ₁) (⊩-inject₁⁻-substSubst σ′ σ₂)


-- | The main lemmas used to prove the associativity of substitution.
-- The lemmas are proven by induction on both d and d′.
substᵈ-useItemᵈ : {σ : Γ′ ⊩ Γ} (σᵈ : σ ≤ᵈ′ d′) {item : Γ ⊩[ Δ ⊢ A ^ ≤‴-refl ]} (itemᵈ : item ≤ᵈ″ d)
  → (σ₁ : Γ ⊩ Δ) → substᵈ σᵈ (useItemᵈ itemᵈ σ₁) ≡ useItemᵈ (≤ᵈ″-refl (substSubstItemᵈ σᵈ item)) (substSubstᵈ σᵈ σ₁)
substᵈ-substᵈ-compose : ∀ {Γ″ Γ′ Γ} {σ′ : Γ″ ⊩ Γ′} (σ′ᵈ : σ′ ≤ᵈ′ d′) {σ : Γ′ ⊩ Γ} (σᵈ : σ ≤ᵈ′ d)
  → (e : Γ ⊢ A ^ n) → substᵈ σ′ᵈ (substᵈ σᵈ e) ≡ subst (substSubstᵈ σ′ᵈ σ) e
substSubstᵈ-substSubstᵈ-compose : ∀ {Γ″ Γ′ Γ} {σ′ : Γ″ ⊩ Γ′} (σ′ᵈ : σ′ ≤ᵈ′ d′) {σ : Γ′ ⊩ Γ} (σᵈ : σ ≤ᵈ′ d)
  → (σ₁ : Γ ⊩ Δ) → substSubstᵈ σ′ᵈ (substSubstᵈ σᵈ σ₁) ≡ substSubst (substSubstᵈ σ′ᵈ σ) σ₁

substᵈ-useItemᵈ {σ = σ} σᵈ {item = var x} itemᵈ σ₁ = useItemᵈ-constant (lookup σ x) (substSubstᵈ σᵈ σ₁)
substᵈ-useItemᵈ {d′ = d′} {d = suc d} {σ = σ} σᵈ {item = term e} itemᵈ σ₁ =
  begin
    substᵈ σᵈ (useItemᵈ {item = (term e)} itemᵈ σ₁)
  ≡⟨⟩
    substᵈ σᵈ (substᵈ (liftᵈ id ++ˢᵈ (≤ᵈ-dom σ₁ (untermᵈ itemᵈ))) e) -- d′ = d′, d = d - 1, so d + d′ decreases by 1
  ≡⟨ substᵈ-substᵈ-compose {d′ = d′} {d = d} σᵈ (liftᵈ id ++ˢᵈ (≤ᵈ-dom σ₁ (untermᵈ itemᵈ))) e ⟩
    subst (substSubstᵈ σᵈ (lift id ++ˢ σ₁)) e
  ≡⟨ cong (λ σ → subst σ e)
      (cong₂ _++ˢ_
        (trans (substSubstᵈ-lift-idʳ σᵈ) (sym (trans (substSubstᵈ-renameSubst-compose (λ x → refl) σ) (substSubstᵈ-liftᵈ-id σ))))
        (lookup-injective-≗ λ x → sym (trans (lookup-substSubstᵈ _ (lift R) x) ((cong (substSubstItemᵈ _) (lookup-lift R x)))))) ⟩
    subst (substSubstᵈ (liftᵈ id ++ˢᵈ ≤ᵈ-dom (substSubstᵈ σᵈ σ₁) (untermᵈ itemᵈ)) (exts++ _ σ)) e
  ≡⟨ sym (substᵈ-substᵈ-compose {d′ = d} {d = d′} (liftᵈ id ++ˢᵈ ≤ᵈ-dom (substSubstᵈ σᵈ σ₁) (untermᵈ itemᵈ)) (exts++ᵈ _ σᵈ) e) ⟩
    substᵈ (liftᵈ id ++ˢᵈ ≤ᵈ-dom (substSubstᵈ σᵈ σ₁) (untermᵈ itemᵈ)) (substᵈ (exts++ᵈ _ σᵈ) e) -- d′ = d - 1, d = d′, so d + d′ decreases by 1
  ≡⟨ substᵈ-constant (lift id ++ˢ (substSubstᵈ σᵈ σ₁)) (substᵈ (exts++ᵈ _ σᵈ) e) ⟩
    useItemᵈ (≤ᵈ″-refl (substSubstItemᵈ σᵈ (term e))) (substSubstᵈ σᵈ σ₁)
  ∎
  where open ≡-Reasoning

substᵈ-substᵈ-compose {d′ = d′} {d = d} σ′ᵈ {σ = σ} σᵈ (` x `with σ₁) =
  begin
    substᵈ σ′ᵈ (substᵈ σᵈ (` x `with σ₁))
  ≡⟨ substᵈ-useItemᵈ {d′ = d′} {d = d} σ′ᵈ (lookupᵈ σᵈ x) (substSubstᵈ σᵈ σ₁) ⟩
    useItemᵈ (≤ᵈ″-refl (substSubstItemᵈ σ′ᵈ (lookup σ x))) (substSubstᵈ σ′ᵈ (substSubstᵈ σᵈ σ₁))
  ≡⟨ trans (useItemᵈ-cong₂ (sym (lookup-substSubstᵈ σ′ᵈ σ x)) refl) (useItemᵈ-constant (lookup (substSubstᵈ σ′ᵈ σ) x) ((substSubstᵈ σ′ᵈ (substSubstᵈ σᵈ σ₁)))) ⟩
    useItemᵈ (lookupᵈ (≤ᵈ′-refl (substSubstᵈ σ′ᵈ σ)) x) (substSubstᵈ σ′ᵈ (substSubstᵈ σᵈ σ₁))
  ≡⟨ cong (useItemᵈ (lookupᵈ (≤ᵈ′-refl (substSubstᵈ σ′ᵈ σ)) x)) (substSubstᵈ-substSubstᵈ-compose σ′ᵈ σᵈ σ₁) ⟩
    useItemᵈ (lookupᵈ (≤ᵈ′-refl (substSubstᵈ σ′ᵈ σ)) x) (substSubst (substSubstᵈ σ′ᵈ σ) σ₁) 
  ≡⟨⟩
    subst (substSubstᵈ σ′ᵈ σ) (` x `with σ₁)
  ∎
  where open ≡-Reasoning
substᵈ-substᵈ-compose σ′ᵈ σᵈ `true = refl
substᵈ-substᵈ-compose σ′ᵈ σᵈ `false = refl
substᵈ-substᵈ-compose σ′ᵈ σᵈ (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (substᵈ-substᵈ-compose σ′ᵈ σᵈ e₁) (substᵈ-substᵈ-compose σ′ᵈ σᵈ e₂) (substᵈ-substᵈ-compose σ′ᵈ σᵈ e₃)
substᵈ-substᵈ-compose σ′ᵈ {σ = σ} σᵈ (`λ⟨ Δ ⟩ e) = cong `λ⟨ Δ ⟩_
  (trans (substᵈ-substᵈ-compose (extsᵈ σ′ᵈ) (extsᵈ σᵈ) e)
    (trans (substᵈ-cong (sym (exts-substSubstᵈ σ′ᵈ σ)) e)
      (substᵈ-constant (exts (substSubstᵈ σ′ᵈ σ)) e)))
substᵈ-substᵈ-compose σ′ᵈ {σ = σ} σᵈ (e₁ · e₂) =
  cong₂ _·_ (substᵈ-substᵈ-compose σ′ᵈ σᵈ e₁)
    (trans (substᵈ-substᵈ-compose (exts++ᵈ _ σ′ᵈ) (exts++ᵈ _ σᵈ) e₂)
      (trans (substᵈ-cong (sym (exts++-substSubstᵈ σ′ᵈ σ)) e₂)
        (substᵈ-constant (exts++ _ (substSubstᵈ σ′ᵈ σ)) e₂)))
substᵈ-substᵈ-compose σ′ᵈ {σ = σ} σᵈ ⟨ e ⟩ =
  cong ⟨_⟩
    (trans (substᵈ-substᵈ-compose (exts↾ᵈ σ′ᵈ) (exts↾ᵈ σᵈ) e)
      (trans (substᵈ-cong (sym (exts↾-substSubstᵈ σ′ᵈ σ)) e)
        (substᵈ-constant (exts↾ (substSubstᵈ σ′ᵈ σ)) e)))
substᵈ-substᵈ-compose σ′ᵈ {σ = σ} σᵈ (`let⟨ Δ ⟩ e₁ e₂) =
  cong₂ (`let⟨ Δ ⟩)
    (trans (substᵈ-substᵈ-compose (exts++ᵈ _ σ′ᵈ) (exts++ᵈ _ σᵈ) e₁)
      (trans (substᵈ-cong (sym (exts++-substSubstᵈ σ′ᵈ σ)) e₁)
        (substᵈ-constant (exts++ _ (substSubstᵈ σ′ᵈ σ)) e₁)))
    (trans (substᵈ-substᵈ-compose (extsᵈ σ′ᵈ) (extsᵈ σᵈ) e₂)
      (trans (substᵈ-cong (sym (exts-substSubstᵈ σ′ᵈ σ)) e₂)
        (substᵈ-constant (exts (substSubstᵈ σ′ᵈ σ)) e₂)))
substᵈ-substᵈ-compose σ′ᵈ {σ = σ} σᵈ (`wrap Δ e) =
  cong (`wrap Δ)
    (trans (substᵈ-substᵈ-compose (exts++ᵈ _ σ′ᵈ) (exts++ᵈ _ σᵈ) e)
      (trans (substᵈ-cong (sym (exts++-substSubstᵈ σ′ᵈ σ)) e)
        (substᵈ-constant (exts++ _ (substSubstᵈ σ′ᵈ σ)) e)))
substᵈ-substᵈ-compose σ′ᵈ {σ = σ} σᵈ (`letwrap Δ e₁ e₂) =
  cong₂ (`letwrap Δ) (substᵈ-substᵈ-compose σ′ᵈ σᵈ e₁)
    (trans (substᵈ-substᵈ-compose (extsᵈ σ′ᵈ) (extsᵈ σᵈ) e₂)
      (trans (substᵈ-cong (sym (exts-substSubstᵈ σ′ᵈ σ)) e₂)
        (substᵈ-constant (exts (substSubstᵈ σ′ᵈ σ)) e₂)))

substSubstᵈ-substSubstᵈ-compose σ′ᵈ σᵈ ∅ = refl
substSubstᵈ-substSubstᵈ-compose σ′ᵈ {σ = σ} σᵈ (σ₁ , var x) = cong₂ _,_ (substSubstᵈ-substSubstᵈ-compose σ′ᵈ σᵈ σ₁) (sym (lookup-substSubstᵈ σ′ᵈ σ x))
substSubstᵈ-substSubstᵈ-compose σ′ᵈ {σ = σ} σᵈ (_,_ {m≥n = m≥n} σ₁ (term e)) = cong₂ _,_ (substSubstᵈ-substSubstᵈ-compose σ′ᵈ σᵈ σ₁)
  (cong term (trans (substᵈ-substᵈ-compose (exts++ᵈ _ (exts↾≥ᵈ m≥n σ′ᵈ)) (exts++ᵈ _ (exts↾≥ᵈ m≥n σᵈ)) e)
    (trans (substᵈ-cong (sym (trans (cong (exts++ _) (exts↾≥-substSubstᵈ m≥n σ′ᵈ σ)) (exts++-substSubstᵈ _ _))) e)
      (substᵈ-constant ((exts++ _ (exts↾≥ m≥n (substSubstᵈ σ′ᵈ σ)))) e))))
substSubstᵈ-substSubstᵈ-compose σ′ᵈ σᵈ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (substSubstᵈ-substSubstᵈ-compose σ′ᵈ σᵈ σ₁) (substSubstᵈ-substSubstᵈ-compose σ′ᵈ σᵈ σ₂)

-- | The associativity property for substitution on terms
subst-substSubst : (σ′ : Γ″ ⊩ Γ′) (σ : Γ′ ⊩ Γ) (e : Γ ⊢ A ^ n) → subst (substSubst σ′ σ) e ≡ subst σ′ (subst σ e)
subst-substSubst σ′ σ e = sym (substᵈ-substᵈ-compose (≤ᵈ′-refl σ′) (≤ᵈ′-refl σ) e)

-- | The associativity property for substitution on substitutions
substSubst-substSubst : (σ′ : Γ″ ⊩ Γ′) (σ : Γ′ ⊩ Γ) (σ₁ : Γ ⊩ Δ) → substSubst σ′ (substSubst σ σ₁) ≡ substSubst (substSubst σ′ σ) σ₁
substSubst-substSubst σ′ σ σ₁ = substSubstᵈ-substSubstᵈ-compose (≤ᵈ′-refl σ′) (≤ᵈ′-refl σ) σ₁

-- | The commutativity property for a single entry
subst-, : ∀ (σ : Γ′ ⊩ Γ) (item : Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) (e : Γ ,[ Δ ⊢ A ^ m≥n ] ⊢ B ^ n) →
  subst (σ , item) e ≡ subst (lift id , item) (subst (exts σ) e)
subst-, σ item e =
  trans
    (cong (λ σ′ → subst σ′ e) (cong (_, item)
      (sym
        (trans (substSubstᵈ-renameSubst-compose {σ′ = lift id} {σ′ᵈ = liftᵈ id} (λ x → refl) σ)
          (trans (substSubstᵈ-constant (lift id) σ) (substSubst-lift-id σ))))))
    (subst-substSubst (lift id , item) (exts σ) e) 

-- | The commutativity property for multiple entries
subst-++ˢ : ∀ (σ : Γ′ ⊩ Γ) (σ′ : Γ′ ⊩ Δ) (e : Term n (Γ ++ Δ) A) →
  subst (σ ++ˢ σ′) e ≡ subst (lift id ++ˢ σ′) (subst (exts++ Δ σ) e)
subst-++ˢ σ σ′ e =
  trans
    (cong (λ σ″ → subst σ″ e) (cong₂ _++ˢ_
      (sym (trans (substSubstᵈ-renameSubst-compose {σ′ = lift id} {σ′ᵈ = liftᵈ id} (λ x → refl) σ)
        (trans (substSubstᵈ-constant (lift id) σ) (substSubst-lift-id σ))))
      (sym (lookup-injective-≗ λ x → trans (lookup-substSubstᵈ _ (lift R) x) (cong (substSubstItemᵈ _) (lookup-lift R x))))))
    (subst-substSubst (lift id ++ˢ σ′) (exts++ _ σ) e)