diff --git a/aspUnify.tex b/aspUnify.tex
index ee4b63c..2d854c5 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -23,6 +23,8 @@
 \usepackage{mathpartir}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{enumitem}
+%\usepackage{amsthm}
 
 \begin{document}
 %
@@ -230,4 +232,29 @@ constraints in the original constraint set and
 there exists a typing for the remaining type placeholders 
 so that the constraint set is satisfied.
 
+Proof:
+\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
+\newcommand*\ncasesmakelabel[1]{Case #1}
+
+\newenvironment{subproof}
+  {\def\proofname{Subproof}%
+   \def\qedsymbol{$\triangleleft$}%
+   \proof}
+  {\endproof}
+
+\begin{proof}
+  Some text or \texttt{\string\leavevmode} (so the enumerate starts in another line)
+  \begin{enumerate}[ncases]
+    \item $\tv{a} \lessdot \type{T}$ where $\tv{a} \notin \type{T}$.
+    \begin{subproof}
+     Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
+    \end{subproof}
+    \item Bar.
+    \begin{subproof}
+     Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
+    \end{subproof}
+  \end{enumerate}
+  And more text.
+\end{proof}
+
 \end{document}