From 8a87c209f7601f3969356dd9f85764265e7c3fb3 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Tue, 5 May 2020 19:26:59 -0400
Subject: [PATCH] Revising before class

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

diff --git a/frap_book.tex b/frap_book.tex
index 989abaf..ecb12fc 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -5416,7 +5416,7 @@ Here is a sketch of the key lemmas.
 
 \begin{lemma}\label{preserve_unused}
   Assume that $\vec{\alpha}$ is a duplicate-free list of parties excluding both sender and receiver of channel $c$.
-  If $\mptys{p}{\vec{\alpha}}{\; \send{c}{x : \sigma}{\tau(x)}}$, then for any $v : \sigma$, we have $\mptys{p'}{\vec{\alpha}}{\tau(v)}$.
+  If $\mptys{p}{\vec{\alpha}}{\; \send{c}{x : \sigma}{\tau(x)}}$, then for any $v : \sigma$, we have $\mptys{p}{\vec{\alpha}}{\tau(v)}$.
   In other words, when we have well-typed code for a set of parties that do not participate in the first step of a protocol, that code remains well-typed when we advance to the next protocol step.
 \end{lemma}
 \begin{proof}