diff --git a/ProofMode.md b/ProofMode.md
index 8bc2bf2dd40fb5bd8a2b0c83e90e1fafd814ab24..0ca7b0b55af7098f71f2f8235464f1b115295aff 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -121,6 +121,11 @@ Modalities
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.
 
+The persistence modality
+------------------------
+
+- `iAlways` is a synonym for `iIntros "!#"`.
+
 The later modality
 ------------------