\right]
\implies
\left[
- D \isin C
+ D \le C
\implies
\patchof{D} = \bot
\right]
}\]
-xxx proof tbd
+\proof{
+Consider some $D \le C$. If $D = C$, $\patchof{D} = \bot$ trivially.
+If $D \neq C$ then $D \le A$ where $A \in \set A$. By Foreign
+Contents of $A$, $\patchof{D} = \bot$.
+}
\subsection{No Replay for Merge Results}
\subsection{Foreign Contents:}
-Only relevant if $\patchof{C} = \bot$. Trivial by Foreign Contents of
-$A$. $\qed$
-
-xxx fixme not trivial use Totally Foreign Contents
+Only relevant if $\patchof{C} = \bot$, and in that case Totally
+Foreign Contents applies. $\qed$
\section{Create Base}
\subsection{Foreign Contents}
-xxx use Totally Foreign Contents
-
-If $\patchof{C} = \bot$, by Foreign Merges
-$\patchof{L} = \patchof{R} = \bot$.
+Only relevant if $\patchof{L} = \bot$, in which case
+$\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
+so Totally Foreign Contents applies. $\qed$
\end{document}