diff --git a/prelude/boolean_props.lp b/prelude/boolean_props.lp
index eb9c4752a2ab2c5efb2a23480d0b0edf7ab5a645..57badd6d409c6a4a89f5767ede01ce1d0587f58e 100644
--- a/prelude/boolean_props.lp
+++ b/prelude/boolean_props.lp
@@ -1,4 +1,4 @@
-require open pvs_core booleans equalities if_def
+require open pvs_core prelude.booleans prelude.equalities prelude.if_def
 
 // true /= false
 symbol bool_inclusive : eps (bnot (eq bool false true))
diff --git a/prelude/equalities.lp b/prelude/equalities.lp
index aca1ad211e8971d256375d239d5cd554116422c2..d3bbfcdd52e2e3af6b89eb448901f8584e30a337 100644
--- a/prelude/equalities.lp
+++ b/prelude/equalities.lp
@@ -1,3 +1,3 @@
-require open pvs_core booleans
+require open pvs_core prelude.booleans
 
 symbol eq : ∀ T : Type, eta T ⇒ eta T ⇒ eta bool
diff --git a/prelude/if_def.lp b/prelude/if_def.lp
index 1b8fe2854dbc6ecc9aa45965dfe47783e20b475a..9e6b18b697ba62f6195fee143dbc1dfdd4a9487b 100644
--- a/prelude/if_def.lp
+++ b/prelude/if_def.lp
@@ -1,3 +1,3 @@
-require open pvs_core booleans equalities notequal
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
 
 symbol if (T:Type): eta bool ⇒ eta T ⇒ eta T ⇒ eta T
diff --git a/prelude/notequal.lp b/prelude/notequal.lp
index 475dec76c24c12598b0b8e042caa86fb0a7e130c..194b60233653069c766f9f18c2ceff5a43303e4c 100644
--- a/prelude/notequal.lp
+++ b/prelude/notequal.lp
@@ -1,3 +1,3 @@
-require open pvs_core booleans equalities
+require open pvs_core prelude.booleans prelude.equalities
 
 definition neq (T: Type) (x: eta T) (y: eta T) ≔ bnot (eq T x y)
diff --git a/prelude/prelude.lp b/prelude/prelude.lp
index 0b0dec0abcb83b9e03ed2cb515c896fc3304b9fc..273a0ac42e859cdf810822499d133dae1fd50415 100644
--- a/prelude/prelude.lp
+++ b/prelude/prelude.lp
@@ -1 +1,2 @@
-require open pvs_core booleans equalities notequal if_def
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
+require open prelude.if_def
diff --git a/prelude/rat.lp b/prelude/rat.lp
index 99e289438cca5356c357026e73f13a371aa732c1..b2596c393eacc4217e658ce5f5029a8daccf77ba 100644
--- a/prelude/rat.lp
+++ b/prelude/rat.lp
@@ -1,4 +1,4 @@
-require open pvs_core booleans equalities notequal
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
 
 constant symbol rat : Type
 constant symbol zero : eta rat