From f8ab8a46c94aec6fa770f4cc422e9fb8319cd8a1 Mon Sep 17 00:00:00 2001
From: 0xd34df00d <0xd34df00d@gmail.com>
Date: Tue, 20 Oct 2020 13:42:17 -0500
Subject: [PATCH] A tad better text style

---
 tex/paper.mng | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tex/paper.mng b/tex/paper.mng
index 87bcfd3d..12143da6 100644
--- a/tex/paper.mng
+++ b/tex/paper.mng
@@ -119,8 +119,8 @@ and we explicitly prove progress and preservation theorems as a sanity check.
 One plausible way to avoid the doubt in type safety of our core language stemming from the presence of the ADTs is to
 encode them via the Boehm-Berarducci encoding \cite{Bohm85}.
 Unfortunately, this does not work in our case,
-as this encoding does not allow expressing the equality between the scrutinee of a pattern match and the patterns in each branch,
-and it seemingly cannot be easily extended to enable this.
+as this encoding does not allow expressing the equality witness between the scrutinee of a pattern match and the patterns in each branch,
+and it seemingly cannot be easily extended to account for this witness.
 
 \paragraph{Subtyping oracle.}
 The refinements in our surface language may contain arbitrary terms, including function application.