diff --git a/protocol/protocol.tex b/protocol/protocol.tex
index d5227fd8..ab75b6ef 100644
--- a/protocol/protocol.tex
+++ b/protocol/protocol.tex
@@ -9782,6 +9782,8 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
     \item Minor changes to avoid clashing notation for
           Edwards curves $\Edwards{a,d}$, Montgomery curves $\Montgomery{A,B}$, and
           extractors $\Extractor{\Adversary}$.
+    \item Correct a use of $\GroupJ$ that should have been $\MontCurve$ in the proof of
+          \theoremref{thmdistinctxcriterion}.
 } %sapling
 \end{itemize}
 
@@ -11323,7 +11325,7 @@ $P_1 = \scalarmult{k_1}{Q}$, there can be only one other point $-P_1$ with
 the same $x$-coordinate. (This follows from the fact that the curve equation
 determines $\pm y$ as a function of $x$.)
 But $-P_1 = \scalarmult{-1}{\scalarmult{k_1}{Q}} = \scalarmult{-k_1}{Q}$.
-Since $\fun{k \typecolon \bigrange{-\halfs}{\halfs}}{\scalarmult{k}{Q} \typecolon \GroupJ}$
+Since $\fun{k \typecolon \bigrange{-\halfs}{\halfs}}{\scalarmult{k}{Q} \typecolon \MontCurve}$
 is injective and $k_\barerange{1}{2}$ are in $\bigrange{-\halfs}{\halfs}$,
 then $k_2 = \pm k_1$ (contradiction).
 \end{proof}