diff --git a/theories/ZornsLemma/FiniteTypes.v b/theories/ZornsLemma/FiniteTypes.v
index c946590c..a634a6c8 100644
--- a/theories/ZornsLemma/FiniteTypes.v
+++ b/theories/ZornsLemma/FiniteTypes.v
@@ -6,7 +6,9 @@ From Coq Require Import
   Lia
   Program.Subset.
 From ZornsLemma Require Import
-  Cardinals
+  Cardinals.Cardinals
+  Cardinals.Combinatorics
+  Cardinals.CSB
   DecidableDec
   FiniteImplicit
   Finite_sets