diff --git a/spec/changelog.tex b/spec/changelog.tex
index 9f203ea2207f8bac6bc6db6cdbc5660da1082cf5..0da3149ecd13c22a656c4920d94841b2ef835c7c 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -23,6 +23,7 @@ Clarifications and corrected errors:
         omitted if the list is empty.
   \item Fix mistake in proof grammar.  It now uses the \texttt{context\_annotation}
         non-terminal in the rule for the \texttt{anchor} command.
+  \item Fix the example of \proofRule{onepoint}.
 \end{itemize}
 
 \subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 2152cdadc91a1af19450da1ea5f4d348fc9db219..f19f9282a1ef3edd84406b56efe65569e3720bb1 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1227,7 +1227,7 @@ An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x
 \rightarrow (f\,x)\land (f\,y))$ look like this:
 
 \begin{AletheVerb}
-(anchor :step t3 :args ((:= y x)))
+(anchor :step t3 :args ((x S) (:= (y S) x)))
 (step t3.t1 (cl (= x y)) :rule refl)
 (step t3.t2 (cl (= (= x y) (= x x)))
     :rule cong :premises (t3.t1))
@@ -1242,7 +1242,7 @@ An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x
 (step t3 (cl (=
         (forall ((x S) (y S)) (=> (= x y) (and (f x) (f y))))
         (forall ((x S))       (=> (= x x) (and (f x) (f x))))))
-    :rule qnt_simplify)
+    :rule onepoint)
 \end{AletheVerb}
 \end{RuleExample}