1 files changed, 13 insertions, 2 deletions
diff --git a/test/phase5/exact-inductive-nested.tex b/test/phase5/exact-inductive-nested.tex
index a784652..cd7cf90 100644
--- a/test/phase5/exact-inductive-nested.tex
+++ b/test/phase5/exact-inductive-nested.tex
@@ -1,9 +1,20 @@
-% Nested recursion is outside the exact direct-inductive fragment.
+\begin{proposition}\label{phase5_nested_guard}
+    For all $A, x$ we have if $x\in\pow{\cumul{A}}$, then
+        $A\in\cumul{A}$.
+\end{proposition}
+\begin{proof}
+    Fix $A, x$.
+    Assume $x\in\pow{\cumul{A}}$.
+\end{proof}
+
+\begin{axiom}\label{phase5_nested_unsafe_support}
+    For all $A$ we have $A=A$.
+\end{axiom}
 
 \begin{inductive}\label{phase5_nested}
     Define $\phasefivenested{A}\subseteq\cumul{A}$ inductively as follows.
     \begin{enumerate}
         \item If $x\in\pow{\phasefivenested{A}}$, then
-            $x\in\phasefivenested{A}$.
+            $A\in\phasefivenested{A}$.
     \end{enumerate}
 \end{inductive}