Fix example for onepoint proof rule

Addresses #40

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}}

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}