diff --git a/FiniteSets/representations/T.v b/FiniteSets/representations/T.v
index c27ebb2..f99ef53 100644
--- a/FiniteSets/representations/T.v
+++ b/FiniteSets/representations/T.v
@@ -73,8 +73,6 @@ Module Export T.
 
 End T.
 
-Check T.
-
 Section merely_dec_lem.
   Variable A : hProp.
   Context `{Univalence}.