path: root/test/phase5/exact-inductive-recursive-domain.tex

\begin{inductive}\label{phase5_recursive_domain}
    Define $\phasefivedomain{A}\subseteq\phasefivedomain{A}$ inductively as follows.
    \begin{enumerate}
        \item $A\in\phasefivedomain{A}$.
    \end{enumerate}
\end{inductive}