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

\begin{struct}\label{phase5_context_other_magma}
    A phase five context other magma $A$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $\phasefivecombine$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{phase5_context_other_refl} $A = A$.
    \end{enumerate}
\end{struct}

\begin{proposition}\label{phase5_context_ambiguous}
    Let $A,a,b$ be sets.
    Then $\phasefivecombine[A](a,b) = \phasefivecombine[A](a,b)$.
\end{proposition}