+\item[ $ C \zhaspatch \p $ ]
+$\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
+~ Informally, $C$ has all the reachable contents of $\p$.
+
+\item[ $ C \haspatch \p $ ]
+$\displaystyle C \zhaspatch \p \land \exists_{F \in \py} F \le C $.
+~ Informally, $C$ nontrivially has all the reachable contents of $\p$.
+
+Note that $\zhaspatch$ and $\nothaspatch$ are neither
+mutually exclusive nor exhaustive.
+$\haspatch$ and $\nothaspatch$ are mutually exclusive but not
+necessarily exhaustive.
+