diff --git a/preserves-expressions.md b/preserves-expressions.md
index 997f036..31d390f 100644
--- a/preserves-expressions.md
+++ b/preserves-expressions.md
@@ -100,7 +100,7 @@ We write ⌜*p*⌝ for the encoding into Preserves of a P-expression *p*.
 | ⌜`,`⌝            | = | `<p |,|>`               |
 | ⌜`;`⌝            | = | `<p |;|>`               |
 | ⌜`:` ...⌝        | = | `<p |:` ...`|>`         |
-| ⌜*t*⌝            | = | ⌜*a*⌝ ... `<a>` | where *a* ... are the annotations in *t* and *t* ∈ **Trailer** |
+| ⌜*t*⌝            | = | `@`⌜*a*⌝ ... `<a>` | where `@`*a* ... are the annotations in *t* and *t* ∈ **Trailer** |
 
 The record `<a>` acts as an anchor for the annotations in a `Trailer`.
 
@@ -108,8 +108,10 @@ We overload the ⌜·⌝ notation for encoding whole `Document`s into
 sequences of Preserves values.
 
 {:.pseudocode.equations}
-| ⌜·⌝ : **P-expression Document** | ⟶ | **Preserves Sequence** |
-| ⌜*p* ...⌝                       | = | `[`⌜*p*⌝ ...`]`        |
+| ⌜·⌝ : **P-expression Document** | ⟶ | **Preserves Sequence**                    |
+| ⌜*p* ...⌝                       | = | `[`⌜*p*⌝ ...`]`                           |
+| ⌜*p* ... `@`*a* ...⌝            | = | `[`⌜*p*⌝ ... `@`⌜*a*⌝ ... `<a>]`          |
+|                                 |   | where `@`*a* ... are trailing annotations |
 
 ## <a id="reading-preserves"></a>Interpreting P-expressions as Preserves