diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2610e565f393fdefb7f55e4b91ba5face96a0b6b..56f605cbabd0e395381e8a71d46a2ada022ff481 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,4 +1,4 @@
-image: dockershelf/latex:full
+image: kjarosh/latex:2023.1
 
 stages:
   - build
@@ -6,6 +6,8 @@ stages:
 
 build:
     stage: build
+    before_script:
+    - apk add py3-pygments
     script:
     - cd spec
     - lualatex -shell-escape -recorder '\def\nocomments{}\input{doc.tex}'
diff --git a/spec/changelog.tex b/spec/changelog.tex
index a058885e76b3e0ac9ee087d7bf12470b9a681e55..e2e3410e98459ff17fa943cffce008f907bc9655 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -1,3 +1,44 @@
+\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}.
+  \item Addition of rules \proofRule{la_mult_pos} and \proofRule{la_mult_neg} to describe multiplication with a positive or negative factor.
+  \item Addition of rules \proofRule{symm} and \proofRule{not_symm} to express symmetry of equality explicitly.
+  \item Addition of the rule \proofRule{eq_symmetric} to express symmetry
+  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.
+\end{itemize}
+
+\noindent
+Breaking changes:
+\begin{itemize}
+  \item Allow arbitrary extra annotations in \texttt{assume} commands.
+  \item Add the sort to all variables in contexts.  Before, the context
+        of a bind could be \texttt{(x S) (:= y x)}.  Now it must
+        be \texttt{(x S) (:= (y S) x)}.
+  \item The arguments for \proofRule{forall_inst} have been changed to
+        no longer take the shape of bindings using \texttt{(:= x c)}.
+        Instead, the list of instatiation terms must follow the variable order and cover all the respective bound variables.
+\end{itemize}
+
+\noindent
+Clarifications and corrected errors:
+\begin{itemize}
+  \item Clarify that the \texttt{:args} annotation in \texttt{anchor} can be
+        omitted if the list is empty.
+  \item Clarify that \proofRule{bind} can work on existential and universal
+        quantifiers.
+  \item Fix mistake in proof grammar.  It now uses the \texttt{context\_annotation}
+        non-terminal in the rule for the \texttt{anchor} command.
+  \item Fix the example of \proofRule{onepoint}.
+  \item Add the missing context to the conclusion of \proofRule{bind},
+        \proofRule{sko_ex}, \proofRule{sko_forall}, \proofRule{onepoint}.
+\end{itemize}
+
 \subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
 
 This release overhauls the entire document, but introduces only few
@@ -10,9 +51,9 @@ command.
 Beyond many smaller clarifications and typographic improvements, the
 following changes are implemented in this release.
 \begin{itemize}
