diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index f5fd584a6beb0b77366d6d81a81f72ff06243ed8..a6cde4e6506ee08d13b51e9c2a78d582b3b44ce5 100644
--- a/encodings/bool_plus.lp
+++ b/encodings/bool_plus.lp
@@ -1,5 +1,4 @@
 require open personoj.encodings.lhol
-             personoj.encodings.prenex
              personoj.encodings.logical;
 
 // It may be generalisable to dependent propositions
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index 28afce3a34c41bd66d1b346204493db6e8c7b29d..07edfb415da4f746ce934b40b59ef5e8d8c243db 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -1,8 +1,7 @@
 require open personoj.encodings.lhol
              personoj.encodings.pvs_cert
              personoj.encodings.logical
-             personoj.encodings.equality
-             personoj.encodings.prenex;
+             personoj.encodings.equality;
 
 constant symbol {|!Number!|}: Set;
 
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index 75a9c8d7061643f1c05be10397642b4cc5119fea..d6c57766c5e3cdfbfba79edb96278ad1295041a3 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -8,6 +8,9 @@
 require open personoj.encodings.lhol
              personoj.encodings.pvs_cert;
 
+constant symbol Kind: TYPE;
+constant symbol set: Kind;
+
 injective symbol Ty : Kind → TYPE;
 rule Ty set ↪ Set;
 
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 08e11753115f727aaece26d703c503415d4b237a..fb6484fad8d3d8c9e544df46afbf4e4ecfcf963b 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -1,12 +1,10 @@
 /// Encoding of λHOL
-symbol Kind: TYPE;
 symbol Set: TYPE;
 symbol Prop: TYPE;
 
 injective symbol El: Set → TYPE;
 injective symbol Prf: Prop → TYPE;
 
-constant symbol {|set|}: Kind;
 constant symbol prop: Set;
 
 rule El prop ↪ Prop;
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
deleted file mode 100644
index 725dab81eceb7d2b4a21b57afaf5bc7c8571fc70..0000000000000000000000000000000000000000
--- a/encodings/prenex.lp
+++ /dev/null
@@ -1,31 +0,0 @@
-/// Prenex polymorphism
-
-/// Prenex polymorphism allows to quantify over variables of type ‘Set’.
-/// PVS allows it in theory formals, such as
-/// groups[t: TYPE]: THEORY BEGIN ... END groups
-/// For more informations on the encoding of prenex polymorphism, see
-/// https://arxiv.org/abs/1807.01873 and theory U
-require open personoj.encodings.lhol
-             personoj.encodings.deptype;
-
-// Quantification for objects of type ‘Kind’
-constant symbol SchemeK: TYPE;
-injective symbol El_k: SchemeK → TYPE;
-constant symbol scheme_k: Kind → SchemeK;
-rule El_k (scheme_k $X) ↪ Ty $X;
-
-constant symbol ∀K: (Set → SchemeK) → SchemeK;
-rule El_k (∀K $e) ↪ Π t: Set, El_k ($e t);
-
-// Quantification for objects of type ‘Set’
-constant symbol SchemeS: TYPE;
-injective symbol El_s: SchemeS → TYPE;
-constant symbol scheme_s: Set → SchemeS;
-rule El_s (scheme_s $X) ↪ El $X;
-
-constant symbol ∀S: (Set → SchemeS) → SchemeS;
-rule El_s (∀S $e) ↪ Π t: Set, El_s ($e t);
-
-// Quantification for objects of type ‘Prop’
-constant symbol ∀B: (Set → Prop) → Prop;
-rule Prf (∀B $p) ↪ Π x: Set, Prf ($p x);
diff --git a/encodings/prenex/README.md b/encodings/prenex/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..9da0107f07372e644b40556b0e00ddf1f2a71e47
--- /dev/null
+++ b/encodings/prenex/README.md
@@ -0,0 +1,11 @@
+Prenex polymorphism
+===================
+
+Submodules in this directory provide the encoding of prenex polymorphism.
+Prenex polymorphism is allowed in PVS using the construction
+
+    groups[G: TYPE]: THEORY BEGIN ... END groups
+
+The encoding of prenex polymorphism is described in
+<https://arxiv.org/abs/1807.01873> and in the
+[Theory U](http://www.lsv.fr/~dowek/Publi/axiomslong.pdf).
diff --git a/encodings/prenex/kind.lp b/encodings/prenex/kind.lp
new file mode 100644
index 0000000000000000000000000000000000000000..c36b9e0def6bfb85691044911e01259a28bd290e
--- /dev/null
+++ b/encodings/prenex/kind.lp
@@ -0,0 +1,9 @@
+require open personoj.encodings.lhol
+             personoj.encodings.deptype;
+
+constant symbol Scheme: TYPE;
+injective symbol Els: Scheme → TYPE;
+constant symbol lift: Kind → Scheme;
+rule Els (lift $X) ↪ Ty $X;
+constant symbol ∀: (Set → Scheme) → Scheme;
+rule Els (∀ $e) ↪ Π t: Set, Els ($e t);
diff --git a/encodings/prenex/prop.lp b/encodings/prenex/prop.lp
new file mode 100644
index 0000000000000000000000000000000000000000..71f3d982818e74dd961f6b114fccfa11732e134a
--- /dev/null
+++ b/encodings/prenex/prop.lp
@@ -0,0 +1,6 @@
+/// Prenex polymorphism in objects of type ‘Prop’
+
+require open personoj.encodings.lhol;
+
+constant symbol ∀: (Set → Prop) → Prop;
+rule Prf (∀ $P) ↪ Π x: Set, Prf ($P x);
diff --git a/encodings/prenex/set.lp b/encodings/prenex/set.lp
new file mode 100644
index 0000000000000000000000000000000000000000..77e47501ff553db290c646a82f3ae57930ed7efd
--- /dev/null
+++ b/encodings/prenex/set.lp
@@ -0,0 +1,10 @@
+/// Prenex polymorphism in sorts of type ‘Set’
+require personoj.encodings.lhol as lhol;
+
+constant symbol Scheme: TYPE;
+injective symbol El: Scheme → TYPE;
+constant symbol lift: lhol.Set → Scheme;
+rule El (lift $X) ↪ lhol.El $X;
+
+constant symbol ∀: (lhol.Set → Scheme) → Scheme;
+rule El (∀ $e) ↪ Π a: lhol.Set, El ($e a);