diff --git a/spec/changelog.tex b/spec/changelog.tex
index 807045a2654d1f662ade02ad9f5a1b7defca0dc1..65f5a4246502de886804b5ccbc8195134876e7a9 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -11,6 +11,8 @@ Proof rules:
   of equality explicitly but as an equivalence. Note that in principle this
   could be done with the rule \proofRule{symm} above, but would require a long
   and tedious use of \proofRule{subproof} for each direction of the equivalence.
+  \item Addition of the rule \proofRule{or_intro} to express weakening of a
+        clause.
 \end{itemize}
 
 \noindent
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 508cfa0dfeb0c7aea8337d612c0c135415e7c391..645b87dca9ef2637b7d9b9b00545a38f871d99ae 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -263,6 +263,7 @@ simplifications.}
 \label{rule-tab:cvc5}\\
   Rule & Description \\
   \hline
+\ruleref{or_intro} & Weakening of a clause. \\
 \ruleref{eq_symmetric} & Symmetry of equality as equivalence. \\
 \end{xltabular}
 \subsection{Rule List}
@@ -844,6 +845,15 @@ An application of the \proofRule{or} rule.
 \end{AletheVerb}
 \end{RuleExample}
 
+\begin{RuleDescription}{or_intro}
+\begin{AletheX}
+$i$. & \ctxsep &
+$\varphi_1, \cdots, \varphi_n$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1, \cdots, \varphi_n, \psi_1, \dots, \psi_m$ & (\currule\;$i$) \\
+\end{AletheX}
+where $m \geq 1$.
+\end{RuleDescription}
+
 \begin{RuleDescription}{not_and}
 \begin{AletheX}
 $i$. & \ctxsep & $\neg (\varphi_1 \land \dots \land \varphi_n)$ & ($\dots$) \\