Merge branch 'add/or_intro' into 'master'

Add weakening rule

See merge request !11

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{weakening} to express weakening of a
+        clause.
 \end{itemize}
 
 \noindent

spec/rule_list.tex

@@ -263,6 +263,7 @@ simplifications.}
 \label{rule-tab:cvc5}\\
   Rule & Description \\
   \hline
+\ruleref{weakening} & 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}{weakening}
+\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$) \\