formalism: Add clause for type marking unicity

hazelgrove · Jun 2, 2023 · 982f349 · 982f349
1 parent 3b82c72
commit 982f349
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -621,6 +621,10 @@ \subsubsection{Metatheorems}
 
 \begin{theorem}[name=Marking Unicity] \
   \begin{enumerate}
+    \item If $\tvarCtxTypeMarkedInto{\tvarCtx}{\TMV}{\MTMV_1}$,
+        and $\tvarCtxTypeMarkedInto{\tvarCtx}{\TMV}{\MTMV_2}$,
+      then $\equal{\MTMV_1}{\MTMV_2}$.
+
     \item If $\bothCtxSynFixedInto{\tvarCtx}{\ctx}{\EMV}{\ECMV_1}{\MTMV_1}$
         and $\bothCtxSynFixedInto{\tvarCtx}{\ctx}{\EMV}{\ECMV_2}{\MTMV_2}$,
       then $\equal{\ECMV_1}{\ECMV_2}$ and $\equal{\MTMV_1}{\MTMV_2}$.