+\subsection{Coherence and Patch Inclusion}
+
+Consider some $D \in \p$.
+$B \not\in \py$ so $D \neq B$. So $D \isin B \equiv D \isin L$
+and $D \le B \equiv D \le L$.
+
+Thus $L \haspatch \p \implies B \haspatch P$
+and $L \nothaspatch \p \implies B \nothaspatch P$.
+
+$\qed$.
+
+\subsection{Foreign Inclusion}
+
+Simple Foreign Inclusion applies. $\qed$
+
+\subsection{Foreign Contents}
+
+Not applicable.
+
+\section{Create Tip}
+
+Given a Topbloke base $B$, create a tip branch initial commit B.
+\gathbegin
+ C \hasparents \{ B \}
+\gathnext
+ \patchof{B} = \pqy
+\gathnext
+ D \isin C \equiv D \isin B \lor D = C
+\end{gather}
+
+\subsection{Conditions}
+
+\[ \eqn{ Ingredients }{
+ \patchof{B} = \pqn
+}\]
+\[ \eqn{ No Sneak }{
+ \pendsof{B}{\pqy} = \{ \}
+}\]
+
+\subsection{No Replay}
+
+Ingredients Prevent Replay applies. $\qed$