diff --git a/spec/doc.tex b/spec/doc.tex
index a2257ec3170e93d0f31fad48014ef4781650035d..84e9119216d210998afadaa6f4cd1cb442434919 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -2335,6 +2335,15 @@ with $1 \leq k \leq n$.
       &(\currule)\\
     \end{plList}
   \end{plContainer}
+
+  \begin{plContainer}
+    \begin{plList}
+      \Gamma\proofsep&
+      i.& \operatorname{\forall x_1, \dots, x_n.} \varphi \leftrightarrow \operatorname{\neg\exists x_1, \dots, x_n.} \neg\varphi
+      &(\currule)\\
+    \end{plList}
+  \end{plContainer}
+
 \end{proof-rule}
 
 \begin{proof-rule}{and_simplify}{veriT}