Add missing variable in proof

1 files changed, 1 insertions, 1 deletions

diff --git a/proof.tex b/proof.tex
index 5caa382..9a192c6 100644
--- a/proof.tex
+++ b/proof.tex
@@ -171,7 +171,7 @@ The other invariants and assumptions for defining two matching states in HTL are
   Given an HTL program, the forward simulation relation should hold after inserting the RAM and wiring the load, store and control signals.
 
   \begin{align*}
-    \forall h, B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
+    \forall h, h', B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
   \end{align*}
 \end{lemma}