diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index bf2e6c531e87abbdbbadb2f7311ba696ccc9554d..e2b4901cfe57eca93bcf3c5086cb2df2c17b3a8a 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -13,18 +13,18 @@ set declared "∀B"
 
 symbol SchemeK: TYPE
 symbol ϕ: SchemeK → TYPE
-symbol schemeK: Kind → SchemeK
-rule ϕ (schemeK $X) ↪ θ $X
+symbol scheme_k: Kind → SchemeK
+rule ϕ (scheme_k $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
+symbol SchemeS: TYPE
+symbol χ: SchemeS → TYPE
+symbol scheme_s: Set → SchemeS
+rule χ (scheme_s $X) ↪ η $X
 
-constant symbol ∀S: (Set → Scheme) → Scheme
+constant symbol ∀S: (Set → SchemeS) → SchemeS
 rule χ (∀S $e) ↪ Πt: Set, χ ($e t)
 
 constant symbol ∀B: (Set → Bool) → Bool
diff --git a/paper/equal.lp b/paper/equal.lp
index 150cc40fd787ba360638de5a33a9507566e64084..d177f9fc73899324b94e7198c1b4f04ad8bd1dc5 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_s (T ~> T ~> bool)))
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 4d7d541bd4cadbed1c495c4704478575aed98c93..ffcae6ffcdc7abdd6be1762c41d7ea97b27bcae5 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -60,7 +60,7 @@ admit
 //
 // Defined types
 //
-definition pred: ϕ (∀K (λ_, schemeK {|set|})) ≔ λt, t ~> bool
+definition pred: ϕ (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> bool
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred