diff --git a/paper/paper.md b/paper/paper.md
index 1380d7b0da..6ae4250774 100644
--- a/paper/paper.md
+++ b/paper/paper.md
@@ -55,7 +55,7 @@ First, like other theorem provers, the Agda language provides only a minimal cor
 As a result, many concepts traditionally considered part of a language must be defined within the program itself.
 This approach reduces compiler complexity and enhances its reliability, and also shows the strength of the core language
 itself as it can indeed push these concepts out to the library.
-For example, in a fresh Agda environment, there is no predefined notion of an integer, let alone more complex data structures such as arrays or maps. Thus the crucial need for a standard library.
+For example, in a fresh Agda environment, there is no predefined notion of an integer, let alone more complex data structures such as arrays, length-indexed vectors or maps. Thus the crucial need for a standard library.
 
 Second, Agda users often seek to prove that programs constructed using data types from the standard library are "correct." 
 Therefore, the standard library needs to provide all the necessary building blocks: not just operations for these data types but also proofs of their basic properties (e.g., that integer addition is commutative or string concatenation is associative). Starting from just the language, something as simple as defining a string-reversing function and proving that it preserves the length of the string would require hundreds of lines of code.
@@ -96,6 +96,7 @@ On the other hand, like `agda-stdlib`, MathLib [@van2020maintaining] for Lean ai
 A second challenge is that Agda was the first major ITP to fully embrace dependently-typed programming as the default (so that, e.g. a `reverse` function can be *statically checked* to be length-preserving).
 With the exception of Idris, a more recent entrant to the field [@brady2013idris], other major theorem provers either do not support dependent types or encourage spare usage.
 In contrast, nearly everything in `agda-stdlib` makes use of dependent types, with correctness-related invariants being closely integrated with definitions.
+For example, we can specify that `reverse` defined on length-indexed vectors is length-preserving *by virtue of its type*.
 Furthermore most proofs consist of evidence-bearing terms for the relevant types, rather than being "irrelevant".
 As a result, the library provides relatively sophisticated features like polymorphic n-ary functions [@allais2019generic], regular expressions which provide proof of membership when compiled and applied, and proof-carrying `All` and `Any` predicates for containers [citation?].
 While this provides powerful tools for users, learning how to design such a large-scale, dependently-typed library is an ongoing journey. The Agda standard library is the first such to tackle this challenge.