+\subsection{Traversal Lemmas}
+
+Firstly, some lemmas.
+\statement{Tip Correct Contents}{
+ \tipcy \haspatch \pa E
+ \equiv
+ \pa E = \pc \lor \pa E \isdep \pc
+}
+\proof{
+ For $\pc = \pa E$, Tip Own Contents suffices.
+ For $\pc \neq \pa E$, Exclusive Tip Contents
+ gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$
+ which by Correct Base $\equiv D \isin \tipcn$.
+}
+