diff --git a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
index 88dae9a7..291fa7d4 100644
--- a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
+++ b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
@@ -288,7 +288,7 @@
   of~$\delta$. Any sequence of G\"odel numbers of sub-!!{derivation}s
   of~$\delta$ is a subsequence of it. Being a subsequence of is a
   primitive recursive relation: $\fn{Subseq}(s, s')$ holds iff
-  $\bforall{i<\len{s}}{\lexists[j<\len{s'}][(s)_i = (s)_j]}$. Being an
+  $\bforall{i<\len{s}}{\lexists[j<\len{s'}][(s)_i = (s')_j]}$. Being an
   immediate sub-!!{derivation} is as well: $\fn{Subderiv}(d, d')$ iff
   $\bexists{j<(d')_0}{d = (d')_j}$. So we can define
   $\fn{OpenAssum}(z, d)$ by
@@ -297,7 +297,7 @@
       \land (s)_0 = d \land {}} \\
     \bexists{n<d}{((s)_{\len{s} \tsub 1} = \tuple{0, z, n} \land {}}\\
       \bforall{i<(\len{s} \tsub 1)}{(\fn{Subderiv}((s)_{i+1}, (s)_i) \land {}}\\
-      \fn{DischargeLabel}((s)_{i+1}) \neq n))).
+      \fn{DischargeLabel}((s)_i) \neq n))).
   \end{multline*}
 \end{proof}