-various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
-(which suffices by definition of $\haspatch$ and $\nothaspatch$).
-
-Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
-Self Inpatch for $L$, $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
-$M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
-$M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
-
-Consider $D \neq C, M \nothaspatch P, D \isin Y$:
+various cases that
+if $M \haspatch \p$, $D \not\isin C$,
+whereas if $M \nothaspatch \p$, $D \isin C \equiv D \le C$.
+And by $Y \haspatch \p$, $\exists_{F \in \py} F \le Y$ and this
+$F \le C$ so this suffices.
+
+Consider $D = C$: Thus $C \in \py, L \in \py$.
+By Tip Own Contents, $L \haspatch \p$ so $L \neq X$,
+therefore we must have $L=Y$, $R=X$.
+Conversely $R \not\in \py$
+so by Tip Merge $M = \baseof{L}$. Thus $M \in \pn$ so
+by Base Acyclic $M \nothaspatch \p$. By $\merge$, $D \isin C$,
+and $D \le C$. OK.
+
+Consider $D \neq C, M \nothaspatch \p, D \isin Y$: