of $\nothaspatch$, $M \nothaspatch \p$. So by coherence/inclusion $C
\haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
-xxx up to here
-
We will consider some $D$ and prove the Exclusive Tip Contents form.
+\subsubsection{For $D \in \py$:}
+$C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
+\le C$. OK.
-So by definition of
-$\haspatch$, $D \isin C \equiv D \le C$. OK.
-
-\subsubsection{For $L \in \py, D \in \py, $:}
-$R \haspatch \p$ so
+xxx up to here
\subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}