1 files changed, 17 insertions, 0 deletions
diff --git a/test/phase5/exact-contextual-abbreviation-ambiguous.tex b/test/phase5/exact-contextual-abbreviation-ambiguous.tex
new file mode 100644
index 0000000..c8fd94c
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation-ambiguous.tex
@@ -0,0 +1,17 @@
+\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}