diff --git a/docs/model.tex b/docs/model.tex
index 41b545ca2b4d060157c6b5238edd736e40620bd0..bb91207bb095ca84ae3b7bcc6e913c747dfaba2a 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -58,7 +58,7 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
         \Sem{\vctx \proves \ownM{\melt} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \melt : \textlog{M}}_\gamma \mincl[n] \meltB}  \\
         \Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \melt : \type}_\gamma \in \mval_n} \\
         \Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
-            \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_k \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\melt')
+            \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
           \end{aligned}
 }
 \end{align*}