\import{test/phase5/exact-contextual-abbreviation.tex}

\begin{proposition}\label{phase5_context_missing}
    Let $a,b$ be sets.
    Then $a\phasefivedot b = b\phasefivedot a$.
\end{proposition}