diff --git a/docs/constructions.tex b/docs/constructions.tex
index 225016c8497075b0615063d5476c3304d2642df5..6a62fa47c889f6dd8471d4027f2bb7b4d074078c 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -295,7 +295,7 @@ The frame-preserving update involves the notion of a \emph{local update}:
 \newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
 \begin{defn}
   It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
-  \[ \All n, \maybe{\melt_\f}. x_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
+  \[ \All n, \maybe{\melt_\f}. \melt_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
 \end{defn}
 In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.