-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$. By Tip Contents
-for $L$, $L \isin L$ so $\neg [ L \nothaspatch \p ]$.
-Therefore we must have $L=Y$, $R=X$.
-By Tip Merge $M = \baseof{L}$ so $M \in \pn$ so
+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