Explicit substitutions

These symbols are working notation only in chapter 54 and appendix A.

symbol	meaning	first
symbol	meaning	first
$A[\gamma ]$	substitution action on a type or term	chapter 54
$\mathsf{id}$	identity substitution	chapter 54
$\gamma \circ \delta$	composition of substitutions	chapter 54
$\mathbf{p}$	context projection/weakening substitution	chapter 54
$\mathbf{q}$	generic last variable	chapter 54
$⟨\gamma ,a⟩$	extension of a substitution by a term	chapter 54
${\gamma }^{+}$	lifting under one context extension	chapter 54