\begin{axiom}\label{phase7_dependent_prefix} $\emptyset = \emptyset$. \end{axiom} \begin{proposition}\label{phase7_dependent_proof} For all $x$ we have $x = x$. \end{proposition} \begin{proof} Fix $x$. Show $x = x$. \begin{subproof} Follows by assumption. \end{subproof} Follows by assumption. \end{proof}