1: \begin{definition}\label{DefAuxCon}

2:  \begin{itemize}

3:   \item The set of positions of an expression $e$ is the set $\pos{e}$ of strings over the alfabet of positive integers defined as $\pos{X} = \{\epsilon\}$, if $X \in \var$; $\pos{h(e_1, \ldots, e_n)} = \{\epsilon\} \cup \bigcup_{i \in \{1, \ldots, n\}} \{i.p~|~p \in \pos{e_i}\}$ otherwise, where $\epsilon$ denotes the empty string and $\_.\_$ is used for concatenation.\\

4:  We say that two positions are parallel if none of them is prefix of the other.

5:   \item For any $e \in Exp_\perp$, $p \in \pos{e}$, the subexpression of $e$ at position $p$ denoted by $s|_p$, is defined as $e|_\epsilon = e$; $h(e_1, \ldots, e_n)|_{i.q}= e_i|_q$.

6:   \item For any $e,e' \in Exp_\perp$, $p \in \pos{e}$, by $e[e']_p$ we denote the expression obtained from $e$ by replacing the subexpression at position $p$ by $e'$, defined as $e[e']_\epsilon = e'$; $f(e_1, \ldots, e_n)[e']_{i.q} = f(e_1, \ldots, e_i[e']_q, \ldots, e_n)$.

7:   \item As one-hole context can be understood as funcions $\con : Exp_\perp \rightarrow Exp_\perp$, for any $\con \in Cntx$ we may assume some $e \in Exp_\perp, p \in \pos{e}$ such that $\con = \lambda e'.e[e']_p$. With this in mind Theorem \ref{lCompPS} can be recasted as $\denp{e[e']_p} = \bigcup_{\overline{t} \subseteq \denp{e'}} \denp{e[?\overline{t}]_p}$, where $?\{t_1, \ldots, t_n\}$ denotes $t_1~?~\ldots~?~t_n$ for some arrangement of the elements of $\{t_1, \ldots,$ $t_n\}$ in $t_1~?~\ldots~?~t_n$.

8:  \end{itemize}

9: \end{definition}

10: