diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 7d200730edb51bd87f531dcec455fc6c5d80fc25..f4325de40f28ea8ae809854b00e21c17c6d75355 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -49,6 +49,10 @@ Section cell.
   Lemma cell_proper' E L ty1 ty2 : eqtype E L ty1 ty2 → eqtype E L (cell ty1) (cell ty2).
   Proof. eapply cell_proper. Qed.
 
+  (* The real [Cell] in Rust is never [Copy], but that is mostly for reasons of
+     ergonomics -- it is widely agreed that it would be sound for [Cell] to be
+     [Copy]. [Cell] is also rather unique as an interior mutable [Copy] type, so
+     proving this is a good benchmark. *)
   Global Instance cell_copy ty :
     Copy ty → Copy (cell ty).
   Proof.