diff --git a/spec/changelog.tex b/spec/changelog.tex
index 9b8d684697153cbca3041f2ab4c0fb19cec288ba..95a38bc5531697560d736f0b94d4dd6c854ad0d9 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -1,4 +1,17 @@
-%\subsection*{Unreleased}
+\subsection*{Unreleased}
+
+List of rules:
+\begin{itemize}
+ \item Improve description of $\proofRule{sko\_ex}$.
+\end{itemize}
+
+\noindent
+Clarifications:
+\begin{itemize}
+ \item Clarify functionality of choice in introduction.
+ \item Add illustratory example to introduction.
+ \item Normalize printing of (variable, term) arguments in the abstract notaton.
+\end{itemize}
\subsection*{0.1 --- \DTMdisplaydate{2021}{07}{10}{-1}}
diff --git a/spec/doc.tex b/spec/doc.tex
index c88deed276168abf6a65ba7ef4294bac67645344..637f851172e862aeb2098cdca5d7ebe50fed1388 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -401,8 +401,10 @@ In addition to the multi-sorted first-order logic used by SMT-LIB,
Alethe also uses Hilbert's choice operator $\varepsilon$. Choice acts
like a binder. The term $\varepsilon x. \varphi$ stands for a value $v$,
such that $\varphi[v/x]$ is true if such a value exists. Any value is
-possible otherwise.
-% PF it might be useful to say that \varepsilon is functional, i.e., if \varphi is logically equivalent to \varpsi then \varepsilon gives the same result
+possible otherwise. Alethe requires that $\varepsilon$ is functional
+with respect to logical equivalence: if for two formulas $\varphi$, $\psi$
+that contain the free variable $x$, it holds that
+$(\forall x.\,\varphi\leftrightarrow\psi)$, then $(\varepsilon x.\, \varphi)\simeq (\varepsilon x.\, \psi)$.
As a matter of notation, we use the symbols $x$, $y$, $z$ for variables,
$f$, $g$, $h$ for functions, and $P$, $Q$ for predicates, i.e.,
@@ -419,9 +421,26 @@ are syntactically equal and the number of leading negations is even
for $\varphi$ and odd for $\psi$, or vice versa. To simplify the
notation we will omit the sort of terms when possible.
+\begin{example} The following example shows a simple Alethe proof.
+It uses quantifier instantiation and resolution to show a contradiction.
+The sections below step-by-step describe the concepts necessary to
+understand the proof intuitively.
+
+\begin{plContainer}
+ \begin{plList}
+ \proofsep& 1.& \forall x.\, P(x) &(\proofRule{assume})\\
+ \proofsep& 2.& \neg P(a) &(\proofRule{assume})\\
+ \proofsep& 3.& \neg (\forall x.\, P(x)) \lor P(a) &(\proofRule{forall_inst};;(x, a))\\
+ \proofsep& 4.& \neg (\forall x.\, P(x)), P(a) &(\proofRule{or}; 3)\\
+ \proofsep& 5.& \bot &(\proofRule{resolution}; 1, 2, 4)\\
+ \end{plList}
+\end{plContainer}
+
+\end{example}
+
\paragraph{Steps.}
A proof in the Alethe format is an indexed list of steps.
-To mimic the concrete syntax we will write a step
+To mimic the concrete syntax we write a step in the form
\begin{plListEq}
c_1,\,\dots,\, c_k &\proofsep i. & \varphi_1,\dots ,\varphi_l &
(\proofRule{rule};\: p_1,\,\dots,\, p_n;\: a_1,\,\dots,\,a_m)
@@ -450,8 +469,12 @@ the \emph{context} of the step. Contexts have their own section below.
Every proof ends with a step that has the empty clause as the conclusion
and an empty context. Section~\ref{sec:rules} provides an overview of
all proof rules used by veriT.
-% PF TODO this above is quite abstract. A figure with a full well-chosen
-% concrete example would be helpful to illustrate this, and the following too
+
+The example above consists of five steps. Step 4 and 5 use premises.
+Since step 3 introduces a tautology, it uses no premises. However,
+it uses arguments to express the substitution $x\mapsto a$ used to instantiate
+the quantifier. Step 4 translates the disjunction into a clause.
+In the example above, the contexts are all empty.
\paragraph{Assumptions.}
The \proofRule{assume} rule introduces a term as an assumption. The
@@ -459,7 +482,10 @@ proof starts with a number of \proofRule{assume} steps. Each step such
corresponds to an assertion. Additional assumptions can be introduced
too. In this case each assumption must be discharged with an appropriate
step. The only rule to do so is the \proofRule{subproof} rule.
-
+
+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.
To prove lemmas, a subproof can
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 2f73d3fef50042932a867323f34110226b9e2558..e0349c17bc10d1c82485721ee9ceba715d0bcefe 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -331,8 +331,7 @@ The \currule{} rule skolemizes existential quantifiers.
\begin{plContainer}
\begin{plSubList}
\plLine\\
-\Gamma, x_1 \mapsto (\varepsilon x_1. (\exists x_2, \dots, x_n. \varphi)), \dots , x_n \mapsto (\varepsilon
-x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{n-1}\mapsto \varepsilon_{n-1}])
+\Gamma, x_1 \mapsto \varepsilon_1, \dots , x_n \mapsto \varepsilon_n
\proofsep& j.&\varphi \leftrightarrow \psi &(\dots)\\
\end{plSubList}
\begin{plList}
@@ -341,7 +340,7 @@ x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{n-1}\mapsto \varepsilon_{n-1}])
\end{plList}
\end{plContainer}
where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
-x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{i-1}\mapsto\varepsilon_{i-1}])$
+x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{i-1}\mapsto\varepsilon_{i-1}])$.
\end{proof-rule}
\begin{proof-rule}{sko_forall}{veriT}
@@ -370,11 +369,11 @@ The \currule{} rule skolemizes universal quantifiers.
\begin{plList}
\proofsep& i.&
\neg (\forall x_1, \dots, x_n. P) \lor P[t_1/x_1]\dots[t_n/x_n]
-&(\currule; ; x_{k_1} := t_{k_1}, \dots, x_{k_n} := t_{k_n})\\
+&(\currule; ; (x_{k_1}, t_{k_1}), \dots, (x_{k_n}, t_{k_n}))\\
\end{plList}
\end{plContainer}
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
+$k_i$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
\smtinline{(:= xki tki)}.
\paragraph{Remark.} A rule simmilar to the \proofRule{let} rule would be