diff --git a/README.md b/README.md
index 6fa3d645d156abe931d9a74e0fd73376c6af2a6b..61186d6902cfb4d76a84625ca30685d0069570e1 100644
--- a/README.md
+++ b/README.md
@@ -23,9 +23,7 @@ library, also known as _Prelude_. The prelude is available
 - `prelude` contains parts of the PVS prelude
 - `sandbox` contains miscellaneous experiments
 - `tools` contains some additional scripts and utilities
-
-Each directory contains a directory per encoding, so the logic file for the
-prelude encoded with `cert_f` is under `prelude/cert_f/logic.lp`.
+- `alternativs` contains files in other encodings
 
 ## Emacs abbreviations
 The `.dir-locals.el` activates the `abbrev-mode` when opening a Dedukti file,
diff --git a/adlib/cert_f/bootstrap.lp b/adlib/bootstrap.lp
similarity index 95%
rename from adlib/cert_f/bootstrap.lp
rename to adlib/bootstrap.lp
index 698dfa8d8f23a8269ee1bd524e17c5697a8839e4..c0cef1a09d91e93833419f70621c8d65418b6403 100644
--- a/adlib/cert_f/bootstrap.lp
+++ b/adlib/bootstrap.lp
@@ -1,4 +1,4 @@
-require open encodings.cert_f
+require open personoj.encodings.cert_f
 
 definition bool ≔ uProp
 definition false ≔ prod bool (λ x, x)
diff --git a/adlib/cert_f/induction.lp b/adlib/induction.lp
similarity index 77%
rename from adlib/cert_f/induction.lp
rename to adlib/induction.lp
index 6d7e787a3f277403305971b414960580eb0ed75f..932f63bcabbc18cc7dbb75d150bf973ac526edb8 100644
--- a/adlib/cert_f/induction.lp
+++ b/adlib/induction.lp
@@ -1,5 +1,5 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
 
 // Allows to make case disjunction in proofs,
 // [refine disjunction P ?Cfalse ?Ctrue]
diff --git a/adlib/cert_f/nat.lp b/adlib/nat.lp
similarity index 100%
rename from adlib/cert_f/nat.lp
rename to adlib/nat.lp
diff --git a/adlib/cert_f/subtype.lp b/adlib/subtype.lp
similarity index 96%
rename from adlib/cert_f/subtype.lp
rename to adlib/subtype.lp
index ec0d4d1d34b94a163f098ce26dae7167bb8ca232..534f6e3e73f27c6e0511f53aeae53189cd713f6f 100644
--- a/adlib/cert_f/subtype.lp
+++ b/adlib/subtype.lp
@@ -1,5 +1,5 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
 
 // rule Term (ePsub &A _ ⊑ &A) → Term true
 //  and Term ((ePsub &A &P) ⊑ (ePsub &B &Q)) →
diff --git a/adlib/core/nat.lp b/alternatives/adlib/core/nat.lp
similarity index 100%
rename from adlib/core/nat.lp
rename to alternatives/adlib/core/nat.lp
diff --git a/adlib/core/nat_ops.lp b/alternatives/adlib/core/nat_ops.lp
similarity index 100%
rename from adlib/core/nat_ops.lp
rename to alternatives/adlib/core/nat_ops.lp
diff --git a/prelude/core/boolean_props.lp b/alternatives/prelude/core/boolean_props.lp
similarity index 100%
rename from prelude/core/boolean_props.lp
rename to alternatives/prelude/core/boolean_props.lp
diff --git a/prelude/core/booleans.lp b/alternatives/prelude/core/booleans.lp
similarity index 100%
rename from prelude/core/booleans.lp
rename to alternatives/prelude/core/booleans.lp
diff --git a/prelude/core/equalities.lp b/alternatives/prelude/core/equalities.lp
similarity index 100%
rename from prelude/core/equalities.lp
rename to alternatives/prelude/core/equalities.lp
diff --git a/prelude/core/if_def.lp b/alternatives/prelude/core/if_def.lp
similarity index 100%
rename from prelude/core/if_def.lp
rename to alternatives/prelude/core/if_def.lp
diff --git a/prelude/core/notequal.lp b/alternatives/prelude/core/notequal.lp
similarity index 100%
rename from prelude/core/notequal.lp
rename to alternatives/prelude/core/notequal.lp
diff --git a/prelude/core/quantifier_props.lp b/alternatives/prelude/core/quantifier_props.lp
similarity index 100%
rename from prelude/core/quantifier_props.lp
rename to alternatives/prelude/core/quantifier_props.lp
diff --git a/prelude/core/xor_def.lp b/alternatives/prelude/core/xor_def.lp
similarity index 100%
rename from prelude/core/xor_def.lp
rename to alternatives/prelude/core/xor_def.lp
diff --git a/sandbox/core/rat.lp b/alternatives/sandbox/core/rat.lp
similarity index 100%
rename from sandbox/core/rat.lp
rename to alternatives/sandbox/core/rat.lp
diff --git a/sandbox/core/rat_explicit.lp b/alternatives/sandbox/core/rat_explicit.lp
similarity index 100%
rename from sandbox/core/rat_explicit.lp
rename to alternatives/sandbox/core/rat_explicit.lp
diff --git a/lambdapi.pkg b/lambdapi.pkg
new file mode 100644
index 0000000000000000000000000000000000000000..8c92627052d13f9c179a4cc0d6147c3fd19966cd
--- /dev/null
+++ b/lambdapi.pkg
@@ -0,0 +1,2 @@
+package_name = personoj
+root_path = personoj
diff --git a/prelude/cert_f/functions.lp b/prelude/functions.lp
similarity index 92%
rename from prelude/cert_f/functions.lp
rename to prelude/functions.lp
index 5d258129ba27b1e0d2d73fc1abd8d63829b8cf7d..a2f29e769c2dc1061f1cda1297c6beb3944cdfd6 100644
--- a/prelude/cert_f/functions.lp
+++ b/prelude/functions.lp
@@ -1,7 +1,7 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
-prelude.cert_f.logic
-require adlib.cert_f.subtype as S
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
+personoj.prelude.logic
+require personoj.adlib.subtype as S
 
 //
 // functions [D, R: TYPE]
