diff --git a/spec/doc.tex b/spec/doc.tex
index fad7a5ce2b1088e05a8be5a232e724b833589033..d02e6a6168cacb2801ad49ab951518dced98927a 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -307,8 +307,10 @@ proofs and a set of proof rules.  On the one side, the language is
 inspired by natural-deduction and is based on the widely used SMT-LIB
 format.  The language also includes a flexible mechanism to reason
 about bound variables which allows fine-grained preprocessing proofs.
+%
 On the other side, the rules are structured around resolution and the
-introduction of theory lemmas.
+introduction of theory lemmas, in the same way as CDCL($\mathcal{T}$)-based SMT
+solvers.
 
 The specification is speculative in the sense that it is not yet
 cast in stone, but it will evolve over time. It emerged from a list
@@ -329,12 +331,14 @@ such tools.
 Nevertheless, it not only serves as a norm to ensure compatibility
 between tools, it also allows us to uncover the unsatisfactory aspects
 that would otherwise be hidden deep within the nooks and crannies of
-solver source code. Every uncovered problem presents an opportunity
+solver and checker implementations.
+%
+Every uncovered problem presents an opportunity
 to improve the format. The authors of this document overlap with the
 authors of those tools and we are committed to improve the tools, the
 format, and ultimately the specification together.
 This document is also an invitation to other researchers to join
-the efforts. To read the reference and provide feedback, or to even
+these efforts. To read the reference and provide feedback, or to even
 implement support for Alethe into their own tools. Please
 get in touch!
 
@@ -344,43 +348,51 @@ get in touch!
 
 \section{Introduction}
 
-This document is a reference of the Alethe format.  The format
-is designed to be a flexible format to represent unsatisfiability
-proofs generated by SMT solvers.  The overall design follows
-a few core
-concepts, such as a natural-deduction style structure and resolution.
-It is split into two parts: the proof language and a set of rules.
+This document is a reference of the Alethe format.  The format is designed to be
+a flexible format to represent unsatisfiability proofs generated by SMT solvers.
+The overall design follows a few core concepts, such as a natural-deduction
+style structure and rules generating and operating on ground first-order
+clauses.
+%
+There are two parts in this document: the proof language and a proof calculus.
 Section~\ref{sec:language} introduces the language.  First informally,
-then formally. Section~\ref{sec:rules-general} discusses some core
-concept behind Alethe proof rules.
-At the end of the document Section~\ref{sec:rules} contains a full list
-of all proof rules used by SMT solvers supporting Alethe.
-
-The concrete syntax and semantic is based on the SMT-LIB~\cite{SMTLIB}
-format, which is widely used as input and output format of SMT
-solvers. Hence, the base logic is the many-sorted first-order logic of
-SMT-LIB. This document assumes the reader is familiar with the SMT-LIB
-standard.  As discussed in Section~\ref{sec:syntax} the concrete syntax
-of Alethe is based on the SMT-LIB syntax.
-
-The format is currently used by the CDCL($T$)-based SMT solver
-veriT~\cite{verit}. If requested by the user, veriT outputs a proof if it can
-deduce that the input problem is unsatisfiable. In proof production mode, veriT
-supports the theory of uninterpreted functions, the theory of linear integer and
-real arithmetic, and quantifiers.  The Alethe proofs can be reconstructed
-by the \texttt{smt} tactic of the proof assistant
-Isabelle/HOL~\cite{fleury-2019,schurr-2021}.  Furthermore, in the future the SMT
-solver cvc5 (the successor of CVC4~\cite{CVC4}) will support Alethe as
-one of multiple proof output formats.
+then formally.
+%
+Section~\ref{sec:rules-generic} discusses the core
+concepts behind the Alethe proof calculus.
+%
+At the end of the document Section~\ref{sec:rules} presents a list of all proof
+rules used by SMT solvers supporting Alethe.
+
+The semantics (Section~\ref{sec:semantic}) and concrete syntax
+(Section~\ref{sec:syntax}) are based on the SMT-LIB~\cite{SMTLIB}
+format, widely used as the input and output standard for SMT solvers.
+%
+Hence, Alethe's base logic is the many-sorted first-order logic of SMT-LIB. This
+document assumes the reader is familiar with the SMT-LIB standard.
+
+The format is currently used by the SMT solver veriT~\cite{verit}. If requested
+by the user, veriT outputs a proof if it can deduce that the input problem is
+unsatisfiable. In proof production mode, veriT supports the theory of
+uninterpreted functions, the theory of linear integer and real arithmetic, and
+quantifiers.
+%
+The Alethe proofs can be reconstructed by the \texttt{smt} tactic
+of the proof assistant Isabelle/HOL~\cite{fleury-2019,schurr-2021}, as well as
+by SMTCoq in the proof assistant Coq~\cite{SMTCoq}.
+%
+The SMT solver cvc5 (the successor of CVC4~\cite{CVC4}) supports Alethe
+experimentally as one of its multiple proof output formats.
 
 In addition to this reference, the proof format has been discussed in past
 publications which provide valuable background information.  The core of
 the format goes back to 2011 when two publications at the PxTP workshop
