diff --git a/formalism/marked.tex b/formalism/marked.tex
index 6f56181..07d746b 100644
--- a/formalism/marked.tex
+++ b/formalism/marked.tex
@@ -432,7 +432,7 @@ \subsection{Marking}
   \inferrule[MKALam3]{
     \matchedArrow{\TMV_3}{\TMV_1}{\TMV_2} \\
     \inconsistent{\TMV}{\TMV_1} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\EMV}{\ECMV}{\TMV_2}
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV}}{\EMV}{\ECMV}{\TMV_2}
   }{
     \ctxAnaFixedInto{\ctx}{\ELam{x}{\TMV}{\EMV}}{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\TMV_3}
   }
@@ -557,7 +557,7 @@ \subsection{Marked expressions}
   \inferrule[MSIf]{
     \ctxAnaTypeM{\ctx}{\ECMV_1}{\TBool} \\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\
-    \ctxSynTypeM{\ctx}{\ECMV_3}{\TMV_2}
+    \ctxSynTypeM{\ctx}{\ECMV_3}{\TMV_2} \\
     \TMV_3 = \TMeet{\TMV_1}{\TMV_2}
   }{
     \ctxSynTypeM{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV_3}
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
index 30ecdab..45b1124 100644
--- a/formalism/polymorphism.tex
+++ b/formalism/polymorphism.tex
@@ -436,7 +436,7 @@ \subsection{Marking}
     \tvarCtxTypeMarkedInto{\tvarCtx}{\TMV_2}{\MTMV_2} \\
     \notMatchedForall{\MTMV}
   }{
-    \bothCtxSynFixedInto{\tvarCtx}{\ctx}{\ETypeAp{\EMV}{\TMV_2}}{\ECTypeAp{\ECMV}{\MTMV_2}}{\MTUnknown}
+    \bothCtxSynFixedInto{\tvarCtx}{\ctx}{\ETypeAp{\EMV}{\TMV_2}}{\ECTypeApSynNonMatchedForall{\ECMV}{\MTMV_2}}{\MTUnknown}
   }
 \end{mathpar}