Fix 224--227.

1 files changed, 4 insertions, 4 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index b848db6..cec4344 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -280,10 +280,10 @@ specified eliminators too; simply take the corresponding projection from the
 product.
 
 Another benefit of eliminator encodings are that the constructors are
-extensible. As no information about exactly which constructor was used remains
-in the encoded type, we are free to add some interesting constructors. For
-example, we can add the constructor \(\mathsf{double}\) that doubles the value
-of each leaf:
+extensible. The encoded type contains no information about which
+constructor was used to construct a value. Thus we are free to add new
+constructors. For example, we can add the constructor
+\(\mathsf{double}\) that doubles the value of each leaf:
 \[
 \mathsf{double}(x) \coloneq \tuple{2 \cdot x.0, x.1}
 \]