-outlined the the fundamental ideas behind the format~\cite{besson-2011}
-and proposed rules for quantifier instantiation~\cite{deharbe-2011}
-More recently the format has gained support for reasoning typically used
-for processing, such as Skolemization, renaming of variables, and other
-manipulations of bound variables~\cite{barbosa-2019}.
+outlined the fundamental ideas behind the format~\cite{besson-2011}
+and proposed rules for quantifier instantiation~\cite{deharbe-2011}.
+%
+More recently the format has gained support for reasoning typically used for
+processing, such as Skolemization, substitutions, and other manipulations of
+bound variables~\cite{barbosa-2019}.
 
 \section{The Alethe Language}
 \label{sec:language}
@@ -449,10 +461,11 @@ To mimic the concrete syntax we write a step in the form
 		(\proofRule{rule};\: p_1,\,\dots,\, p_n;\: a_1,\,\dots,\,a_m)
 \end{plListEq}
 \noindent
-Each step has an index \(i \in \mathbb{I}\) where \(\mathbb{I}\) is a countable
+Each step has a unique index \(i \in \mathbb{I}\), where \(\mathbb{I}\) is a countable
 infinite set of valid indices. In the concrete syntax all SMT-LIB symbols are
-valid indices, but for examples we will use natural numbers. No two steps have
-the same index. Furthermore, a step has a clause \(\varphi_1,
+valid indices, but for examples we will use natural numbers.
+%
+Furthermore, a step has a clause \(\varphi_1,
 \dots ,\varphi_l\) as its conclusion. If a step has the empty clause
 as its conclusion (i.e., \(l = 0\)) we will write \(\bot\).  While this
 muddles the water a bit with regards to steps which have the unit clause
@@ -488,7 +501,10 @@ The example above uses two assumptions which are introduced in the first
 two steps.
 
 \paragraph{Subproofs and Lemmas.}
-Alethe uses subproof to prove lemmas and to manipulate the context.
+Alethe uses subproofs to create new contexts
+
+prove lemmas and to manipulate the context.
+%
 To prove lemmas, a subproof can
 introduce local assumptions. The \proofRule{subproof} \emph{rule} discharges the
 local assumptions.
@@ -496,7 +512,9 @@ From an
 assumption $\varphi$ and a formula $\psi$ proved by intermediate steps
 from $\varphi$, the \proofRule{subproof} rule deduces the clause $\neg \varphi, 
 \psi$ that discharges the local assumption $\varphi$.
+%
 A \proofRule{subproof} step can not use premise from a subproof nested within the current subproof.
+
 \begin{comment}{Mathias Fleury}
 There are two ways to export one element from the subproof:
 \begin{itemize}
@@ -1050,7 +1068,7 @@ $\grT{define-fun}$ command to define shorthand 0-ary functions for
 the $\grT{(choice }\dots\grT{)}$ terms needed. Without this option,
 no $\grT{define-fun}$ commands are issued and the constants are expanded.
 
-\section{The Alethe Rules}
+\section{The Alethe proof calculus}
 \label{sec:rules-generic}
 
 Together with the language, the Alethe format also comes with a set