diff --git a/docs/model.tex b/docs/model.tex
index 9d1bef1a0fa66102013640e2720fc1ada59c1572..1d9e2c74057bb0e86259e1cd510a529f52ae5298 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -32,37 +32,37 @@ Remember that $\UPred(\monoid)$ is isomorphic to $\monoid \monra \SProp$.
 We are thus going to define the assertions as mapping CMRA elements to sets of step-indices.
 
 \begin{align*}
-	\Sem{\vctx \proves t =_\type u : \Prop}_\gamma &\eqdef
-	\Lam \any. \setComp{n}{\Sem{\vctx \proves t : \type}_\gamma \nequiv{n} \Sem{\vctx \proves u : \type}_\gamma} \\
-	\Sem{\vctx \proves \FALSE : \Prop}_\gamma &\eqdef \Lam \any. \emptyset \\
-	\Sem{\vctx \proves \TRUE : \Prop}_\gamma &\eqdef \Lam \any. \nat \\
-	\Sem{\vctx \proves \prop \land \propB : \Prop}_\gamma &\eqdef
-	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cap \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
-	\Sem{\vctx \proves \prop \lor \propB : \Prop}_\gamma &\eqdef
-	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cup \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
-	\Sem{\vctx \proves \prop \Ra \propB : \Prop}_\gamma &\eqdef
+	\Sem{\vctx \proves t =_\type u : \Prop}_\venv &\eqdef
+	\Lam \any. \setComp{n}{\Sem{\vctx \proves t : \type}_\venv \nequiv{n} \Sem{\vctx \proves u : \type}_\venv} \\
+	\Sem{\vctx \proves \FALSE : \Prop}_\venv &\eqdef \Lam \any. \emptyset \\
+	\Sem{\vctx \proves \TRUE : \Prop}_\venv &\eqdef \Lam \any. \nat \\
+	\Sem{\vctx \proves \prop \land \propB : \Prop}_\venv &\eqdef
+	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\venv(\melt) \cap \Sem{\vctx \proves \propB : \Prop}_\venv(\melt) \\
+	\Sem{\vctx \proves \prop \lor \propB : \Prop}_\venv &\eqdef
+	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\venv(\melt) \cup \Sem{\vctx \proves \propB : \Prop}_\venv(\melt) \\
+	\Sem{\vctx \proves \prop \Ra \propB : \Prop}_\venv &\eqdef
 	\Lam \melt. \setComp{n}{\begin{aligned}
             \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land m \in \mval(\meltB) \Ra {} \\
-            & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\
-	\Sem{\vctx \proves \All \var : \type. \prop : \Prop}_\gamma &\eqdef
-	\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
-	\Sem{\vctx \proves \Exists \var : \type. \prop : \Prop}_\gamma &\eqdef
-        \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) }
+            & m \in \Sem{\vctx \proves \prop : \Prop}_\venv(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\venv(\meltB)\end{aligned}}\\
+	\Sem{\vctx \proves \All \var : \type. \prop : \Prop}_\venv &\eqdef
+	\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \venv}(\melt) } \\
+	\Sem{\vctx \proves \Exists \var : \type. \prop : \Prop}_\venv &\eqdef
+        \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \venv}(\melt) }
 \end{align*}
 \begin{align*}
-	\Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB_2)\end{aligned}}
+	\Sem{\vctx \proves \prop * \propB : \Prop}_\venv &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\venv(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\venv(\meltB_2)\end{aligned}}
 \\
-	\Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &\eqdef
+	\Sem{\vctx \proves \prop \wand \propB : \Prop}_\venv &\eqdef
 	\Lam \melt. \setComp{n}{\begin{aligned}
             \All m, \meltB.& m \leq n \land  m \in \mval(\melt\mtimes\meltB) \Ra {} \\
-            & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
-        \Sem{\vctx \proves \ownM{\term} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mincl[n] \meltB}  \\
-        \Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \mval(\Sem{\vctx \proves \term : \textlog{M}}_\gamma) \\
-	\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
-	\Sem{\vctx \proves \plainly{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\munit) \\
-	\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
-        \Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
-            \All m, \melt'. & m \leq n \land m \in \mval(\melt \mtimes \melt') \Ra {}\\& \Exists \meltB. m \in \mval(\meltB \mtimes \melt') \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
+            & m \in \Sem{\vctx \proves \prop : \Prop}_\venv(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\venv(\melt\mtimes\meltB)\end{aligned}} \\
+        \Sem{\vctx \proves \ownM{\term} : \Prop}_\venv &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\venv \mincl[n] \meltB}  \\
+        \Sem{\vctx \proves \mval(\term) : \Prop}_\venv &\eqdef \Lam\any. \mval(\Sem{\vctx \proves \term : \textlog{M}}_\venv) \\
+	\Sem{\vctx \proves \always{\prop} : \Prop}_\venv &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\venv(\mcore\melt) \\
+	\Sem{\vctx \proves \plainly{\prop} : \Prop}_\venv &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\venv(\munit) \\
+	\Sem{\vctx \proves \later{\prop} : \Prop}_\venv &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\venv(\melt)}\\
+        \Sem{\vctx \proves \upd\prop : \Prop}_\venv &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
+            \All m, \melt'. & m \leq n \land m \in \mval(\melt \mtimes \melt') \Ra {}\\& \Exists \meltB. m \in \mval(\meltB \mtimes \melt') \land m \in \Sem{\vctx \proves \prop :\Prop}_\venv(\meltB)
           \end{aligned}
 }
 \end{align*}
