diff --git a/spec/doc.tex b/spec/doc.tex
index a50de4ad210745b63c83626192c9aa723ebadd83..f68c66c324944b3760e8c28c18ca4be0ca277e54 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -663,7 +663,7 @@ An Alethe proof is a list of commands.
 (assume h1 (not (p a)))
 (assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
 ...
-(anchor :step t9 :args ((:= z2 vr4)))
+(anchor :step t9 :args ((vr4 U) (:= z2 vr4)))
 (step t9.t1 (cl (= z2 vr4)) :rule refl)
 (step t9.t2 (cl (= (p z2) (p vr4)))
          :rule cong :premises (t9.t1))