A tad better text style

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.