diff --git a/prelude/nat.lp b/adlib/core/nat.lp
similarity index 77%
rename from prelude/nat.lp
rename to adlib/core/nat.lp
index 0306c9d655b0e62910c27315bfe830cc69cddca5..11b1f7ee4e5d2c41d2b849a77ec1b640c58826fc 100644
--- a/prelude/nat.lp
+++ b/adlib/core/nat.lp
@@ -1,4 +1,4 @@
-require open pvs_core prelude.notequal
+require open encodings.pvs_core prelude.core.notequal
 // Not part of prelude as integers are built in pvs
 
 constant symbol int : Type
diff --git a/prelude/nat_ops.lp b/adlib/core/nat_ops.lp
similarity index 76%
rename from prelude/nat_ops.lp
rename to adlib/core/nat_ops.lp
index bdbaa559000c42dcc0fa73305bfd44febac82a3d..b06f59913ed05a41de18b872f740425a1e8351f9 100644
--- a/prelude/nat_ops.lp
+++ b/adlib/core/nat_ops.lp
@@ -1,4 +1,5 @@
-require open pvs_core prelude.notequal prelude.nat prelude.equalities
+require open encodings.pvs_core prelude.core.notequal adlib.core.nat
+prelude.core.equalities
 
 symbol times : eta int ⇒ eta int ⇒ eta int
 rule times &n 1  → &n
diff --git a/encodings/cf.lp b/encodings/cert_f.lp
similarity index 83%
rename from encodings/cf.lp
rename to encodings/cert_f.lp
index 1770eea0651bc17910188e36e660d0c6ff56e7da..bde178ad280c849a32f509e1daf83c324e2e9d12 100644
--- a/encodings/cf.lp
+++ b/encodings/cert_f.lp
@@ -31,7 +31,7 @@ rule Term uProp → Univ Prop
 symbol prod {s1 s2 : Sort} (A : Univ s1) :
   (Term A ⇒ Univ s2) ⇒ Univ (Rule s1 s2)
 
-rule Term (prod &s1 &s2 &A &B) → ∀ x : Term &A, Term (&B x)
+rule Term (prod &A &B) → ∀ x : Term &A, Term (&B x)
 
 // Predicate subtyping
 // can be seen as a dependant pair type with
@@ -42,21 +42,21 @@ symbol psub (A : Univ Type) : (Term A ⇒ Univ Prop) ⇒ Univ Type
 // Γ ⊢ M : { v : T | U }
 // —————————————————————PROJl
 //      Γ ⊢ fst(M) : T
-symbol fst {T : Univ Type} {U : Term T ⇒ Univ Prop}: Term (psub T U) ⇒ Term T
+symbol fst {T : Univ Type} (U : Term T ⇒ Univ Prop): Term (psub T U) ⇒ Term T
 
 //  Γ ⊢ M : { v : T | U }
 // ——————————————————————————PROJr
 // Γ ⊢ snd(M) : U[v ≔ fst(M)]
-symbol snd (T: Univ Type) (U: Term T ⇒ Univ Prop) (M: Term (psub T U)):
-  Term (U (@fst T U M))
+symbol snd {T: Univ Type} (U: Term T ⇒ Univ Prop) (M: Term (psub T U)):
+  Term (U (fst U M))
 
 // An inhabitant of a predicate subtype, that is, a pair of
 // an element and the proof that it satisfies the predicate
 // Γ ⊢ M : T    Γ ⊢ N : U[v ≔ M]    Γ ⊢ { v : T | U }
 // ——————————————————————————————————————————————————PAIR
 //           Γ ⊢ ⟨M, N⟩ : {v : T | U}
-symbol pair {T: Univ Type} (U: @Term Type T ⇒ Univ Prop) (M: @Term Type T):
+symbol pair {T: Univ Type} (U: Term T ⇒ Univ Prop) (M: Term T):
   Term (U M) ⇒ Term (psub T U)
 
-rule @fst &T &U (@pair &T &U &M _) → &M
-rule @snd &T &U (@pair &T &U _ &P) → &P
+rule fst &U (pair &U &M _) → &M
+rule snd &U (pair &U _ &P) → &P
diff --git a/prelude/cf/booleans.lp b/prelude/cert_f/booleans.lp
similarity index 69%
rename from prelude/cf/booleans.lp
rename to prelude/cert_f/booleans.lp
index e0e80b63d6deac733fe015426f353e632f330ce8..68f2df936144ae52ecbfd969be2778252ef8a498 100644
--- a/prelude/cf/booleans.lp
+++ b/prelude/cert_f/booleans.lp
@@ -1,7 +1,7 @@
 require open encodings.cf
 
 definition bool ≔ Prop
-definition false ≔ @prod Type Prop uProp (λ x : @Term Type uProp, x)
+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)
diff --git a/prelude/cf/equalities.lp b/prelude/cert_f/equalities.lp
similarity index 100%
rename from prelude/cf/equalities.lp
rename to prelude/cert_f/equalities.lp
diff --git a/prelude/cf/int.lp b/prelude/cert_f/int.lp
similarity index 100%
rename from prelude/cf/int.lp
rename to prelude/cert_f/int.lp
diff --git a/prelude/cf/naturalnumbers.lp b/prelude/cert_f/naturalnumbers.lp
similarity index 100%
rename from prelude/cf/naturalnumbers.lp
rename to prelude/cert_f/naturalnumbers.lp
diff --git a/prelude/cf/notequal.lp b/prelude/cert_f/notequal.lp
similarity index 100%
rename from prelude/cf/notequal.lp
rename to prelude/cert_f/notequal.lp
diff --git a/prelude/boolean_props.lp b/prelude/core/boolean_props.lp
similarity index 72%
rename from prelude/boolean_props.lp
rename to prelude/core/boolean_props.lp
index 120c1434c5ba17154ea056a22ef9daf4be5d6b12..aca40ad983be075a031d70a776336e18883a1e58 100644
--- a/prelude/boolean_props.lp
+++ b/prelude/core/boolean_props.lp
@@ -1,4 +1,5 @@
-require open pvs_core prelude.booleans prelude.equalities prelude.if_def
+require open encodings.pvs_core
+prelude.core.booleans prelude.core.equalities prelude.core.if_def
 
 // true /= false
 symbol bool_inclusive : eps (bnot (eq bool false true))
diff --git a/prelude/booleans.lp b/prelude/core/booleans.lp
similarity index 94%
rename from prelude/booleans.lp
rename to prelude/core/booleans.lp
index 3fee8c957b565c94bb411768c85dea427a094087..e0ef4aa46dccad44cc584e46b371faad3517483e 100644
--- a/prelude/booleans.lp
+++ b/prelude/core/booleans.lp
@@ -1,4 +1,4 @@
-require open pvs_core
+require open encodings.pvs_core
 
 set builtin "T" ≔ eta
 set builtin "P" ≔ eps
