diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 716350954749deccb5a6c1b56a459221fc07f4ab..facbfd82b6b3528f68667dd184728e74ea1cc1c8 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -984,6 +984,10 @@ Proof.
 Qed.
 
 (** Later *)
+(** Note that the projection [later_car] is not non-expansive (see also the
+lemma [later_car_anti_contractive] below), so it cannot be used in the logic.
+If you need to get a witness out, you should use the lemma [Next_uninj]
+instead. *)
 Record later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.