diff --git a/spec/changelog.tex b/spec/changelog.tex
index e2e3410e98459ff17fa943cffce008f907bc9655..39049184b4a1a6239b7eefff773a6331ce1b3312 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -22,7 +22,11 @@ Breaking changes:
         be \texttt{(x S) (:= (y S) x)}.
   \item The arguments for \proofRule{forall_inst} have been changed to
         no longer take the shape of bindings using \texttt{(:= x c)}.
-        Instead, the list of instatiation terms must follow the variable order and cover all the respective bound variables.
+        Instead, the list of instatiation terms must follow the variable
+        order and cover all the respective bound variables.
+  \item The rules \proofRule{and_pos}, \proofRule{or_neg}, \proofRule{and},
+        \proofRule{not_or} now have one argument that indicates which subterm
+        they use.
 \end{itemize}
 
 \noindent
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 4b8955036f2e147dfc442934265f466846db994b..44c309949e9638b1f5b7abae28816b04f69cf486 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -810,7 +810,7 @@ done during clausification.
 \begin{RuleDescription}{and}
 \begin{AletheX}
 $i$. & \ctxsep & $\varphi_1 \land \cdots \land \varphi_n$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_k$ & (\currule\;$i$) \\
+$j$. & \ctxsep & $\varphi_k$ & (\currule\;$i$)\, k\\
 \end{AletheX}
 and $1 \leq k \leq n$.
 \end{RuleDescription}
@@ -818,7 +818,7 @@ and $1 \leq k \leq n$.
 \begin{RuleDescription}{not_or}
 \begin{AletheX}
 $i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg \varphi_k$  & (\currule\;$i$) \\
+$j$. & \ctxsep & $\neg \varphi_k$  & (\currule\;$i$)\, k\\
 \end{AletheX}
 and $1 \leq k \leq n$.
 \end{RuleDescription}
@@ -931,7 +931,8 @@ $j$. & \ctxsep & $\neg\varphi_1, \neg\varphi_2$ & (\currule\;$i$) \\
 
 \begin{RuleDescription}{and_pos}
 \begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 \land \cdots \land \varphi_n) , \varphi_k$ & \currule \\
+$i$. & \ctxsep & $\neg (\varphi_1 \land \cdots \land \varphi_n) , \varphi_k$ &
+  \currule\, k\\
 \end{AletheX}
 with $1 \leq k \leq n$.
 \end{RuleDescription}
@@ -950,7 +951,8 @@ $i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n) , \varphi_1 , \dot
 
 \begin{RuleDescription}{or_neg}
 \begin{AletheX}
-$i$. & \ctxsep & $(\varphi_1 \lor \cdots \lor \varphi_n), \neg \varphi_k$ & \currule \\
+$i$. & \ctxsep & $(\varphi_1 \lor \cdots \lor \varphi_n), \neg \varphi_k$ &
+  \currule\, k\\
 \end{AletheX}
 with $1 \leq k \leq n$.
 \end{RuleDescription}