+OK for $C \haspatch \p$.
+
+So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
+
+\subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
+
+$C \haspatch \p \equiv M \nothaspatch \p$.
+
+\proofstarts
+
+Merge Ends applies.
+
+$D \isin Y \equiv D \le Y$. $D \not\isin X$. Recall that we
+are considering $D \in \py$.
+
+Consider $D = C$. Thus $C \in \py, L \in \py$.
+But $X \not\haspatch \p$ means xxx wip
+But $X \not\haspatch \p$ means $D \not\in X$,