diff --git a/FiniteSets/FSets.v b/FiniteSets/FSets.v
index c7d000a..6c66da7 100644
--- a/FiniteSets/FSets.v
+++ b/FiniteSets/FSets.v
@@ -1,2 +1,2 @@
 Require Export HoTT HitTactics.
-Require Export kuratowski_sets kuratowski.operations kuratowski.properties extensionality.
\ No newline at end of file
+Require Export kuratowski_sets kuratowski.operations kuratowski.properties extensionality prelude.