From 84791f343ff42d7cd69c177b8fb1bab282dc0216 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Wed, 12 Oct 2016 13:24:52 -0400
Subject: [PATCH] Typo fix (issue #14)

---
 frap_book.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/frap_book.tex b/frap_book.tex
index 0ae35f3..9f0a1d7 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -2779,7 +2779,7 @@ These rules together are \emph{complete}\index{completeness of Hoare logic}, in
 Here we only go into detail on a proof of the dual property, \emph{soundness}\index{soundness of Hoare logic}.
 
 \begin{lemma}\label{hoare_while}
-  Assume the following fact: Together, $\bigstep{(h, v, c)}{(h', v')}$, $I(h, v)$, and $\denote{b}(h, s)$ imply $I(h', v')$.
+  Assume the following fact: Together, $\bigstep{(h, v, c)}{(h', v')}$, $I(h, v)$, and $\denote{b}(h, v)$ imply $I(h', v')$.
   Then, given $\bigstep{(h, v, \{I\} \while{b}{c})}{(h', v')}$, it follows that $I(h', v')$ and $\neg \denote{b}(h', v')$.
 \end{lemma}
 \begin{proof}