\begin{axiom}\label{phase7_concurrent_earlier_axiom} For all $x$ we have $x = x$. \end{axiom} \begin{proposition}\label{phase7_concurrent_earlier_failure} For all $x$ we have $x = x$. \end{proposition} \begin{proof} Fix $x$. Follows by assumption. \end{proof}