test/phase5/exact-inductive.tex


1
2
3
4
5
6
7
8

% One direct inductive whose domain guard is a checked foundation axiom.

\begin{inductive}\label{phase5_fin}
    Define $\phasefivefin{A}\subseteq\cumul{A}$ inductively as follows.
    \begin{enumerate}
        \item $A\in\phasefivefin{A}$.
    \end{enumerate}
\end{inductive}