\import{test/phase7/diamond-base.tex}

\begin{proposition}\label{phase7_diamond_left}
    For all $x$ we have $x = x$.
\end{proposition}