diff --git a/prelude/cert_f/logic.lp b/prelude/logic.lp
similarity index 87%
rename from prelude/cert_f/logic.lp
rename to prelude/logic.lp
index 18ee520fa825d364fbe3a9a21f7ae834d46a88fd..ef6be7110053238a7fff0b7275300752ef4b888d 100644
--- a/prelude/cert_f/logic.lp
+++ b/prelude/logic.lp
@@ -1,7 +1,7 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
-require adlib.cert_f.induction as I
-require adlib.cert_f.subtype as S
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
+require personoj.adlib.induction as I
+require personoj.adlib.subtype   as S
 
 //
 // Booleans
@@ -28,7 +28,6 @@ symbol if {T: Term uType}: Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
 //
 // boolean_props
 // Slightly modified from the prelude
-// FIXME explicitness required
 constant symbol bool_exclusive: Term (neq false true)
 constant symbol bool_inclusive A: Term ((eq A false) ∨ (eq A true))
 
@@ -46,15 +45,13 @@ qed
 //
 // xor_def
 //
-// FIXME explicitness required
 definition xor (a b: Term bool) ≔ neq a b
 
-// FIXME explicitness required
 theorem xor_def (a b: Term bool):
-  Term (@eq bool (xor a b) (if a (bnot b) b))
+  Term (eq (xor a b) (if a (bnot b) b))
 proof
 refine I.disjunction
-  (λa: Term bool, @forall bool (λb, eq (xor a b) (if a (bnot b) b)))
+  (λa: Term bool, forall (λb, eq (xor a b) (if a (bnot b) b)))
   ?Cf ?Ct
 refine I.disjunction
   (λ b, eq (xor false b) (if false (bnot b) b))
diff --git a/prelude/cert_f/numbers.lp b/prelude/numbers.lp
similarity index 92%
rename from prelude/cert_f/numbers.lp
rename to prelude/numbers.lp
index 42ba6f7e2c46847b6e3b4a005b4ea637a85b8a26..a471a2af1eb5eed3aa900780cf73bdad1659d261 100644
--- a/prelude/cert_f/numbers.lp
+++ b/prelude/numbers.lp
@@ -1,8 +1,7 @@
-require adlib.cert_f.subtype as S
-require open encodings.cert_f
-adlib.cert_f.bootstrap
-// adlib.cert_f.numerals
-prelude.cert_f.logic
+require personoj.adlib.subtype as S
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
+personoj.prelude.logic
 
 //
 // Theory numbers
@@ -58,6 +57,8 @@ symbol closed_plus_real: ∀(x y: Term real),
   let ynf ≔ ↑ numfield pr y in
   Term (real_pred (xnf + ynf))
 
+hint Term &x ≡ Univ Type → &x ≡ uType
+
 // With polymorphic plus
 rule ty_plus real real → real
 
@@ -92,6 +93,12 @@ proof
   refine S.restr real rational_pred
 qed
 
+hint Psub &x ⊑ &y ≡ rational ⊑ real → &x ≡ rational_pred, &y ≡ real
+theorem rat_is_real_auto: Term (rational ⊑ real)
+proof
+  apply S.restr _ _
+qed
+
 definition nonzero_rational_pred (x: Term rational): Term bool ≔
   neq zero (↑ real rat_is_real x)
 definition nonzero_rational ≔ Psub nonzero_rational_pred
diff --git a/sandbox/cert_f/even.lp b/sandbox/even.lp
similarity index 100%
rename from sandbox/cert_f/even.lp
rename to sandbox/even.lp
diff --git a/sandbox/cert_f/rat.lp b/sandbox/rat.lp
similarity index 100%
rename from sandbox/cert_f/rat.lp
rename to sandbox/rat.lp