diff --git a/spec/doc.tex b/spec/doc.tex
index 38138cdb7c8cbd335102ff24b0948b5e209597cc..42605bc3061ae1c3baf3d45b4cbb129378dc9350 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -485,8 +485,8 @@ understand the proof intuitively.
 A proof in the Alethe language is an indexed list of steps.
 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 &
-		(\ruleType{rule}\; p_1,\,\dots,\, p_n)\,[a_1,\,\dots,\,a_m]
+  c_1,\,\dots,\, c_k &\proofsep i. & \varphi_1,\dots ,\varphi_l &
+    (\ruleType{rule}\; p_1,\,\dots,\, p_n)\,[a_1,\,\dots,\,a_m]
 \end{plListEq}
 \noindent
 Each step has a unique index \(i \in \mathbb{I}\), where \(\mathbb{I}\) is a countable
@@ -548,8 +548,8 @@ A \proofRule{subproof} step can not use premise from a subproof nested within th
 \begin{comment}{Mathias Fleury}
 There are two ways to export one element from the subproof:
 \begin{itemize}
-	\item rely on the order and take the last one
-	\item add an explicit :premises in the conclusion stop to give the exported step
+  \item rely on the order and take the last one
+  \item add an explicit :premises in the conclusion stop to give the exported step
 \end{itemize}
 \end{comment}
 
@@ -640,17 +640,17 @@ In the following a concluding rule is a proof rule that concludes a
 subproof (such as \proofRule{subproof} and \proofRule{bind}).
 
 \begin{definition}[Calculated Context]
-	Let $s_i$ be a step or anchor in $P$ such that no step $s_j$
-	where $j < i$ uses a concluding
-	rule.  Let $a_1, \dots, a_m$ be the anchors among $s_1, \dots, s_{i-1}$.
+  Let $s_i$ be a step or anchor in $P$ such that no step $s_j$
+  where $j < i$ uses a concluding
+  rule.  Let $a_1, \dots, a_m$ be the anchors among $s_1, \dots, s_{i-1}$.
 
-	The calculated context of $s_i$ is the context
-	$c_{1,1}, \dots, c_{1, n_1}, \dots, c_{m,1}, \dots, c_{m, n_m}$
-	where $c_{k,1}, \dots, c_{k, n_k}$ is the context of $a_k$.
+  The calculated context of $s_i$ is the context
+  $c_{1,1}, \dots, c_{1, n_1}, \dots, c_{m,1}, \dots, c_{m, n_m}$
+  where $c_{k,1}, \dots, c_{k, n_k}$ is the context of $a_k$.
 
-	Note that if $s_i$ is an anchor, its calculated context is the
-	context before concatenating it with the context associated
-	with $s_i$.
+  Note that if $s_i$ is an anchor, its calculated context is the
+  context before concatenating it with the context associated
+  with $s_i$.
 \end{definition}
 
 To check the validity of a proof we can inductively eliminate subproofs
@@ -671,30 +671,28 @@ Of course this is only valid if the steps that are replace do not contain
 partial subpoors.  Due to our induction, we will only replace entire subproofs that
 do not contain subpoof.
 
-\begin{definition}[Admissible Proof, Pure Subproofs]
-	Let $P_i$ be the proof $[s_1, \dots, s_n]$ and $1 \leq \mathit{start}
-	< \mathit{end} \leq n$ such that
-	\begin{itemize}
-		\item $s_{\mathit{start}}$ is an anchor,
-		\item $s_{\mathit{end}}$ is a step that uses a concluding rule,
-		\item no $s_k$ with $\mathit{start} < k < \mathit{end}$ is an anchor or
-		 a step that uses a concluding rule.
-	\end{itemize}
-	The proof $P_i$ is \emph{admissible} if it either contains no such $\mathit{start}$,
-	$\mathit{end}$, or
-	\begin{itemize}
-		\item all steps $s_k$ with $\mathit{start} < k <
-		\mathit{end}$ only use the premises $s_l$ with $\mathit{start} <
-		l < k$,
-		\item all steps $s_k$ are valid application of their rule under the
-		calculated context of $s_{\mathit{start}}$,
-		\item the step $s_{\mathit{end}}$ is a valid application of its rule
-		under its calculated context,
-		\item the proof $P_{i+1}$, where the steps $s_{\mathit{start}}, \dots,
-		s_{\mathit{end}}$ have been replaced by $s'$ as described above, is admissible.
-	\end{itemize}
-	We call the admissible proof $[s_{\mathit{start}}, \dots, s_{\mathit{end}}]$ a \emph{pure
-	subproof}.
+\begin{definition}[Admissible Proof]
+  Let $P_i$ be the proof $[s_1, \dots, s_n]$ and $1 \leq \mathit{start}
+  < \mathit{end} \leq n$ such that
+  \begin{itemize}
+    \item $s_{\mathit{start}}$ is an anchor,
+    \item $s_{\mathit{end}}$ is a step that uses a concluding rule,
+    \item no $s_k$ with $\mathit{start} < k < \mathit{end}$ is an anchor or
+     a step that uses a concluding rule.
+  \end{itemize}
+  The proof $P_i$ is \emph{admissible} if it either contains no such $\mathit{start}$,
+  $\mathit{end}$, or
+  \begin{itemize}
+    \item all steps $s_k$ with $\mathit{start} < k <
+    \mathit{end}$ only use the premises $s_l$ with $\mathit{start} <
+    l < k$,
+    \item all steps $s_k$ are valid application of their rule under the
+    calculated context of $s_{\mathit{start}}$,
+    \item the step $s_{\mathit{end}}$ is a valid application of its rule
+    under its calculated context,
+    \item the proof $P_{i+1}$, where the steps $s_{\mathit{start}}, \dots,
+    s_{\mathit{end}}$ have been replaced by $s'$ as described above, is admissible.
+  \end{itemize}
 \end{definition}
 
 Since proofs are finite, this process stops at some admissible proof