diff --git a/prelude/core/equalities.lp b/prelude/core/equalities.lp
new file mode 100644
index 0000000000000000000000000000000000000000..863cc7dce0afcc8df18bec9a0fd9cb5d44f431c1
--- /dev/null
+++ b/prelude/core/equalities.lp
@@ -0,0 +1,3 @@
+require open encodings.pvs_core prelude.core.booleans
+
+symbol eq {T : Type} : eta T ⇒ eta T ⇒ eta bool
diff --git a/prelude/core/if_def.lp b/prelude/core/if_def.lp
new file mode 100644
index 0000000000000000000000000000000000000000..ede0300ca27cb9c1ee51748f932eb3b54ac0a043
--- /dev/null
+++ b/prelude/core/if_def.lp
@@ -0,0 +1,4 @@
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
+prelude.core.notequal
+
+symbol if (T:Type): eta bool ⇒ eta T ⇒ eta T ⇒ eta T
diff --git a/prelude/core/notequal.lp b/prelude/core/notequal.lp
new file mode 100644
index 0000000000000000000000000000000000000000..12486613b60e70426ce0adc5b53667c93f7241e2
--- /dev/null
+++ b/prelude/core/notequal.lp
@@ -0,0 +1,3 @@
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
+
+definition neq {T: Type} (x: eta T) (y: eta T) ≔ bnot (eq x y)
diff --git a/prelude/prelude.lp b/prelude/core/prelude.lp
similarity index 100%
rename from prelude/prelude.lp
rename to prelude/core/prelude.lp
diff --git a/prelude/pvs_core.lp b/prelude/core/pvs_core.lp
similarity index 100%
rename from prelude/pvs_core.lp
rename to prelude/core/pvs_core.lp
diff --git a/prelude/quantifier_props.lp b/prelude/core/quantifier_props.lp
similarity index 83%
rename from prelude/quantifier_props.lp
rename to prelude/core/quantifier_props.lp
index 5cf168aee881a02b80d0f2100baf843e54d53beb..85c51a98053768f539a2b94dc84866624e1436cb 100644
--- a/prelude/quantifier_props.lp
+++ b/prelude/core/quantifier_props.lp
@@ -1,4 +1,4 @@
-require open pvs_core prelude.booleans prelude.equalities
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
 
 definition exists (T: Type) (p : eta T ⇒ eta bool) ≔
     (bnot (all T (λ x, (bnot (p x)))))
diff --git a/prelude/core/xor_def.lp b/prelude/core/xor_def.lp
new file mode 100644
index 0000000000000000000000000000000000000000..0ef531873c82059e3fd56cbb0a8fa782added8ce
--- /dev/null
+++ b/prelude/core/xor_def.lp
@@ -0,0 +1,3 @@
+require open encodings.pvs_core prelude.core.booleans prelude.core.notequal
+
+definition xor (A : eta bool) (B : eta bool) ≔ neq bool A B
diff --git a/prelude/equalities.lp b/prelude/equalities.lp
deleted file mode 100644
index 9ad3b3fbf6691f353eaf9ba1cf44561d815dc9ba..0000000000000000000000000000000000000000
--- a/prelude/equalities.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-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
deleted file mode 100644
index 9e6b18b697ba62f6195fee143dbc1dfdd4a9487b..0000000000000000000000000000000000000000
--- a/prelude/if_def.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-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
deleted file mode 100644
index abf4f864b109469770e8da79e808b93a947b68a4..0000000000000000000000000000000000000000
--- a/prelude/notequal.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open pvs_core prelude.booleans prelude.equalities
-
-definition neq {T: Type} (x: eta T) (y: eta T) ≔ bnot (eq x y)
diff --git a/prelude/xor_def.lp b/prelude/xor_def.lp
deleted file mode 100644
index 449e701d83e580864340390f0949d4386738a146..0000000000000000000000000000000000000000
--- a/prelude/xor_def.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open pvs_core prelude.booleans prelude.notequal
-
-definition xor (A : eta bool) (B : eta bool) ≔ neq bool A B
diff --git a/prelude/rat_exp.lp b/sandbox/core/rat.lp
similarity index 100%
rename from prelude/rat_exp.lp
rename to sandbox/core/rat.lp
diff --git a/prelude/rat.lp b/sandbox/core/rat_explicit.lp
similarity index 83%
rename from prelude/rat.lp
rename to sandbox/core/rat_explicit.lp
index 5afd078fde0708c487f898e5164e2dc9c861ea14..4a03b1df40283a31ef4b2804c8e6b5f55d01c53c 100644
--- a/prelude/rat.lp
+++ b/sandbox/core/rat_explicit.lp
@@ -1,6 +1,6 @@
-require open pvs_core prelude.booleans prelude.equalities prelude.notequal
-prelude.nat
-require prelude.nat_ops as N
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
+prelude.core.notequal adlib.core.nat
+require adlib.core.nat_ops as N
 
 constant symbol rat : Type
 constant symbol zero : η rat