A comment that `agree_car` is not non-expansive.

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