1 files changed, 22 insertions, 0 deletions
diff --git a/test/phase5/exact-inductive-wrapper.tex b/test/phase5/exact-inductive-wrapper.tex
new file mode 100644
index 0000000..057528c
--- /dev/null
+++ b/test/phase5/exact-inductive-wrapper.tex
@@ -0,0 +1,22 @@
+\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}