\begin{abbreviation}\label{phase5_nested_wrapper}
    $\phasefivenestedwrapper{A}=\pow{A}$.
\end{abbreviation}

\begin{proposition}\label{phase5_nested_wrapper_guard}
    For all $A, x$ we have if
        $x\in\phasefivenestedwrapper{\cumul{A}}$, then
        $A\in\cumul{A}$.
\end{proposition}
\begin{proof}
    Fix $A, x$.
    Assume $x\in\phasefivenestedwrapper{\cumul{A}}$.
\end{proof}

\begin{inductive}\label{phase5_nested_wrapper_inductive}
    Define $\phasefivenestedwrapped{A}\subseteq\cumul{A}$ inductively as follows.
    \begin{enumerate}
        \item If
            $x\in\phasefivenestedwrapper{\phasefivenestedwrapped{A}}$, then
            $A\in\phasefivenestedwrapped{A}$.
    \end{enumerate}
\end{inductive}