diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 355f976b32531c3f07579131c4f7c645e23f41f7..ad8dc5a553afd649a2abd6624fad1373b68e2762 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -26,6 +26,9 @@ Proof.
   Thus Ag(T) is not necessarily complete.
 *)
 
+(** Note that the projection [agree_car] is not non-expansive, so it cannot be
+used in the logic. If you need to get a witness out, you should use the
+lemma [to_agree_uninjN] instead. *)
 Record agree (A : Type) : Type := {
   agree_car : list A;
   agree_not_nil : bool_decide (agree_car = []) = false