diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index 7aac76c27bad58d04ee09e3aa7790cbe540a6747..0aa7d98dd07c0e727fd901f34edb7cb9ecf43bc5 100644
--- a/encodings/bool_plus.lp
+++ b/encodings/bool_plus.lp
@@ -1,6 +1,6 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.prenex
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
 
 // It may be generalisable to dependent propositions
 theorem and_intro:
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index 115d7713fbb320a9092020b744c600c4b869ee24..5d469557237b780450a6e40edaa316a3c8eb516f 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -1,8 +1,9 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
+require open personoj.encodings.prenex
 
-constant symbol {|!Number!|}: θ {|set|}
+constant symbol {|!Number!|}: Set
 
 constant symbol zero: El {|!Number!|}
 constant symbol succ: El ({|!Number!|} ~> {|!Number!|})
@@ -17,7 +18,7 @@ with Prf (zero = succ _) ↪ Prf false
 with Prf (zero = zero) ↪ Prf true
 
 // Define strings as list of numbers
-constant symbol {|!String!|}: θ {|set|}
+constant symbol {|!String!|}: Set
 constant symbol str_empty: El {|!String!|}
 constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|}
 
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index 9b1fc41bf21624e2b6a3291a2a13ecc8c0017b63..ffc1bff0e3794aef628e7372f3d022015f3633e2 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -7,7 +7,8 @@
 
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
+require open personoj.encodings.prenex
 
 constant symbol darr: Set → Kind → Kind
 set infix right 6 "*>" ≔ darr
-rule θ ($t *> $k) ↪ El $t → θ $k
+rule Ty ($t *> $k) ↪ El $t → Ty $k
diff --git a/encodings/bool_pvs.lp b/encodings/if.lp
similarity index 100%
rename from encodings/bool_pvs.lp
rename to encodings/if.lp
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 8e94c6fcb3819199d0f216171f48ad5017a96a88..75843f2598f6f420c849efb602f69f591c16123a 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -3,16 +3,13 @@ symbol Kind: TYPE
 symbol Set: TYPE
 symbol Bool: TYPE
 
-set declared "θ"
 set declared "∀"
-injective symbol θ: Kind → TYPE
 injective symbol El: Set → TYPE
 injective symbol Prf: Bool → TYPE
 
 constant symbol {|set|}: Kind
 constant symbol bool: Set
 
-rule θ {|set|} ↪ Set
 rule El bool ↪ Bool
 
 constant symbol ∀ {x: Set}: (El x → Bool) → Bool
diff --git a/encodings/bool_hol.lp b/encodings/logical.lp
similarity index 100%
rename from encodings/bool_hol.lp
rename to encodings/logical.lp
diff --git a/encodings/pairs.lp b/encodings/pairs.lp
index eb53f18b0892eecbe29fbc84445b4315dab204fd..4b852f2e49188bed4f438f3d7faca14033f24c41 100644
--- a/encodings/pairs.lp
+++ b/encodings/pairs.lp
@@ -1,8 +1,4 @@
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
-require open personoj.encodings.tuple
-require open personoj.encodings.prenex
 
 set declared "Σ" // Dependent pairs
 set declared "σ" // Non dependent pairs
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index 77709b20a027ce61fde0bbf293e3fe1cd4812208..3ac6e860fb30a540a24650b07bfd3eb4fd04ece4 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -8,29 +8,31 @@
 require open personoj.encodings.lhol
 
 // 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"
 
+// To interpret PVS sorts
+injective symbol Ty : Kind → TYPE
+rule Ty {|set|} ↪ Set
+
 constant symbol SchemeK: TYPE
-symbol ϕ: SchemeK → TYPE
+injective symbol El_k: SchemeK → TYPE
 constant symbol scheme_k: Kind → SchemeK
-rule ϕ (scheme_k $X) ↪ θ $X
+rule El_k (scheme_k $X) ↪ Ty $X
 
 constant symbol ∀K: (Set → SchemeK) → SchemeK
-rule ϕ (∀K $e) ↪ Πt: Set, ϕ ($e t)
+rule El_k (∀K $e) ↪ Πt: Set, El_k ($e t)
 
 constant symbol SchemeS: TYPE
-symbol χ: SchemeS → TYPE
+injective symbol El_s: SchemeS → TYPE
 constant symbol scheme_s: Set → SchemeS
-rule χ (scheme_s $X) ↪ El $X
+rule El_s (scheme_s $X) ↪ El $X
 
 constant symbol ∀S: (Set → SchemeS) → SchemeS
-rule χ (∀S $e) ↪ Πt: Set, χ ($e t)
+rule El_s (∀S $e) ↪ Πt: Set, El_s ($e t)
 
 constant symbol ∀B: (Set → Bool) → Bool
 rule Prf (∀B $p) ↪ Πx: Set, Prf ($p x)
diff --git a/prelude/functions.lp b/prelude/functions.lp
index fe6835edd13415c91740791151cdf10f8d57e2c2..c0d6db25cd39118d7d925c8ab5987898916d0106 100644
--- a/prelude/functions.lp
+++ b/prelude/functions.lp
@@ -1,6 +1,6 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
 require open personoj.encodings.prenex
 require open personoj.prelude.logic
 //
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 66947840b33eb5d1aec1fef8e0f2a3b407cdb6dd..cd351e4fe5e99a7bb9312f151a17829766844f8a 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -1,6 +1,6 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.logical
 require open personoj.encodings.prenex
 require open personoj.encodings.builtins
 //
@@ -60,7 +60,7 @@ admit
 //
 // Defined types
 //
-definition pred: ϕ (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> bool
+definition pred: El_k (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred
@@ -112,8 +112,8 @@ set builtin "eqind" ≔ eqind
 //
 
 theorem lift_if1:
-  Prf (∀B (λs: θ {|set|},
-           ∀B (λt: θ {|set|},
+  Prf (∀B (λs: Ty {|set|},
+           ∀B (λt: Ty {|set|},
                  ∀ {bool}
                    (λa,
                       ∀ (λx: El s,