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

\begin{inductive}\label{phase5_nested_recursive_element}
    Define $\phasefiveelement{A}\subseteq\cumul{A}$ inductively as follows.
    \begin{enumerate}
        \item If $\phasefiveelement{A}\in\pow{\phasefiveelement{A}}$, then
            $A\in\phasefiveelement{A}$.
    \end{enumerate}
\end{inductive}