diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex
index 4daf0d0..07dca76 100644
--- a/chapters/3_rewriting.tex
+++ b/chapters/3_rewriting.tex
@@ -420,7 +420,7 @@ suitable alpha renaming.
 \centering
 \begin{prooftree}
   \hypo{\texttt{function} ~t\texttt{:}~\ptinline{F(\(p_1, \ldots{}, p_k\)) = E;} \in{} \Prog{} \text{~where the~} p_i \text{~are fresh}}
-  \infer[no rule]1{\Sem{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env}} \Rightarrow{} \tuple{v, \Env'}
+  \infer[no rule]1{\Sem{\(\ptinline{E}_{[p_i \mapsto a_i, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
   \infer1[(Call)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{} \tuple{v, \Env'}}
 \end{prooftree} \\
 \bigskip
@@ -431,8 +431,8 @@ suitable alpha renaming.
 \bigskip
 \begin{prooftree}
   \hypo{\texttt{predicate}~\ptinline{F(\(p_1, \ldots, p_k\));} \in \Prog}
-  \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env_0} \Rightarrow{}
-    \tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env_k}}}
+  \infer1[(CallPredicate)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
+    \tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
 \end{prooftree}
 \caption{\label{fig:4-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
   of \microzinc\ calls to \nanozinc.}
@@ -515,17 +515,10 @@ notation.
 
 \begin{figure*}
 \centering
-% \begin{prooftree}
-%   \hypo{x \in \langle \text{ident} \rangle}
-%   \hypo{v \in \langle \text{literal} \rangle}
-%   \infer2[(IdC)]{\Sem{\(x\)}{\Prog, \{x \mapsto\ v \sep\ []\} \cup\ \Env} \Rightarrow \tuple{v, \{x \mapsto v \sep [] \} \cup \Env}}
-% \end{prooftree} \\
-% \bigskip
 \begin{prooftree}
   \hypo{x \in \langle \text{ident} \rangle}
-  \hypo{v}
-  \hypo{\phi \text{~otherwise}}
-  \infer3[(IdX)]{\Sem{\(x\)}{\Prog, \{t: x^{\texttt{~└──~}} \phi\ \} \cup\ \Env} \Rightarrow{} \tuple{x, \{t: x^{\texttt{~└──~}} \phi{} \cup{} \Env}}
+  \hypo{\{t: x_{\texttt{~└──~}} \phi\ \} \in \Env}
+  \infer2[(IdX)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}}
 \end{prooftree} \\
 \bigskip
 \begin{prooftree}