diff --git a/spec/changelog.tex b/spec/changelog.tex
index 0e0dc1b913653c8f2bd53f66a973f7d814abe3d5..8fea177adeca471973c9433f8e11a3b083503faa 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -1,6 +1,6 @@
 \subsection*{Unreleased}
 
-Braking changes:
+Breaking changes:
 \begin{itemize}
   \item Allow arbitrary extra annotations in \texttt{assume} commands.
 \end{itemize}
diff --git a/spec/doc.tex b/spec/doc.tex
index 2ce54c6d3005efcca90755c57c20ae17dca8b2cb..a50de4ad210745b63c83626192c9aa723ebadd83 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -858,12 +858,12 @@ expressed as a concrete proof.
 \begin{AletheVerb}
 (assume h1 (forall ((x S)) (P x)))
 (assume h2 (not (forall ((y S)) (P y))))
-(anchor :step t5 :args ((:= x y)))
+(anchor :step t5 :args ((y S) (:= x y)))
 (step t3 (cl (= x y)) :rule refl)
 (step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
 (step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
                               :rule bind)
-(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
+(step t6 (cl (not (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
              (not (forall ((x S)) (P x)))
              (forall ((y S)) (P y))) :rule equiv_pos2)
 (step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))