1 2 3 4 5 6
\begin{datatype}\label{phase5_nested_data} Define $\phasefivenesteddata$ inductively as follows. \begin{enumerate} \item $\phasefivenested{p} \in \phasefivenesteddata$ for $p \in \pow{\phasefivenesteddata}$. \end{enumerate} \end{datatype}