Add some bitvector rules

This moves #31 forward!

spec/changelog.tex

 \subsection*{Unreleased}
 
+Proof rules:
+\begin{itemize}
+  \item Addition of a section describing bitvector proofs.
+  \item Bitblasting rules: \proofRule{bitblast_extract},  \proofRule{bitblast_add},
+      \proofRule{bitblast_ult}.
+\end{itemize}
+
+\noindent
 Breaking changes:
 \begin{itemize}
   \item Allow arbitrary extra annotations in \texttt{assume} commands.