At the very end of Section 4.1 (page 11), a paragraph added in
form of a remark:
There is a less radical approach for the circumvention of
administrative reductions than the introduction of another set of
variables, due to Andou [1,2]. The need above,
namely that $\mu$-bound variables $x$ only occur free in subterms of
the form $xt$, is turned into the definition of a \emph{regular} term,
and only regular terms are studied. (Clearly, if one knows that $x$ is
bound by some $\mu x^{\neg A}$, one might replace free occurrences of
$x$ by $\lambda y^A. xy$ and arrive at a regular term.) Then, one may
define reduction as in $\lambda\mu$-calculus, and regularity is not
lost during reduction. However, we would still only obtain a common
reduct for the translated terms on both sides of the new
$\mu$-reduction rule. For a proper simulation of $\mu$-reduction, it
will be essential to translate the type $\neg A$ of such a variable
$x$ into $\neg A'$ and not into $(\neg A)'$. Therefore,
compositionality considerations require to open up a new namespace of
``$\mu$-variables'' for the variables that receive this special
treatment of their types during translation.
[1] Yuuki Andou. A normalization-procedure for the
first order classical natural deduction with full logical symbols,
Tsukuba Journal of Mathematics, vol. 19(1995), no.1, pp.153--162.
[2] Yuuki Andou. Church-Rosser property of a simple reduction for
full first-order classical natural deduction, Annals of
Pure and Applied Logic, vol.119(2003), pp.225--237.