Hello! I generalized the statement of commute-subst-rename and added some definitions and lemmas in the Substitution appendix.

Here is the previous statement of commute-subst-rename:

commute-subst-rename : ∀{Γ Δ}{M : Γ ⊢ ★}{σ : Subst Γ Δ}
                        {ρ₁ : Rename Γ (Γ , ★)}{ρ₂ : Rename Δ (Δ , ★)}
                     → (∀{x : Γ ∋ ★} → exts σ (ρ₁ x) ≡ rename ρ₂ (σ x))
                     → subst (exts σ) (rename ρ₁ M) ≡ rename ρ₂ (subst σ M)

And suggested revision:

Commute : ∀ {Γ₁ Γ₂ Δ₁ Δ₂} → Subst Γ₂ Δ₂ → Rename Γ₁ Γ₂ → Subst Γ₁ Δ₁ → Rename Δ₁ Δ₂ → Set
Commute {Γ₁ = Γ₁} σ₁ ρ₁ σ₂ ρ₂ = ∀ (x : Γ₁ ∋ ★) → σ₁ (ρ₁ x) ≡ rename ρ₂ (σ₂ x)

commute-subst-rename : ∀ {Γ₁ Γ₂ Δ₁ Δ₂}
                         {σ₁ : Subst Γ₂ Δ₂} {ρ₁ : Rename Γ₁ Γ₂} {σ₂ : Subst Γ₁ Δ₁} {ρ₂ : Rename Δ₁ Δ₂}
                     → Commute σ₁ ρ₁ σ₂ ρ₂
                     → ∀ (M : Γ₁ ⊢ ★) → subst σ₁ (rename ρ₁ M) ≡ rename ρ₂ (subst σ₂ M)

Old statement is an instance of the new one, where σ₁ = exts σ and σ₂ = σ.

The motivation for this change is two folded. First, it is simply more general, so it has more applications in theory. Second and more importantly, the new proof can be naturally adapted to typed setting, while the older one is not. Consider the previous proof of commute-subst-rename for the ƛ_ case.

commute-subst-rename {Γ}{Δ}{ƛ N}{σ}{ρ₁}{ρ₂} H =
   cong ƛ_ (commute-subst-rename{Γ , ★}{Δ , ★}{N}
               {exts σ}{ext ρ₁}{ext ρ₂} (λ {x} → H′ {x}))
   where
   H′ : {x : Γ , ★ ∋ ★} → exts (exts σ) (ext ρ₁ x) ≡ rename (ext ρ₂) (exts σ x)
   H′ = ...

In the type of H′, exts σ on the LHS and exts σ on the RHS may seem equal, but each occurrence of exts operations are responsible for different variables. If we annotate ext/exts operations with relatedness, the type would be something like the following:

H′ : {x : Γ , ★ ∋ ★} → exts₂ (exts₁ σ) (ext₂ ρ₁ x) ≡ rename (ext₂ ρ₂) (exts₂ σ x)

However the use of H′ in commute-subst-rename{Γ , ★}{Δ , ★}{N}{exts σ}{ext ρ₁}{ext ρ₂} (λ {x} → H′ {x}) requires exts₁ σ and exts₂ σ to be judgementally equal. This is the case in our untyped setting, but it could be false in general, for instance in intrinsically typed setting. The generalized version does not have this problem.

I also fixed text according to changed proof structure.