@@ -73,29 +73,29 @@ For every definition, we have to show all the side-conditions: The maps have to
 
 \judgment[Interpretation of non-propositional terms]{\Sem{\vctx \proves \term : \type} : \Sem{\vctx} \nfn \Sem{\type}}
 \begin{align*}
-	\Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\
-	\Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \\
-	\Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\gamma &\eqdef
-	\Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\mapinsert \var \termB \gamma} \\
-	\Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef
-	\Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\
-	\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
-	\fixp_{\Sem{\type}}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
+	\Sem{\vctx \proves x : \type}_\venv &\eqdef \venv(x) \\
+	\Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\venv &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\venv, \dots, \Sem{\vctx \proves \term_n : \type_n}_\venv) \\
+	\Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\venv &\eqdef
+	\Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\mapinsert \var \termB \venv} \\
+	\Sem{\vctx \proves \term(\termB) : \type'}_\venv &\eqdef
+	\Sem{\vctx \proves \term : \type \to \type'}_\venv(\Sem{\vctx \proves \termB : \type}_\venv) \\
+	\Sem{\vctx \proves \MU \var:\type. \term : \type}_\venv &\eqdef
+	\fixp_{\Sem{\type}}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \venv}) \\
   ~\\
-	\Sem{\vctx \proves \textlog{abort}\;\term : \type}_\gamma &\eqdef \mathit{abort}_{\Sem\type}(\Sem{\vctx \proves \term:0}_\gamma) \\
-	\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
-	\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\
-	\Sem{\vctx \proves \pi_i\; \term : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\
-        \Sem{\vctx \proves \textlog{inj}_i\;\term : \type_1 + \type_2}_\gamma &\eqdef \mathit{inj}_i(\Sem{\vctx \proves \term : \type_i}_\gamma) \\
-        \Sem{\vctx \proves \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var_1. \term_1 \mid \Ret\textlog{inj}_2\; \var_2. \term_2 \;\textlog{end} : \type }_\gamma &\eqdef 
-    \Sem{\vctx, \var_i:\type_i \proves \term_i : \type}_{\mapinsert{\var_i}\termB \gamma} \\
-    &\qquad \text{where $\Sem{\vctx \proves \term : \type_1 + \type_2}_\gamma = \mathit{inj}_i(\termB)$}
+	\Sem{\vctx \proves \textlog{abort}\;\term : \type}_\venv &\eqdef \mathit{abort}_{\Sem\type}(\Sem{\vctx \proves \term:0}_\venv) \\
+	\Sem{\vctx \proves () : 1}_\venv &\eqdef () \\
+	\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\venv &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\venv, \Sem{\vctx \proves \term_2 : \type_2}_\venv) \\
+	\Sem{\vctx \proves \pi_i\; \term : \type_i}_\venv &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\venv) \\
+        \Sem{\vctx \proves \textlog{inj}_i\;\term : \type_1 + \type_2}_\venv &\eqdef \mathit{inj}_i(\Sem{\vctx \proves \term : \type_i}_\venv) \\
+        \Sem{\vctx \proves \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var_1. \term_1 \mid \Ret\textlog{inj}_2\; \var_2. \term_2 \;\textlog{end} : \type }_\venv &\eqdef 
+    \Sem{\vctx, \var_i:\type_i \proves \term_i : \type}_{\mapinsert{\var_i}\termB \venv} \\
+    &\qquad \text{where $\Sem{\vctx \proves \term : \type_1 + \type_2}_\venv = \mathit{inj}_i(\termB)$}
     \\
   ~\\
-        \Sem{ \melt : \textlog{M} }_\gamma &\eqdef \melt \\
-	\Sem{\vctx \proves \mcore\term : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \term : \textlog{M}}_\gamma} \\
-	\Sem{\vctx \proves \term \mtimes \termB : \textlog{M}}_\gamma &\eqdef
-	\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mtimes \Sem{\vctx \proves \termB : \textlog{M}}_\gamma
+        \Sem{ \melt : \textlog{M} }_\venv &\eqdef \melt \\
+	\Sem{\vctx \proves \mcore\term : \textlog{M}}_\venv &\eqdef \mcore{\Sem{\vctx \proves \term : \textlog{M}}_\venv} \\
+	\Sem{\vctx \proves \term \mtimes \termB : \textlog{M}}_\venv &\eqdef
+	\Sem{\vctx \proves \term : \textlog{M}}_\venv \mtimes \Sem{\vctx \proves \termB : \textlog{M}}_\venv
 \end{align*}
 %
 
@@ -115,10 +115,10 @@ We can now define \emph{semantic} logical entailment.
 \MoveEqLeft
 \forall n \in \nat.\;
 \forall \rs \in \monoid.\; 
-\forall \gamma \in \Sem{\vctx},\;
+\forall \venv \in \Sem{\vctx},\;
 \\&
-n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs)
-\Ra n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs)
+n \in \Sem{\vctx \proves \prop : \Prop}_\venv(\rs)
+\Ra n \in \Sem{\vctx \proves \propB : \Prop}_\venv(\rs)
 \end{aligned}
 \]