explain Subst and Rename in Confluence chapter (#1022)

src/plfa/part2/Confluence.lagda.md

@@ -67,7 +67,7 @@ open import plfa.part2.Untyped
   using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; begin_; _—→⟨_⟩_; _—↠⟨_⟩_; _∎;
   abs-cong; appL-cong; appR-cong; —↠-trans;
   _⊢_; _∋_; `_; #_; _,_; ★; ƛ_; _·_; _[_];
-  rename; ext; exts; Z; S_; subst; subst-zero)
+  rename; ext; exts; Z; S_; subst; subst-zero; Context)
 ```
 
 ## Parallel Reduction
@@ -249,13 +249,26 @@ We cannot prove this directly by induction, so we
 generalize it to: if `N ⇛ N′` and
 the substitution `σ` pointwise parallel reduces to `τ`,
 then `subst σ N ⇛ subst τ N′`. We define the notion
-of pointwise parallel reduction as follows.
+of pointwise parallel reduction of a substitution as follows.
 
 ```agda
 par-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
 par-subst {Γ}{Δ} σ σ′ = ∀{A}{x : Γ ∋ A} → σ x ⇛ σ′ x
 ```
 
+In the type of `par-subst` we make use of the shorthand `Subst Γ Δ`
+for the type of a substitution. Similarly, we shall make use of
+`Rename Γ Δ` for the type of a renaming. Both are defined in Chapter
+[Substitution](/Substitution/) and have the following meaning.
+
+```agda
+_ : ∀(Γ Δ : Context) → Set₁
+_ = λ Γ Δ →   Rename Γ Δ ≡ ∀{A} → Γ ∋ A → Δ ∋ A
+
+_ : ∀(Γ Δ : Context) → Set₁
+_ = λ Γ Δ →   Subst Γ Δ ≡ ∀{A} → Γ ∋ A → Δ ⊢ A
+```
+
 Because substitution depends on the extension function `exts`, which
 in turn relies on `rename`, we start with a version of the
 substitution lemma, called `par-rename`, that is specialized to