diff --git a/GNUmakefile b/GNUmakefile
new file mode 100644
index 0000000000000000000000000000000000000000..16c1e0cd033b982e9a75280996246d5c2d55b537
--- /dev/null
+++ b/GNUmakefile
@@ -0,0 +1,2 @@
+tests:
+	lambdapi prelude/core/prelude.lp
diff --git a/prelude/cert_f/booleans.lp b/prelude/cert_f/booleans.lp
index 68f2df936144ae52ecbfd969be2778252ef8a498..1ea9b8c59546b161cd012bd631df6c327dff99ec 100644
--- a/prelude/cert_f/booleans.lp
+++ b/prelude/cert_f/booleans.lp
@@ -1,7 +1,7 @@
-require open encodings.cf
+require open encodings.cert_f
 
 definition bool ≔ Prop
 definition false ≔ @prod Type Prop uProp (λ x : Term uProp, x)
 definition true ≔ Term false ⇒ Term false
 
-definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ x, false)
+definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)
diff --git a/prelude/cert_f/equalities.lp b/prelude/cert_f/equalities.lp
index 8d0f8f28087929b45e07e5b1d91f32db320468f1..83456f64a2bb9938a99af0f4b9094ffe0c0bdee9 100644
--- a/prelude/cert_f/equalities.lp
+++ b/prelude/cert_f/equalities.lp
@@ -1,3 +1,3 @@
-require open encodings.cf prelude.cf.booleans
+require open encodings.cert_f prelude.cert_f.booleans
 
 symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term uProp
diff --git a/prelude/cert_f/int.lp b/prelude/cert_f/int.lp
index 7c07f856fb841d6b1bdc1dfb776a5a7a6f13bce5..23588971dc0a17c4ee28fca1f5904b7652025d4c 100644
--- a/prelude/cert_f/int.lp
+++ b/prelude/cert_f/int.lp
@@ -1,4 +1,4 @@
-require open encodings.cf prelude.cf.booleans prelude.cf.notequal
+require open encodings.cert_f prelude.cert_f.booleans prelude.cert_f.notequal
 
 constant symbol integer : Term uType
 definition int ≔ integer
diff --git a/prelude/cert_f/naturalnumbers.lp b/prelude/cert_f/naturalnumbers.lp
index 41e63179ce3b5bada5707ea3839d95f5e467b75f..0cdbea3d0c7241a5d7ad258ea398677645a6cda4 100644
--- a/prelude/cert_f/naturalnumbers.lp
+++ b/prelude/cert_f/naturalnumbers.lp
@@ -1,4 +1,4 @@
-require open encodings.cf prelude.cf.booleans
+require open encodings.cert_f prelude.cert_f.booleans
 
 constant symbol nat : Term uType
 constant symbol zero : Term nat
diff --git a/prelude/cert_f/notequal.lp b/prelude/cert_f/notequal.lp
index f2a759cdcf50c445b45d9763eccffa1adb72d9c5..3ad95f32339036c54622ec32e3b5a61334ddfef5 100644
--- a/prelude/cert_f/notequal.lp
+++ b/prelude/cert_f/notequal.lp
@@ -1,3 +1,3 @@
-require open encodings.cf prelude.cf.booleans prelude.cf.equalities
+require open encodings.cert_f prelude.cert_f.booleans prelude.cert_f.equalities
 
 definition neq {T: Term uType} (x y: Term T) ≔ bnot (eq x y)
diff --git a/prelude/core/prelude.lp b/prelude/core/prelude.lp
index 273a0ac42e859cdf810822499d133dae1fd50415..39bb6dbe66c20e695d363bc1e15a98d3135848c3 100644
--- a/prelude/core/prelude.lp
+++ b/prelude/core/prelude.lp
@@ -1,2 +1,2 @@
-require open pvs_core prelude.booleans prelude.equalities prelude.notequal
-require open prelude.if_def
+require encodings.pvs_core prelude.core.booleans prelude.core.equalities
+prelude.core.notequal prelude.core.if_def