@@ -704,19 +702,19 @@ $P_{\mathit{last}}$.  Otherwise, we can check $P_{\mathit{last}}$ to
 see if the overall proof is valid.
 
 \begin{definition}[Valid Alethe Proof]
-	An Alethe proof $P_0 = [s_1, \dots, s_n]$ is valid if
-	\begin{itemize}
-		\item $P_0$ does not contain any step that uses the \proofRule{hole} rule,
-		\item each step in $P_0$ uses an unique index,
-		\item $P_0$ is admissible,
-		\item $P_0$ contains a step that has the empty clause as its conclusion,
-		\item $P_{\mathit{last}}$ does not contain any anchor or step using a concluding
-		rule,
-		\item all steps $s_k$ in $P_{\mathit{last}}$
-		only use the premises $s_l$ with $1 \leq l < k$,
-		\item all steps in $P_{\mathit{last}}$ are valid
-		applications of their rules under the empty context.
-		\end{itemize}
+  An Alethe proof $P_0 = [s_1, \dots, s_n]$ is valid if
+  \begin{itemize}
+    \item $P_0$ does not contain any step that uses the \proofRule{hole} rule,
+    \item each step in $P_0$ uses an unique index,
+    \item $P_0$ is admissible,
+    \item $P_0$ contains a step that has the empty clause as its conclusion,
+    \item $P_{\mathit{last}}$ does not contain any anchor or step using a concluding
+    rule,
+    \item all steps $s_k$ in $P_{\mathit{last}}$
+    only use the premises $s_l$ with $1 \leq l < k$,
+    \item all steps in $P_{\mathit{last}}$ are valid
+    applications of their rules under the empty context.
+    \end{itemize}
 \end{definition}
 
 In this document we will often call $P_{\mathit{last}}$ the outermost
@@ -725,7 +723,8 @@ proof.
 \subsubsection{Soundness}
 
 To show the soundness of a valid Alethe proof $P = [s_1, \dots, s_n]$
-we can use the same induction as the for the definition of validity.
+we can use the same approach as for the definition of validity:  consider
+subproof free subproofs and then replace subproofs by holes.
 
 \begin{theorem}[Soundness of Alethe]
 If there is a valid Alethe proof $P$ that has the formulas
@@ -736,28 +735,53 @@ steps in its outermost proof, then
 \]
 \end{theorem}
 
-We wills start with simple subproofs with empty contexts and then add contexts.
+We wills start with simple subproofs without subproofs and with empty contexts.
 Here, we will assume that every rule is sound.
 
 \begin{lemma}
