\subsection{Tip Contents}
-xxx up to here
-
We need worry only about $C \in \py$.
And $\patchof{C} = \patchof{L}$
so $L \in \py$ so $L \haspatch \p$. We will use the coherence and
patch inclusion of $C$ as just proved.
-Firstly we prove $C \haspatch \p$: If $R \in \py$, this is true by
-coherence/inclusion $C \haspatch \p$. If $R \not\in \py$ then
-by Tip Merge
+Firstly we prove $C \haspatch \p$: If $R \in \py$, then $R \haspatch
+\p$ and by coherence/inclusion $C \haspatch \p$ . If $R \not\in \py$
+then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
+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.