\subsection{Desired Contents}
-\[ $D \isin C \equiv [ D \not\in \pry \land D \isin L$ ] \lor D = C \]
+\[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
{\it Proof.}
\subsubsection{For $D = C$:}
Trivially $D \isin C$. OK.
-\subsubsection{For $D \not\le C$:}
+\subsubsection{For $D \neq C, D \not\le L$:}
+By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
+$D \not\isin R^-$. Thus $D \not\isin C$. OK.
+\subsubsection{For $D \neq C, D \le L, D \in \pry$:}
-\subsubsection{For $D \in R^+$:}
-By Currently Included,
+By Currently Included, $D \isin L$.
+
+By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
+by Unique Tip, $D \le R^+ \equiv D \le L$.
+So $D \isin R^+$.
+
+By Base Acyclic, $D \not\isin R^-$.
+
+Apply $\merge$: $D \not\isin C$. OK.
+
+\subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
+
+By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
+
+Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
+
+$\qed$
\subsection{Unique Base}