\import{test/phase5/exact-producer.tex}

\begin{definition}\label{phase5_imported_definition}
    $\phasefiveimporter{X}{Y} = \phasefivealias{X}{Y}$.
\end{definition}