diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 257f36ac3c122d70404b50bb39f03804ee07e453..4b8955036f2e147dfc442934265f466846db994b 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -101,6 +101,7 @@ to quickly find the definition of rules.
 \ruleref{distinct_elim} & Elimination of the $\lsymb{distinct}$ operator. \\
 \ruleref{la_rw_eq} & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \\
 \ruleref{nary_elim} & Eliminate $n$-ary application of operators via binary applications. \\
+\ruleref{eq_symmetric} & Symmetry of equality as equivalence. \\
 \end{xltabular}
 
 \begin{xltabular}{\linewidth}{l X}
@@ -256,6 +257,14 @@ simplifications.}
 \ruleref{symm}     & Symmetry of equality. \\
 \ruleref{not_symm} & Symmetry of not-equal.\\
 \end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Rules used by the Carcara elaborator.}
+\label{rule-tab:cvc5}\\
+  Rule & Description \\
+  \hline
+\ruleref{eq_symmetric} & Symmetry of equality as equivalence. \\
+\end{xltabular}
 \subsection{Rule List}
 \label{sec:alethe:rules-list}