diff --git a/preserves.md b/preserves.md
index 1936975..8646805 100644
--- a/preserves.md
+++ b/preserves.md
@@ -104,8 +104,8 @@ the `totalOrder` predicate defined in section 5.10 of [IEEE Std
 
 A `Record` is a *labelled* tuple of `Value`s, the record's *fields*. A
 label can be any `Value`, but is usually a `Symbol`.[^extensibility]
-[^iri-labels] `Record`s are compared lexicographically: first by
-label, then by field sequence.
+[^iri-labels] `Record`s are ordered first by label, then
+lexicographically[^lexicographical-sequences] by field sequence.
 
   [^extensibility]: The [Racket](https://racket-lang.org/) programming
     language defines
@@ -123,10 +123,25 @@ label, then by field sequence.
     it cannot be read as an IRI at all, and so the label simply stands
     for itself—for its own `Value`.
 
+  [^lexicographical-sequences]: When comparing sequences of values for
+    the total order, [lexicographical
+    ordering](https://en.wikipedia.org/wiki/Lexicographic_order) is
+    used. Elements are drawn pairwise from the two sequences to be
+    compared. If one is smaller than the other according to the total
+    order, the sequence it was drawn from is the smaller of the
+    sequences. If the end of one sequence is reached, while the other
+    sequence has elements remaining, the shorter sequence is considered
+    smaller. Otherwise, all the elements compared equal and neither was
+    longer than the other, so they compare equal. For example,
+      - `[#f]` is ordered before `[foo]` because `Boolean` appears before `Symbol` in the kind ordering;
+      - `[x]` before `[x y]` because there is no element remaining to compare against `y`;
+      - `[a b]` before `[x]` because `a` is smaller than `x`; and
+      - `[x y]` before `[x z]` because `y` is ordered before `z` according to the ordering rules for `Symbol`.
+
 ### Sequences.
 
 A `Sequence` is a sequence of `Value`s. `Sequence`s are compared
-lexicographically.
+lexicographically.[^lexicographical-sequences]
 
 ### Sets.
 
@@ -134,15 +149,16 @@ A `Set` is an unordered finite set of `Value`s. It contains no
 duplicate values, following the [equivalence relation](#equivalence)
 induced by the total order on `Value`s. Two `Set`s are compared by
 sorting their elements ascending using the [total order](#total-order)
-and comparing the resulting `Sequence`s.
+and comparing the resulting `Sequence`s.[^lexicographical-sequences]
 
 ### Dictionaries.
 
 A `Dictionary` is an unordered finite collection of pairs of `Value`s.
 Each pair comprises a *key* and a *value*. Keys in a `Dictionary` are
 pairwise distinct. Instances of `Dictionary` are compared by
-lexicographic comparison of the sequences resulting from ordering each
-`Dictionary`'s pairs in ascending order by key.
+lexicographic[^lexicographical-sequences] comparison of the sequences
+resulting from ordering each `Dictionary`'s pairs in ascending order by
+key.
 
 ### Embeddeds.
 
@@ -194,8 +210,12 @@ sequences use [the Preserves binary encoding](preserves-binary.html).
 
 The total ordering specified [above](#total-order) means that the following statements are true:
 
-    "bzz" < "c" < "caa" < #!"a"
-    #t < 3.0f < 3.0 < 3 < "3" < |3| < [] < #!#t
+ - `"bzz"` &lt; `"c"` &lt; `"caa"` &lt; `#!"a"`
+ - `#t` &lt; `3.0f` &lt; `3.0` &lt; `3` &lt; `"3"` &lt; `|3|` &lt; `[]` &lt; `#!#t`
+ - `[#f]` &lt; `[foo]`, because `Boolean` appears before `Symbol` in the kind ordering
+ - `[x]` &lt; `[x y]`, because there is no element remaining to compare against `y`
+ - `[a b]` &lt; `[x]`, because `a` is smaller than `x`
+ - `[x y]` &lt; `[x z]`, because `y` is ordered before `z`
 
 ### Simple examples.