diff --git a/spec/doc.tex b/spec/doc.tex
index 648d9b742e5eb4cbc169370fe7668a1abb169cd0..5c93ec45dd51538b9b6e66e02de3b1e29d789d56 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -442,24 +442,9 @@ terms of sort $\mathbf{Bool}$.
 %
 We use $=$ to denote syntactic equality and $\simeq$ to denote the sorted
 equality predicate.
-%
-We also use the notion of complementary literals
-very liberally: $\varphi = \bar{\psi}$ holds if the terms obtained
-after removing all leading negations from $\varphi$ and $\bar{\psi}$
-are syntactically equal and the number of leading negations is even
-for $\varphi$ and odd for $\psi$, or vice versa.  To simplify the
+To simplify the
 notation we will omit the sort of terms when possible.
-\begin{comment}{Haniel Barbosa}
-  This notation is clashing with the notation of sequences of symbols, like in
-  $\bar x$ for $x_1, \dots, x_n$.
-
-  Maybe we could use an alternative notation for ``normalization under double
-  negation elimination''? Like $\llfloor \varphi \rrfloor_{\neg\neg}$? I find
-  the use of ``complementary literal'' to refer this a bit confusing
-  anyway. There are very few uses in the rules (only tautology, and/or simps),
-  so we could even not introduce a notation and just refer to ``normalized under
-  double negation elimination''.
-\end{comment}
+
 \begin{example} The following example shows a simple Alethe proof.
 It uses quantifier instantiation and resolution to show a contradiction.
 The sections below step-by-step describe the concepts necessary to
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 5f0decf14c5e25263eca434b3222b4c39923b2de..ed23cb8da3da255d69607580cac8eb84f47feac8 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -87,7 +87,12 @@ serves only informational purpose.
       \proofsep& j.& \top &(\currule; i)\\
     \end{plList}
   \end{plContainer}
-  and $\varphi_i = \bar\varphi_j$.
+  and $\varphi_i$, $\varphi_j$ are such that
+  \begin{align*}
+  \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
+  \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
+  \end{align*}
+  and one of $n, m$ is odd and the other even.  Either can be $0$.
 \end{proof-rule}
 
 \begin{proof-rule}{contraction}{veriT}
@@ -986,8 +991,13 @@ The possible transformations are:
     \land \dots \land \varphi_{n'} $ where the right hand side has all
     repeated literals removed.
     \item $\varphi_1 \land\dots\land \bot\land\dots \land \varphi_n \leftrightarrow \bot$
-    \item $\varphi_1 \land\dots\land \varphi_i\land \dots \land \varphi_j\land\dots \land \varphi_n \leftrightarrow \bot$ if
-      $\varphi_i = \bar{\varphi_j}$
+    \item $\varphi_1 \land\dots\land \varphi_i\land \dots \land \varphi_j\land\dots \land \varphi_n \leftrightarrow \bot$
+  and $\varphi_i$, $\varphi_j$ are such that
+  \begin{align*}
+  \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
+  \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
+  \end{align*}
+  and one of $n, m$ is odd and the other even.  Either can be $0$.
 \end{itemize}
 \end{proof-rule}
 
@@ -1014,8 +1024,13 @@ The possible transformations are:
     \lor \dots \lor \varphi_{n'} $ where the right hand side has all
     repeated literals removed.
     \item $\varphi_1 \lor\dots\lor \top\lor\dots \lor \varphi_n \leftrightarrow \top$
-    \item $\varphi_1 \lor\dots\lor \varphi_i\lor \dots \lor \varphi_j\lor\dots \lor \varphi_n \leftrightarrow \top$ if
-    	$\varphi_i = \bar{\varphi_j}$
+    \item $\varphi_1 \lor\dots\lor \varphi_i\lor \dots \lor \varphi_j\lor\dots \lor \varphi_n \leftrightarrow \top$
+  and $\varphi_i$, $\varphi_j$ are such that
+  \begin{align*}
+  \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
+  \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
+  \end{align*}
+  and one of $n, m$ is odd and the other even.  Either can be $0$.
 \end{itemize}
 \end{proof-rule}