path: root/test/phase5/exact-inductive-unsupported-context.tex

\begin{inductive}\label{phase5_nested_unsupported_context}
    Define $\phasefiveunsupported{A}\subseteq\cumul{A}$ inductively as follows.
    \begin{enumerate}
        \item If $x\in\{z\in\phasefiveunsupported{A}\mid z=z\}$, then
            $x\in\phasefiveunsupported{A}$.
    \end{enumerate}
\end{inductive}