diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 7dabafd973d5133e6018d5ec333c8f62828d8ab6..0fc57f84177b955cc41e09c9a3b31b93710e0a80 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -3,29 +3,29 @@ symbol Kind: TYPE
 symbol Set: TYPE
 symbol Bool: TYPE
 
-set declared "Ï•"
+set declared "θ"
 set declared "η"
 set declared "ε"
 set declared "∀"
-injective symbol ϕ: Kind → TYPE
+injective symbol θ: Kind → TYPE
 injective symbol η: Set → TYPE
 injective symbol ε: Bool → TYPE
 
-symbol {|set|}: Kind
-symbol bool: Set
+constant symbol {|set|}: Kind
+constant symbol bool: Set
 
-rule ϕ {|set|} ↪ Set
+rule θ {|set|} ↪ Set
 rule η bool ↪ Bool
 
-symbol ∀ {x: Set}: (η x → Bool) → Bool
-symbol impd {x: Bool}: (ε x → Bool) → Bool
-symbol arrd {x: Set}: (η x → Set) → Set
+constant symbol ∀ {x: Set}: (η x → Bool) → Bool
+constant symbol impd {x: Bool}: (ε x → Bool) → Bool
+constant symbol arrd {x: Set}: (η x → Set) → Set
 
 rule ε (∀ {$X} $P) ↪ Πx: η $X, ε ($P x)
 with ε (impd {$H} $P) ↪ Πh: ε $H, ε ($P h)
 with η (arrd {$X} $T) ↪ Πx: η $X, η ($T x)
 
-symbol arr: Set → Set → Set
+constant symbol arr: Set → Set → Set
 rule η (arr $X $Y) ↪ (η $X) → (η $Y)
 set infix right 6 "~>" ≔ arr
 
diff --git a/encodings/pvs_more.lp b/encodings/pvs_more.lp
new file mode 100644
index 0000000000000000000000000000000000000000..ab7a0cb976ec1c99ce71c5774140bf56abac6b6f
--- /dev/null
+++ b/encodings/pvs_more.lp
@@ -0,0 +1,10 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+// Dependent type
+// FIXME: quantification on types must be restricted to a prenex form
+set declared "ι"
+symbol ι: Kind → TYPE
+symbol dt_arr: Kind → Kind → Kind
+set infix right 7 "*>" ≔ dt_arr
+rule ι ({|set|} *> {|set|}) ↪ θ {|set|} → θ {|set|}
diff --git a/paper/equal.lp b/paper/equal.lp
index 7bd14765f5b5cfc33f82aeef496b24f0f08e61f2..150cc40fd787ba360638de5a33a9507566e64084 100644
--- a/paper/equal.lp
+++ b/paper/equal.lp
@@ -2,4 +2,4 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.prenex
 
-symbol eq: χ (∀S (λT: ϕ {|set|}, scheme (T ~> T ~> bool)))
+symbol eq: χ (∀S (λT: θ {|set|}, scheme (T ~> T ~> bool)))
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 0daaf1acfa5eddbf5a4872b0bf79d4ce778dc7ef..d109dc042769173804c04253b27e5a894de9b6e3 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -64,9 +64,8 @@ definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
 // Defined types
 //
 // FIXME: needs another prenex polymorphism to be encoded,
-// ∀K (λt, ? (t ~> {|set|})) ≔ λt: ϕ {|set|}, t ~> bool
-// definition pred : χ (∀S (λt, scheme (t ~> {|set|}))) ≔ λt: ϕ {|set|}, t ~> bool
-definition pred t ≔ t ~> bool
+require open personoj.encodings.pvs_more
+definition pred : ι ({|set|} *> {|set|}) ≔ λt: θ {|set|}, t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index c6e066031859c579db240f24946bb50dad7aa692..9f47ebe9a7c1df74c739e39707c0777e29a6b01f 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -7,7 +7,7 @@ require open personoj.prelude.logic
 //
 // Theory numbers
 //
-constant symbol number: Ï• {|set|}
+constant symbol number: θ {|set|}
 
 //
 // Theory number_fields