\startitemize
\item Before starting normalization, all binders in the function are made
unique. This is done by generating a fresh binder for every binder used. This
also replaces binders that did not pose any conflict, but it does ensure that
all binders within the function are generated by the same unique supply. See
\startitemize
\item Before starting normalization, all binders in the function are made
unique. This is done by generating a fresh binder for every binder used. This
also replaces binders that did not pose any conflict, but it does ensure that
all binders within the function are generated by the same unique supply. See