diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index b6222b04d43b485a866deb03a3a77e6d89b37e13..1c798adb5ab8a203233a2399be0944779b1ea109 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -3,14 +3,16 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
 set declared "χ"
-set declared "∇"
+set declared "∀S"
+set declared "∀B"
+
 symbol Scheme: TYPE
 symbol χ: Scheme → TYPE
-symbol ∇: Set → Scheme
-rule χ (∇ $X) ↪ η $X
+symbol scheme: Set → Scheme
+rule χ (scheme $X) ↪ η $X
 
-constant symbol forallS: (Set → Scheme) → Scheme
-rule χ (forallS $p) ↪ ΠT: Set, χ ($p T)
+constant symbol ∀S: (Set → Scheme) → Scheme
+rule χ (∀S $p) ↪ ΠT: Set, χ ($p T)
 
-constant symbol forallB: (Set → Bool) → Bool
-rule ε (forallB $P) ↪ Πx: Set, ε ($P x)
+constant symbol ∀B: (Set → Bool) → Bool
+rule ε (∀B $P) ↪ Πx: Set, ε ($P x)
diff --git a/paper/equal.lp b/paper/equal.lp
index d65d092b700c18ad9f97b07593a603ba1bd9dcdb..7bd14765f5b5cfc33f82aeef496b24f0f08e61f2 100644
--- a/paper/equal.lp
+++ b/paper/equal.lp
@@ -1,5 +1,5 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require personoj.encodings.prenex as P
+require open personoj.encodings.prenex
 
-symbol eq: P.χ (P.forallS (λT: ϕ {|set|}, P.∇ (T ~> T ~> bool)))
+symbol eq: χ (∀S (λT: ϕ {|set|}, scheme (T ~> T ~> bool)))