-	Let $P = [s_1, \dots, s_n]$ be a pure subpoof such that no $s_i$ is
-	an anchor, $s_n$ is a \proofRule{subproof} step with the conclusion
-	$\psi$, and $\varphi_1, \dots, \varphi_m$ are the conclusion of \proofRule{assume}
-	steps.  Then $\vDash \varphi_1, \dots, \varphi_m \limp \psi$.
+  Let $P = [s_{\mathit{start}}, \dots, s_{\mathit{end}}]$ be an
+  admissible proof such that no $s_i$ with $ i> 1$ is an anchor,
+  $s_{\mathit{end}$ is a \proofRule{subproof} step with the
+  conclusion $\psi$, and $\varphi_1, \dots, \varphi_m$ are the
+  conclusion of \proofRule{assume} steps.  Then $\vDash \varphi_1,
+  \dots, \varphi_m \limp \psi$.
 \end{lemma}
 \begin{proof}
-	Let $s_j$ be the premise of the step $s_n$.  Due to the definition of
-	\proofRule{subproof}, this conclusion of $s_j$ is $\psi$.  If we can
-	show that $s_j$ means $\varphi_1, \dots, \varphi_m  \vDash \psi$,
-	then $\vDash \varphi_1, \dots, \varphi_m \limp \psi$ since
-	\proofRule{subproof} is sound.
-
-	We show this by induction over the proof steps.  Let $V_0 = \emptyset$.
-	Let $\psi_i$ be the conclusions of the step $s_i$.  If $s_i$ is an
-	\proofRule{assume} step, then let $V_i = V_{i-1} \cup \{\psi_i\}$.
-	Otherwies, 
+  By induction over the proof steps we can show that for each step $s_i$ with
+  the conclusion $\psi_i$ it holds that $V_i \vDash \psi_i$ where
+  $V_i$ is the set formulas assumed before $s_i$.
+
+  Let $V_0 = \emptyset$.
+  Let $\psi_i$ be the conclusions of the step $s_i$.  If $s_i$ is an
+  \proofRule{assume} step, then let $V_i = V_{i-1} \cup \{\psi_i\}$.
+  Otherwise,  let $S$ be the set of premises of $s_i$ and $P$ the set
+  of the conclusions of the steps in $S$.
+  Since $s_i$ is a valid application of its rule, we have $P \vDash \psi_i$.
+
+  Now, for every step $s_j \in S$ with the conclusion $\psi_j \in P$, we
+  have $j < i$ and $V_j \vDash \psi_j$ due to the induction hypothesis. Since $j < i$, the
+  premises $V_j$ are a subset of $V_i$ and we can weaken $V_j \vDash \psi_j$ to
+  $V_i \vDash \psi_j$. Consequently, $V_i \vDash \psi_i$.
+
+  This process ends when $s_{\mathit{end}}$ is reached and we
+  get $\varphi_1, \dots, \varphi_n \vDash \psi$ and by definition of
+  \proofRule{subproof} $\vDash \varphi_1, \dots, \varphi_m \limp \psi$.
 \end{proof}
 
+To clarify the subproofs with contexts, we translate the contexts into
+$\lambda$-terms.  For a deeper description of this approach see the 
+publication that introduced this approach~\cite{barbosa-2019}.
+These $\lambda$-terms are called \emph{metaterms}
+
+\begin{definition}[Metaterm]
+	Metaterms are expressions constructed by the grammar
+	\[
+		M \,::=\, \boxed{t}\,\mid\, \lambda x.\,M\,\mid\,(\lambda \bar{x}_n.\,
+		M)\,\bar{t}_n
+	\]
+
+\end{definition}
+
 \subsubsection{Abstract Inference System}  % or Rules, or Rules of Inference
 \label{sec:inference-system}
 Most of the content is taken from the presentation and the correctness proof of
@@ -1250,22 +1274,22 @@ remove the steps of the subproof from memory after checking it.
    There is an open question with regard to the best way to print
    subproofs:
 
-	 There is an implicit relation between the last step of the subproof
+   There is an implicit relation between the last step of the subproof
        and the step concluding the subproof.
     {\textrightarrow} what if we would, for some reason, have some crap after the last step
     of the subproof? We cannot accommodate this yet.
 
-	There are multiple solutions to solve this implicit dependency.
+  There are multiple solutions to solve this implicit dependency.
 
-	{\textbullet} One is to
-	give the final step of the subproof as a premise to the step concluding
-	the subproof.
-		{\textrightarrow} downside: normally it's forbidden to use steps from within a deeper proof
+  {\textbullet} One is to
+  give the final step of the subproof as a premise to the step concluding
+  the subproof.
+    {\textrightarrow} downside: normally it's forbidden to use steps from within a deeper proof
 
-	{\textbullet} We could have the conclusion of the subproof already in the anchor.
-	or we could turn the current structure upside down
-	  {\textrightarrow} downside: a solver that just dumps out steps can not no always know
-	      the conclusion when opening a subproof. For example, when simplifications are applied.
+  {\textbullet} We could have the conclusion of the subproof already in the anchor.
+  or we could turn the current structure upside down
+    {\textrightarrow} downside: a solver that just dumps out steps can not no always know
+        the conclusion when opening a subproof. For example, when simplifications are applied.
 \end{comment}
 
 \subsection*{Sharing and Skolem Terms}
@@ -1492,7 +1516,7 @@ f(t_1, \dots, t_n) \simeq f(u_1, \dots, u_n)\) \\
 P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n)\) \\
 \ruleref{qnt_cnf} & Clausification of a quantified formula. \\
 \ruleref{and_pos} & \(\neg (\varphi_1 \land \dots \land \varphi_n) , \varphi_k \) \\
-\ruleref{and_neg} & \( (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1	, \dots , \neg\varphi_n \) \\
+\ruleref{and_neg} & \( (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1  , \dots , \neg\varphi_n \) \\
 \ruleref{or_pos} & \( \neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots , \varphi_n \) \\
 \ruleref{or_neg} & \( (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k \) \\
 \ruleref{xor_pos1} & \( \neg (\varphi_1 \operatorname{xor} \varphi_2) , \varphi_1 , \varphi_2 \) \\
@@ -1610,7 +1634,7 @@ Rule & Description \\
 \ruleref{and_pos} & \(\neg (\varphi_1 \land \dots \land \varphi_n), \varphi_k\)\\
 \ruleref{and_neg} & \((\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n \) \\
 \ruleref{or_pos} & \(\neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots
-	, \varphi_n \) \\
+  , \varphi_n \) \\
 \ruleref{or_neg} &
 \( (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k \)\\
 \ruleref{xor_pos1} &