diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 18c00adba992e35dad80893acdb5d306488ae935..33a7f4c80a8462edeb1e79a30259240b06d6a6ff 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -500,7 +500,7 @@ f(t_1, \dots, t_n) \simeq f(u_1, \dots, u_n)
 \begin{plList}
 \proofsep& i.&
 \neg (t_1 \simeq u_1) , \dots , \neg (t_n \simeq u_n) ,
-P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n)
+\neg (P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n))
 &(\currule)\\
 \end{plList}
 \end{plContainer}