diff --git a/theories/finite.v b/theories/finite.v
index c5013d7695120df74278a06a1aad282dd4f6389c..c81b84462340f8b5e1de1eb4b1625a0cbf18f6cd 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -5,6 +5,7 @@ Set Default Proof Using "Type".
 
 Class Finite A `{EqDecision A} := {
   enum : list A;
+  (* [NoDup] makes it easy to define the cardinality of the type. *)
   NoDup_enum : NoDup enum;
   elem_of_enum x : x ∈ enum
 }.