\begin{axiom}\label{phase7_batch_prefix}
    $\emptyset = \emptyset$.
\end{axiom}

\begin{struct}\label{phase7_batch_structure}
    A phase seven batch structure $X$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $\phaseSevenPick$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{phase7_batch_first} $X = X$.
        \item\label{phase7_batch_second}
            $\phaseSevenPick[X] = \phaseSevenPick[X]$.
    \end{enumerate}
\end{struct}