\noindent{\em Proof.} We aim to use the same approach and conventions as in the previous two proofs but hit a minor snag. The $g$-rules for R1l include
\[
  g_{\ip\beta}  = \delta_{\ip\beta} + Tg_{\ipp,\beta}+(1-T)g_{\ip,\beta}
  \qquad\text{and}\qquad
  g_{\alpha,\ip} = g_{\alpha i} + (1-T)g_{\alpha\ip} + \delta_{\alpha,\ip},
\]
and if these are implemented as simple left to right replacement rules, they lead to infinite recursion. Fortunately, these rules can be rewritten in the form
\[
  g_{\ip\beta}  = T^{-1}\delta_{\ip\beta} +g_{\ipp,\beta}
  \qquad\text{and}\qquad
  g_{\alpha,\ip} = T^{-1}g_{\alpha i} + T^{-1}\delta_{\alpha,\ip},
\]
which makes perfectly valid replacement rules. We thus redefine:

\nbpdfInput{Snips/Implementation/52.pdf}
The same issue does not arise for R1r (!), and thus the following lines conclude the proof:
{\def\nbpdfPostInput{\hfill}

\nbpdfInput{Snips/Implementation/53.pdf}
\nbpdfOutput{Snips/Implementation/54.pdf}
}\endpar{\ref{prop:R1s}}