diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index 1c798adb5ab8a203233a2399be0944779b1ea109..bf2e6c531e87abbdbbadb2f7311ba696ccc9554d 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -1,18 +1,31 @@
-// Prenex polymorphism
+// Prenex polymorphism: prenex quantification on elements of type ‘Set’.
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
+// Quantification for objects of type ‘Kind’
+set declared "Ï•"
+set declared "∀K"
+// Quantification for objects of type ‘Set’
 set declared "χ"
 set declared "∀S"
+// Quantification for objects of type ‘Bool’
 set declared "∀B"
 
+symbol SchemeK: TYPE
+symbol ϕ: SchemeK → TYPE
+symbol schemeK: Kind → SchemeK
+rule ϕ (schemeK $X) ↪ θ $X
+
+constant symbol ∀K: (Set → SchemeK) → SchemeK
+rule ϕ (∀K $e) ↪ Πt: Set, ϕ ($e t)
+
 symbol Scheme: TYPE
 symbol χ: Scheme → TYPE
 symbol scheme: Set → Scheme
 rule χ (scheme $X) ↪ η $X
 
 constant symbol ∀S: (Set → Scheme) → Scheme
-rule χ (∀S $p) ↪ ΠT: Set, χ ($p T)
+rule χ (∀S $e) ↪ Πt: Set, χ ($e t)
 
 constant symbol ∀B: (Set → Bool) → Bool
-rule ε (∀B $P) ↪ Πx: Set, ε ($P x)
+rule ε (∀B $p) ↪ Πx: Set, ε ($p x)
diff --git a/prelude/logic.lp b/prelude/logic.lp
index e04d30546d58b6bb9bf9f05d63ce32b02957f564..4d7d541bd4cadbed1c495c4704478575aed98c93 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -60,8 +60,7 @@ admit
 //
 // Defined types
 //
-// NOTE ‘pred’ cannot be typed in the encoding
-definition pred (t: θ {|set|}) ≔ t ~> bool
+definition pred: ϕ (∀K (λ_, schemeK {|set|})) ≔ λt, t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred