\[ \eqn{ Ingredients }{
\patchof{L} = \pa{L} \lor \patchof{L} = \bot
}\]
-\[ \eqn{ Non-recursion }{
+\[ \eqn{ Create Acyclic }{
L \not\haspatch \pa{Q}
}\]
\subsection{Base Acyclic}
Consider some $D \isin B$. If $D = B$, $D \in \pan{Q}$.
-If $D \neq B$, $D \isin L$, and by Non-recursion
+If $D \neq B$, $D \isin L$, and by Create Acyclic
$D \not\in \pay{Q}$. $\qed$
\subsection{Coherence and Patch Inclusion}