prove and use totally foreign contents

diff --git a/article.tex b/article.tex
index f69420fc071f170952b9e5a60ca9a60916658ec5..65be01f4e3e5b51b9a378e5dc73d854c82723f1c 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -301,12 +301,16 @@ xxx proof tbd
    \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}
 
@@ -461,10 +465,8 @@ $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 
 \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}
 
@@ -908,9 +910,8 @@ $\qed$
 
 \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}