diff --git a/algebra/upred.v b/algebra/upred.v
index 0477b715c0215a942afe65f33f663bc6c17b9479..306906368165bc7ad6313ad46f908e682621504a 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -301,6 +301,8 @@ Infix "↔" := uPred_iff : uPred_scope.
 
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
 Arguments timelessP {_} _ {_}.
+(* TODO: Derek suggested to call such assertions "persistent", which we now
+   do in the paper. *)
 Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
 Arguments always_stable {_} _ {_}.