diff --git a/formalism/constraint.tex b/formalism/constraint.tex
index 0a0d887..a0245dd 100644
--- a/formalism/constraint.tex
+++ b/formalism/constraint.tex
@@ -11,6 +11,8 @@ \section{Constraint generation}
 Here, we give the list of constraint-generating bidirectional typing rules under the marked lambda
 calculus for type hole inference, described in Section 4 of the paper.
 
+\nomechanization{}
+
 \judgbox{\ensuremath{\matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}} $\TMV$ has matched arrow type $\TArrow{\TMV_1}{\TMV_2}$ and generates constraints $C$
 \begin{mathpar}
   \judgment{ }{