-	\item Add an abstract proof checking procedure to clarify
-	the semantics of the proof format.
-	\item Add a description of the semantics of contexts based on λ-terms.
+  \item Add an abstract proof checking procedure to clarify
+  the semantics of the proof format.
+  \item Add a description of the semantics of contexts based on λ-terms.
   \item List all transformations that are implicit in Alethe proofs.
   \item Change the notation used for terms from first-order style
    (e.g., $f(x,g(y))$) to higher-order style (e.g.,
diff --git a/spec/doc.tex b/spec/doc.tex
index 6acc942785c9f245d9481d1662ff44e3e2046a4a..b826c03ec0e80ed1d4d61f8b2758b0e92ae234e3 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -36,7 +36,7 @@
 \indexsetup{level=\indexsection,firstpagestyle=headings,noclearpage}
 
 % Must come after imakeidx
-\usepackage[hidelinks=true]{hyperref}
+\usepackage[hidelinks,hypertexnames=false]{hyperref}
 \usepackage{breakurl}
 
 \usepackage{tikz}
@@ -73,6 +73,7 @@
 \newcommand\lsymb[1]{\mathbf{#1}}
 \DeclareMathOperator*{\subst}{subst}
 \DeclareMathOperator*{\reify}{reify}
+\DeclareMathOperator*{\bvexplode}{bvexplode}
 \newcommand\groundbox[1]{\boxed{#1}}
 
 % Proofs
@@ -663,7 +664,7 @@ An Alethe proof is a list of commands.
 (assume h1 (not (p a)))
 (assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
 ...
-(anchor :step t9 :args ((:= z2 vr4)))
+(anchor :step t9 :args ((vr4 U) (:= (z2 U) vr4)))
 (step t9.t1 (cl (= z2 vr4)) :rule refl)
 (step t9.t2 (cl (= (p z2) (p vr4)))
          :rule cong :premises (t9.t1))
@@ -691,25 +692,25 @@ An Alethe proof is a list of commands.
 \[
   \begin{array}{r c l}
  \grNT{proof}           &\grRule & \grNT{proof\_command}^{*} \\
- \grNT{proof\_command}  &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
+ \grNT{proof\_command}  &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
                         &\grOr   & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause}
                                         \; \textAlethe{:rule}\; \grNT{symbol} \\
                         &        & \quad \grNT{premises\_annotation}^{?} \\
-                        &        & \quad \grNT{context\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
+                        &        & \quad \grNT{args\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
                         & \grOr  & \textAlethe{(anchor :step}\; \grNT{symbol}\;
                                             \\
-                        &        & \quad \grNT{args\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
+                        &        & \quad \grNT{context\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
                         & \grOr  & \textAlethe{(define-fun}\; \grNT{function\_def}\,\textAlethe{)} \\
  \grNT{clause}          &\grRule & \textAlethe{(cl}\; \grNT{proof\_term}^{*}\,\textAlethe{)} \\
  \grNT{proof\_term}     &\grRule & \grNT{term}\text{ extended with } \\
                         &        & \textAlethe{(choice (}\, \grNT{sorted\_var}\,\textAlethe{)}\; \grNT{proof\_term}\,\textAlethe{)}  \\
  \grNT{premises\_annotation} &\grRule & \textAlethe{:premises (}\; \grNT{symbol}^{+}\textAlethe{)} \\
  \grNT{args\_annotation}     &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{step\_arg}^{+}\,\textAlethe{)}  \\
- \grNT{step\_arg}            &\grRule & \grNT{symbol} \grOr
+ \grNT{step\_arg}            &\grRule & \grNT{symbol}\;\grOr\;
                                           \textAlethe{(}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
  \grNT{context\_annotation}  &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{context\_assignment}^{+}\,\textAlethe{)}  \\
- \grNT{context\_assignment}  &\grRule & \textAlethe{(}    \,\grNT{sorted\_var}\,\textAlethe{)}  \\
-                             & \grOr  & \textAlethe{(:=}\, \grNT{symbol}\;\grNT{proof\_term}\,\textAlethe{)} \\
+ \grNT{context\_assignment}  &\grRule & \grNT{sorted\_var} \\
+                             & \grOr  & \textAlethe{(:=}\, \grNT{sorted\_var}\;\grNT{proof\_term}\,\textAlethe{)} \\
   \end{array}
   \]
   \caption{The proof grammar.}
@@ -807,9 +808,12 @@ A subproof is concluded by a matching \inlineAlethe{step} command.  This step mu
 a \index{rule!concluding}{\em concluding rule}
 (such as \proofRule{subproof}, \proofRule{bind}, and so forth).
 
-After the \inlineAlethe{anchor} command, the proof uses \inlineAlethe{assume} commands to list
-the assumptions of the subproof.  Subsequently, the subproof is a list of
-\inlineAlethe{step} commands that can use prior steps in the subproofs as premises.
+After the \inlineAlethe{anchor} command, the proof uses
+\inlineAlethe{assume} commands to list the assumptions of the subproof.
+Subsequently, the subproof is a list of \inlineAlethe{step} commands
+that can use prior steps in the subproofs as premises.  It is not allowed
+to issue \inlineAlethe{assume} commands after the first \inlineAlethe{step}
+command of a subproof has been issued.
 
 In the abstract notation, every step is associated with a context.  The
 concrete syntax uses anchors to optimize this.
@@ -820,9 +824,14 @@ pushes precisely $c_1,\dots, c_n$ onto the context.
 Since contexts can only be manipulated by push and pop, context manipulations
 are nested.  The \inlineAlethe{anchor} commands push onto the context and the
 corresponding \inlineAlethe{step} commands pop from the context.
+%
 To indicate these changes to the context, every anchor is associated with a list
-of fixed variables and mappings.
-This list can be empty.
+of fixed variables and mappings.  The list is provided by the \inlineAlethe{:args}
+annotation.  If the list is empty, the \inlineAlethe{:args} annotation is
+omitted\footnote{The only rule that allows an empty list is the
+\proofRule{subproof} rule.  Since this rule corresponds to implication introduction,
+it does not interact with binders.}.
+%
 Note that, when an \inlineAlethe{anchor} command extends a context $\Gamma$ with
 some mappings $x_1 \mapsto t_1, \dots,  x_n \mapsto t_n$,
 then the terms $t_i$ are normalized by applying
@@ -858,12 +867,12 @@ expressed as a concrete proof.
 \begin{AletheVerb}
 (assume h1 (forall ((x S)) (P x)))
 (assume h2 (not (forall ((y S)) (P y))))
-(anchor :step t5 :args ((:= x y)))
+(anchor :step t5 :args ((y S) (:= (x S) y)))
 (step t3 (cl (= x y)) :rule refl)
 (step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
 (step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
                               :rule bind)
-(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
+(step t6 (cl (not (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
              (not (forall ((x S)) (P x)))
              (forall ((y S)) (P y))) :rule equiv_pos2)
 (step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
@@ -1030,7 +1039,7 @@ the calculation of the context of the steps in the subproof.
 The proof in Example~\ref{ex:ti:ctx-concrete} has only one subproof
 and this subproof is also a first-innermost subproof.  It is the subproof
 \begin{AletheVerb}
-(anchor :step t5 :args ((:= x y)))
+(anchor :step t5 :args ((y S) (:= (x S) y)))
 (step t3 (cl (= x y)) :rule refl)
 (step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
 (step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
@@ -1683,6 +1692,88 @@ is functional congruence, and \proofRule{sko_forall} works like
 \end{AletheS}
 \end{example}
 
+\subsection{Bitvector Reasoning with Bitblasting}
+
+A standard approach to handle bitvector reasoning in SMT solvers
+is bitblasting.  Bitblasting\index{bitblasting} works by translating
+bitvector\index{bitvector} functions to propositional formulas that
+model the logical circuit of the bitvector function.
+
+To express bitblasting in Alethe proof rules, the the Alethe calculus uses
+multiple families of helper functions: $\lsymb{bbT}$, $\lsymb{bitOf}_m$,
+$\lsymb{bvsize}$, and $\lsymb{bv}_n^i$.  Functions in the families are
+distinguished either by overloading ($\lsymb{bbT}$ and $\lsymb{bvsize}$)
+or by explicit indexing ($\lsymb{bitOf}_m$ and $\lsymb{bv}_n^i$).
+To avoid name clashes with user defined
+functions, $\lsymb{bbT}$ is written as \inlineAlethe{@bbT}, $\lsymb{bitOf}$
+as \inlineAlethe{@bitOf}, $\lsymb{bvsize}$ as \inlineAlethe{@bvsize}, and
+$\lsymb{bv}$ as \inlineAlethe{@bv}.  The SMT-LIB standard specifies
+that simple symbols starting with ``\inlineAlethe{@}'' are reserved for
+solver generated functions.
+
+The family $\lsymb{bbT}$ consists of one function for each bitvector sort
+$(\lsymb{BitVec}\;n)$.
+\[
+\lsymb{bbT}\,:\,\underbrace{\lsymb{Bool}\,\dots\,\lsymb{Bool}}_n\;(\lsymb{BitVec}\;n).
+\]
+
+\noindent
+Intuitively, the function $\lsymb{bbT}$ takes a list of boolean arguments and
+packs them into a bitvector.
+Let $\langle u_1, \dots, u_n\rangle$ denote a bitvector of sort $(\lsymb{BitVec}\;n)$
+where $u_i = \top$ if the bit at position $i$ is $1$, and $u_i = \bot$ otherwise.
+The bit $u_n$ is the least significant bit.  Then
+
+\[
+\lsymb{bbT}\; v_1 \dots v_n = \langle v_1, \dots, v_n\rangle .
+\]
+
+\noindent
+The $\lsymb{bbT}$ functions could be defined in terms of standard SMT-LIB functions.
+\begin{align*}
+\lsymb{bbT}\;v_1 \dots v_n :=\;
+ &\lsymb{concat}\,(\lsymb{concat}\,(\dots \\
+ &(\lsymb{concat}\,(\lsymb{ite}\,v_1\,\langle\top\rangle\,\langle\bot\rangle)\,(\lsymb{ite}\,v_2\,\langle\top\rangle\,\langle\bot\rangle))\\
+ & \dots \\
+ & (\lsymb{ite}\,v_{n-1}\,\langle\top\rangle\,\langle\bot\rangle)) \\
+ & (\lsymb{ite}\,v_n\,\langle\top\rangle\,\langle\bot\rangle)) \\
+\end{align*}
+
+\noindent
+The functions $\lsymb{bitOf}_m$ are the inverse of $\lsymb{bbT}$.  They extract
+a bit of a bitvector as a boolean.  Just as the built in $\lsymb{extract}$
+symbol, $\lsymb{bitOf}_m$ is used as an indexed symbol.  Hence, for $m \leq n$, we
+write \inlineAlethe{(_ @bitOf} $m$ \inlineAlethe{)}, to denote functions
+\[
+\lsymb{bitOf}_m : (\lsymb{BitVec}\;n) \to \lsymb{Bool}.
+\]
+These functions are defined as 
+\[
+\lsymb{bitOf}_m \langle u_1, \dots, u_n \rangle := u_m.
+\]
+
+
+\noindent
+The functions $\lsymb{bvsize}$ return the size of a bitvector.  Formally, there
+is one $\lsymb{bvsize}$ for for each bitvector sort $(\lsymb{BitVec}\;n)$.  Each
+$\lsymb{bvsize}$ is a constant function that returns $n$.  Using notation:
+
+\begin{align*}
+\lsymb{bvsize}& : (\lsymb{BitVec}\;n) \to \mathbb{N}\\
+\lsymb{bvsize}&\;b := n
+\end{align*}
+
+\noindent
+Finally, $\lsymb{bv}_n^i$ is a family of constants indexed by two parameters:
+a bitvector length $n$, and a natural number $i$.  We
+write \inlineAlethe{(_ @bv}$n$ $i$ \inlineAlethe{)} for $\lsymb{bv}_n^i$.
+The space before $n$ is omitted for historical reasons.
+Each $\lsymb{bv}_n^i$ is the bitvector constant that represents the bitvector
+of length $n$ that encodes the integer $i$.  Formally, it corresponds
+to \inlineAlethe{nat2bv[n](i)}, where \inlineAlethe{nat2bv} is defined
+as in the SMT-LIB
+standard.\footnote{See \url{https://smt-lib.github.io/theories-FixedSizeBitVectors.shtml}.}
+
 \section{The Alethe Rules}
 \label{apx:rules}
 \input{rule_list}
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 30b40984d5784c488dbd7fb69ed0582330517174..4e760cf1b3867fcbd23412151181298090c50270 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -51,6 +51,8 @@ to quickly find the definition of rules.
 \ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
 \ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
 \ruleref{la_tautology} & A trivial linear tautology. \\
+\ruleref{la_mult_pos} & Multiplication with a positive factor. \\
+\ruleref{la_mult_neg} & Multiplication with a negative factor.\\
 \ruleref{forall_inst} & Quantifier instantiation. \\
 \ruleref{refl} & Reflexivity after applying the context. \\
 \ruleref{eq_reflexive} & $t ≈ t$ without context. \\
@@ -99,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}
@@ -111,6 +114,8 @@ to quickly find the definition of rules.
 \ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
 \ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
 \ruleref{la_tautology} & A trivial linear tautology. \\
+\ruleref{la_mult_pos} & Multiplication with a positive factor. \\
+\ruleref{la_mult_neg} & Multiplication with a negative factor.\\
 \ruleref{la_rw_eq} & $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \\
 \ruleref{div_simplify} & Simplification of division. \\
 \ruleref{prod_simplify} & Simplification of products. \\
@@ -229,6 +234,37 @@ simplifications.}
 \ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
 \end{xltabular}
 
+\begin{xltabular}{\linewidth}{l X}
+\caption{Bitvector rules.}
+\label{rule-tab:bitblasting}\\
+  Rule & Description \\
+  \hline
+\ruleref{bitblast_extract} & Bitblasting of $\lsymb{extract}$. \\
+\ruleref{bitblast_ult} & Bitblasting of $\lsymb{ult}$. \\
+\ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\
+\end{xltabular}
+
+\begin{xltabular}{\linewidth}{l X}
+\caption{Rules used by cvc5, but not by veriT.}
+\label{rule-tab:cvc5}\\
+  Rule & Description \\
+  \hline
+\ruleref{bitblast_extract} & Bitblasting of $\lsymb{extract}$. \\
+\ruleref{bitblast_ult} & Bitblasting of $\lsymb{ult}$. \\
+\ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\
+\ruleref{la_mult_pos} & Multiplication with a positive factor. \\
+\ruleref{la_mult_neg} & Multiplication with a negative factor.\\
+\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}
 
@@ -518,7 +554,7 @@ $\varphi_1 \lor \varphi_2$ % Checked: this is a proper disjunction not a cl
  & (\currule) \\
 \end{AletheX}
 
-It can be checked by using the procedure for \proofRule{la_generic} with
+It can be checked by using the procedure for \proofRule{la_generic}
 while setting the arguments to $1$. Informally, the rule follows one of several
 cases:
 \begin{itemize}
@@ -528,10 +564,67 @@ cases:
     \item $s_1 \geq d_1 \lor \neg (s_1 \geq d_2)$ where $d_1 = d_2$
     \item $\neg (s_1 \leq d_1) \lor \neg(s_1 \geq d_2)$ where $d_1 < d_2$
 \end{itemize}
-The inequalities $s_1 \bowtie d$ are are the result of applying normalization
+The inequalities $s_1 \bowtie d$ are the result of applying normalization
 as for the rule \proofRule{la_generic}.
 \end{RuleDescription}
 
+\begin{RuleDescription}{la_mult_pos}
+
+Either of the form:
+
+  \begin{AletheX}
+    $i$. & \ctxsep  &
+     $(t_1 > 0 \wedge t_2 \bowtie t_3) \to t_1 * t_2 \bowtie t_1 * t_3$
+    & (\currule) \\
+  \end{AletheX}
+
+with $\bowtie \in \{<,>, \le,\ge, ≈\}$.\\
+
+\noindent Or of the form:
+
+\begin{AletheX}
+  $i$. & \ctxsep  &
+  $(t_1 > 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$
+  & (\currule) \\
+\end{AletheX}
+
+\end{RuleDescription}
+
+\begin{RuleDescription}{la_mult_neg}
+
+Either of the form:
+
+  \begin{AletheX}
+    $i$. & \ctxsep  &
+    $(t_1 < 0 \land t_2 \bowtie t_3) \rightarrow t_1 * t_2 \bowtie_{inv} t_1 * t_3$
+    & (\currule) \\
+  \end{AletheX}
+
+  with $\bowtie \in \{<,>, \le,\ge, ≈\}$ and $\bowtie_{inv}$ being defined according to the following table.
+
+  \begin{center}
+  \begin{tabular}{|c | c|}
+  \hline
+  $\bowtie$ & $\bowtie_{inv}$ is defined as: \\
+  \hline
+  $ < $ & $ > $ \\
+  $ \le $ & $ \ge $ \\
+  $ ≈ $ & $ ≈ $ \\
+  $ > $ & $ < $ \\
+  $ \ge $ & $ \le $ \\
+  \hline
+  \end{tabular}
+  \end{center}
+
+\noindent Or of the form:
+
+  \begin{AletheX}
+    $i$. & \ctxsep  &
+    $(t_1 < 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$
+    & (\currule) \\
+  \end{AletheX}
+\end{RuleDescription}
+
 \begin{RuleDescription}{bind}
   The \currule{} rule is used to rename bound variables.
 
@@ -540,12 +633,15 @@ as for the rule \proofRule{la_generic}.
 $j$. & \spctx{ $\Gamma, y_1,\dots, y_n,  x_1 \mapsto y_1, \dots ,  x_n \mapsto y_n$}
    & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
    \spsep
-$k$. & & \ctxsep &
-    $\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
+$k$. & $\Gamma$ & \ctxsep &
+    $Q x_1, \dots, x_n.\varphi ≈ Q y_1, \dots, y_n. \varphi'$
      & \currule{} \\
 \end{AletheXS}
-  where the variables $y_1, \dots, y_n$ are neither free in $\forall x_1,
-  \dots, x_n.\varphi$ nor occur in $\Gamma$.
+
+\noindent
+where $Q \in \{\forall, \exists\}$,
+and the variables $y_1, \dots, y_n$ are neither free in $Q x_1,
+\dots, x_n.\varphi$ nor occur in $\Gamma$.
 \end{RuleDescription}
 
 \begin{RuleDescription}{sko_ex}
@@ -557,8 +653,10 @@ $j$. &
 \spctx{$\Gamma, x_1 \mapsto \varepsilon_1, \dots ,  x_n \mapsto \varepsilon_n$}
    & \ctxsep &  $\varphi ≈ \psi$ & ($\dots$) \\
    \spsep
-$k$. & & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
+$k$. & $\Gamma$ & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
 \end{AletheXS}
+
+\noindent
 where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
 x_n. \varphi)$.
 \end{RuleDescription}
@@ -572,7 +670,7 @@ $j$. &
 \spctx{$\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots,  x_n \mapsto (\varepsilon x_n.\neg\varphi)$}
    & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
  \spsep
-$k$. & & \ctxsep  & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
+$k$. & $\Gamma$ & \ctxsep  & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
 \end{AletheXS}
 
 \end{RuleDescription}
@@ -581,18 +679,29 @@ $k$. & & \ctxsep  & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
 \begin{AletheX}
 $i$. & \ctxsep &
 $\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]$
- & \currule\, [$(x_{k_1}, t_{k_1})$, $\dots$, $(x_{k_n}, t_{k_n})$] \\
+ & \currule\, [$t_1$, $\dots$, $t_n$] \\
 \end{AletheX}
-where $k_1, \dots, k_n$ is a permutation of $1, \dots, n$ and $x_i$ and
-$k_i$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
-\inlineAlethe{(:= xki tki)}.
+
+\noindent
+where $x_i$ and $t_i$ have the same sort.
 \end{RuleDescription}
 
+\begin{RuleExample}
+An application of the \proofRule{forall_inst} rule.
+\begin{AletheVerb}
+(step t16 (cl (or (not (forall ((x S) (y T)) (P y x    )))
+                                             (P b (f a))
+      :rule forall_inst :args ((f a) b)
+\end{AletheVerb}
+\end{RuleExample}
+
 
 \begin{RuleDescription}{refl}
 \begin{AletheXS}
 $j$. & \ctxsep  & $\Gamma$  & $t_1 ≈ t_2 $ & \currule \\
 \end{AletheXS}
+
+\noindent
 where, if $\sigma = \subst(\Gamma)$,
 the terms $t_1\sigma$ and $t_2$ are
 syntactically equal up to  renaming of
@@ -1196,7 +1305,7 @@ variables that can only have one value.
 $j$. & \spctx{$\Gamma, x_{k_1},\dots, x_{k_m},  x_{j_1} \mapsto t_{j_1}, \dots ,  x_{j_o} \mapsto t_{j_o}$}
    & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
  \spsep
-$k$. & & \ctxsep  & $Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$ & \currule{} \\
+$k$. & $\Gamma$ & \ctxsep  & $Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$ & \currule{} \\
 \end{AletheXS}
 where $Q\in\{\forall, \exists\}$,  $n = m + o$,  $k_1, \dots, k_m$ and
 $j_1, \dots, j_o$ are monotone
@@ -1217,7 +1326,7 @@ An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x
 \rightarrow (f\,x)\land (f\,y))$ look like this:
 
 \begin{AletheVerb}
-(anchor :step t3 :args ((:= y x)))
+(anchor :step t3 :args ((x S) (:= (y S) x)))
 (step t3.t1 (cl (= x y)) :rule refl)
 (step t3.t2 (cl (= (= x y) (= x x)))
     :rule cong :premises (t3.t1))
@@ -1232,7 +1341,7 @@ An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x
 (step t3 (cl (=
         (forall ((x S) (y S)) (=> (= x y) (and (f x) (f y))))
         (forall ((x S))       (=> (= x x) (and (f x) (f x))))))
-    :rule qnt_simplify)
+    :rule onepoint)
 \end{AletheVerb}
 \end{RuleExample}
 
@@ -1532,58 +1641,58 @@ form and the reordering of equalities.
 
 \begin{RuleDescription}{bitblast_extract}
 \begin{AletheX}
-$i$. & \ctxsep & $((\_\ \mathrm{extract}\ j\ i)\ x) \simeq (\mathrm{bbterm}\ x[i]\ \ldots\ x[j])$ & (\currule) \\
+$i$. & \ctxsep & $((\lsymb{extract}\ j\ i)\ x) ≈ (\lsymb{bbT}\ \varphi_i\ \ldots\ \varphi_j)$ & (\currule) \\
 \end{AletheX}
 
-Each term $x[i]$ corresponds to whether the $i$-th bit of $x$ is true or not, which
-will be represented via an application of the operator ``bit\_of'', i.e.,
-$((\_\ bit\_of\ i)\ x)$, which has a Boolean return type.
-%
-The ``bbterm'' operator takes $n$ Booleans and yields a bit-vector of size $n$
-where the least significant bit is 1 if the first argument 1 is true, 0
-otherwise, and so on.
-%
+\noindent
+where the formulas $\varphi_k$ are $(\lsymb{bitOf}_k\ x)$ for $i \leq k \leq j$.
+
 Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
-above when $x$ is a ``bbterm'' application:
+above when $x$ is a $\lsymb{bbT}$ application:
 
 \medskip
 \begin{AletheX}
-$i$. & \ctxsep & $((\_\ \mathrm{extract}\ j\ i)\ (\mathrm{bbterm}\ x_0\ \ldots\
-x_i\ \ldots \ x_j\ \ldots\ x_n)) \simeq (\mathrm{bbterm}\ x_i\ \ldots\ x_j)$ & (\currule) \\
+$i$. & \ctxsep & $((\lsymb{extract}\ j\ i)\ (\lsymb{bbT}\ x_0\ \ldots\
+x_i\ \ldots \ x_j\ \ldots\ x_n)) ≈ (\lsymb{bbT}\ x_i\ \ldots\ x_j)$ & (\currule) \\
 \end{AletheX}
 
+\noindent
 This alternative is based on the validity of the equality
-$$(\mathrm{bbterm}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)[i]\simeq x_i$$
-for any bit-vector $x$ of size $n+1$, where $0\leq i\leq n$.
+\[
+\lsymb{bitOf}_k\ (\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n) ≈ x_k
+\]
+for any bit-vector $x$ of size $n+1$, where $0\leq k\leq n$.
 
 \end{RuleDescription}
 
 \begin{RuleDescription}{bitblast_ult}
 \begin{AletheX}
-$i$. & \ctxsep & $(\mathrm{bvult}\ x\ y) \simeq res_{n-1}$ & (\currule) \\
+$i$. & \ctxsep & $(\lsymb{bvult}\ x\ y) ≈ \mathrm{res}_{n-1}$ & (\currule) \\
 \end{AletheX}
-in which both $x$ and $y$ must have the same type $(\_\ \mathrm{BitVec}\ n)$ and, for
-$i\geq 0$:
+in which both $x$ and $y$ must have the same type $(\lsymb{BitVec}\ n)$ and, for
+$i\geq 0$
 \[
   \begin{array}{lcl}
-    \mathrm{res}_0&=&\neg x[0] \wedge y[0]\\
-    \mathrm{res}_{i+1}&=&((x[i+1]\simeq y[i+1])\wedge
-                          \mathrm{res}_i)\vee (\neg x[i+1]\wedge y[i+1])
+    \mathrm{res}_0&=&\neg (\lsymb{bitOf}_0\ x) \wedge (\lsymb{bitOf}_0\ y)\\
+    \mathrm{res}_{i+1}&=&(((\lsymb{bitOf}_{i+1}\ x) ≈ (\lsymb{bitOf}_{i+1}\ y))\wedge \mathrm{res}_i)\vee
+                       (\neg (\lsymb{bitOf}_{i+1}\ x) \wedge (\lsymb{bitOf}_{i+1}\ y))
   \end{array}
 \]
+
+\noindent
 Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
-above when $x$ and $y$ are ``bbterm'' applications. So given that
+above when $x$ and $y$ are ``$\lsymb{bbT}$'' applications. So given that
 \[
   \begin{array}{lcl}
-    x&=&(\mathrm{bbterm}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
-    y&=&(\mathrm{bbterm}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
+    x&=&(\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
+    y&=&(\lsymb{bbT}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
   \end{array}
 \]
-then ``res'' can be defined, for $i \geq 0$, as 
+then ``$\mathrm{res}$'' can be defined, for $i \geq 0$, as
 \[
   \begin{array}{lcl}
     \mathrm{res}_0&=&\neg x_0 \wedge y_0\\
-    \mathrm{res}_{i+1}&=&((x_{i+1}\simeq y_{i+1})\wedge
+    \mathrm{res}_{i+1}&=&((x_{i+1} ≈ y_{i+1})\wedge
                           \mathrm{res}_i)\vee (\neg x_{i+1}\wedge y_{i+1})
   \end{array}
 \]
@@ -1592,42 +1701,99 @@ then ``res'' can be defined, for $i \geq 0$, as
 
 \begin{RuleDescription}{bitblast_add}
 \begin{AletheX}
-$i$. & \ctxsep & $(\mathrm{bvadd}\ x\ y) \simeq (\mathrm{bbterm}\ (x[0] \oplus y[0])\oplus\mathrm{carry}_0\ \ldots\ (x[n-1]
-        \oplus y[n-1])\oplus\mathrm{carry}_{n-1})$ & (\currule) \\
+$i$. & \ctxsep & $(\lsymb{bvadd}\ x\ y) ≈ A_1$ & (\currule) \\
 \end{AletheX}
-in which both $x$ and $y$ must have the same type $(\_\ \mathrm{BitVec}\ n)$ and, for
-$i\geq 0$:
-    \[
-      \begin{array}{lcl}
-        \mathrm{carry}_0&=&\bot\\
-        \mathrm{carry}_{i+1}&=&(x[i]\wedge y[i])\vee((x[i]\oplus y[i])\wedge \mathrm{carry}_i)
-      \end{array}
-    \]
+in which both $x$ and $y$ must have the same type $(\lsymb{BitVec}\ n)$.
+The term ``$A_1$'' is
+\begin{align*}
+(\lsymb{bbT}\;& (((\lsymb{bitOf}_{0}\ x) \,\lsymb{xor}\,(\lsymb{bitOf}_{0}\ y))\,\lsymb{xor}\,\mathrm{carry}_0) \\
+              & (((\lsymb{bitOf}_{1}\ x) \,\lsymb{xor}\,(\lsymb{bitOf}_{1}\ y))\,\lsymb{xor}\,\mathrm{carry}_1) \\
+              & \ldots \\
+              & (((\lsymb{bitOf}_{n-1}\ x) \,\lsymb{xor}\, (\lsymb{bitOf}_{n-1}\ y))\,\lsymb{xor}\,\mathrm{carry}_{n-1}))
+\end{align*}
+and for $i\geq 0$
+\[
+  \begin{array}{lcl}
+    \mathrm{carry}_0&=&\bot\\
+    \mathrm{carry}_{i+1}&=&((\lsymb{bitOf}_{i}\ x) \wedge (\lsymb{bitOf}_{i}\ y))\vee(((\lsymb{bitOf}_{i}\ x)\,\lsymb{xor}\, (\lsymb{bitOf}_{i}\ y))\wedge \mathrm{carry}_i)
+  \end{array}
+\]
 
+\noindent
 Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
-above when $x$ and $y$ are ``bbterm'' applications. So given that
+above when $x$ and $y$ are ``$\lsymb{bbT}$'' applications. So given that
 \[
   \begin{array}{lcl}
-    x&=&(\mathrm{bbterm}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
-    y&=&(\mathrm{bbterm}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
+    x&=&(\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
+    y&=&(\lsymb{bbT}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
   \end{array}
 \]
 then the rule can be alternatively phrased as
 
 \begin{AletheX}
-$i$. & \ctxsep & $(\mathrm{bvadd}\ x\ y) \simeq (\mathrm{bbterm}\ (x_0 \oplus y_0)\oplus\mathrm{carry}_0\ \ldots\ (x_{n-1}
-        \oplus y_{n-1})\oplus\mathrm{carry}_{n-1})$ & (\currule) \\
+$i$. & \ctxsep & $(\mathrm{bvadd}\ x\ y) ≈ A_2$ & (\currule) \\
 \end{AletheX}
-with ``carry'' being defined, for $i \geq 0$, as 
+with $A_2 := (\lsymb{bbT}\ (x_0 \,\lsymb{xor}\, y_0)\,\lsymb{xor}\,\mathrm{carry}_0\ \ldots\ (x_{n-1}
+        \,\lsymb{xor}\, y_{n-1})\,\lsymb{xor}\,\mathrm{carry}_{n-1})$ and
+``$\mathrm{carry}$'' being defined, for $i \geq 0$, as
 \[
   \begin{array}{lcl}
     \mathrm{carry}_0&=&\bot\\
-    \mathrm{carry}_{i+1}&=&(x_i\wedge y_i)\vee((x_i\oplus y_i)\wedge \mathrm{carry}_i)
+    \mathrm{carry}_{i+1}&=&(x_i\wedge y_i)\vee((x_i\,\lsymb{xor}\, y_i)\wedge \mathrm{carry}_i)
   \end{array}
 \]
 
 \end{RuleDescription}
 
+\begin{RuleDescription}{symm}
+\begin{AletheX}
+$i$. & \ctxsep & $ \varphi ≈ \psi$ & ($\dots$) \\
+$j$. & \ctxsep & $ \psi ≈ \varphi$ & (\currule\; $i$) \\
+\end{AletheX}
+
+\noindent
+If $\varphi \neq \psi$ then the conclusion \emph{must not} be $\varphi ≈ \psi$.
+
+Note that since Alethe allows the implicit reordering of equalities, this
+rule is technically superfluous.  However, the rule is useful to indicate
+an explicit usage of the symmetry of equality to aid proof reconstruction.
+
+\begin{RuleExample}
+The side condition ensures that the following example is not a valid application
+of the rule.  Without this condition, this derivation could be obtained by
+applying symmetry of equality implicitly to the conclusion.
+
+\begin{AletheX}
+$10$. & \ctxsep & $ P(a) ≈ Q(b)$ & ($\dots$) \\
+$11$. & \ctxsep & $ P(a) ≈ Q(b)$ & (\currule\; $10$) \\
+\end{AletheX}
+\end{RuleExample}
+\end{RuleDescription}
+
+\begin{RuleDescription}{not_symm}
+\begin{AletheX}
+$i$. & \ctxsep & $ \neg (\varphi ≈ \psi)$  & ($\dots$) \\
+$j$. & \ctxsep & $ \neg (\psi ≈ \varphi)$  & (\currule\; $i$) \\
+\end{AletheX}
+
+\noindent
+If $\varphi \neq \psi$ then the conclusion \emph{must not} be $\neg (\varphi ≈ \psi)$.
+
+See \proofRule{symm} for an explanation of this rule.
+
+\end{RuleDescription}
+
+\begin{RuleDescription}{eq_symmetric}
+\begin{AletheX}
+$i$. & \ctxsep & $ (t_1 ≈ t_2) ≈ (t_2 ≈ t_1)$ & (\currule) \\
+\end{AletheX}
+
+\noindent
+Note that since Alethe allows the implicit reordering of equalities, this
+rule is technically superfluous.  However, the rule is useful to state
+an explicit usage of symmetry of equality reasoning to aid proof reconstruction.
+\end{RuleDescription}
+
 \clearpage
 \subsection{Index of Rules}
 \label{sec:alethe:rules-index}
diff --git a/spec/shell.nix b/spec/shell.nix
index 0f2987e5dced529fa96c1bfa65ad9843276c6fe0..0c75edcea21a544cafdd34d1f62355b8d112dfee 100644
--- a/spec/shell.nix
+++ b/spec/shell.nix
@@ -18,6 +18,6 @@ pkgs.stdenvNoCC.mkDerivation {
   buildInputs = with pkgs; [
     gnumake
     entr
-    python39Packages.pygments
+    python311Packages.pygments
 	];
 }