diff --git a/edit_distance_l1_matching_v2.txt b/edit_distance_l1_matching_v2.txt
index 7e12b54..ffbd524 100644
--- a/edit_distance_l1_matching_v2.txt
+++ b/edit_distance_l1_matching_v2.txt
@@ -1,8 +1,8 @@
 EDIT DISTANCE IN l1: MATCHING BOUNDS UP TO CONSTANTS IN THE EXPONENT
 
-This is a complete, self-contained proof of the main theorem below. It is
-written for a reader who knows sets, functions, and finite sums. Every
-symbol is defined before it is used.
+This is a complete proof of the main theorem below, up to one stated
+external embedding theorem. It is written for a reader who knows sets,
+functions, and finite sums. Every symbol is defined before it is used.
 
 ===============================================================================
 1. WHAT IS BEING PROVED
@@ -13,13 +13,13 @@ from Sigma. The length of x is written |x|. The empty string is eps.
 
 Two distances are used.
 
-ED(x,y) is the usual edit distance: the least number of single-letter
-insertions, deletions, and substitutions that turn x into y. Every
-operation costs one.
+ED(x,y) is the usual edit distance: the least number of
+single-letter insertions, deletions, and substitutions that turn x into y.
+Every operation costs one.
 
 Delta(x,y) is the insertion-deletion distance: the least number of
-single-letter insertions and deletions that turn x into y. Substitutions are not
-allowed.
+single-letter insertions and deletions that turn x into y.
+Substitutions are not allowed.
 
 Write l1 for the real vector space of absolutely summable sequences, with
 norm