From dad4d406f691c7fe11ee326ac68846cfea361f26 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <pietromonticone.cs@gmail.com>
Date: Thu, 7 Sep 2023 13:39:29 +0200
Subject: [PATCH] Update frap_book.tex

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

diff --git a/frap_book.tex b/frap_book.tex
index 59523c4..9a6779d 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -4769,7 +4769,7 @@ More involved and raising new complications is the rule for loops; see the Coq c
 
   Actually, we need to modify our translation judgment so that it also applies to ``silly'' intermediate states of execution in the target language.
   For instance, we wind up with $\skipe$s that are quickly stepped away, yet those configurations must be related to source configurations by $\sim$.
-  Here is one example of the extra rules that we need to add to make our induction hypothsis strong enough.
+  Here is one example of the extra rules that we need to add to make our induction hypothesis strong enough.
   $$\infer{\dscomp{v}{x \leftarrow \mt{Return} \; n; c(x)}{\mt{skip}; s}}{
     v(y) = n
     & \dscomp{v}{c(n)}{s}