diff --git a/paper/equal.lp b/paper/equal.lp
index d7770401b05289811b105f3c3a005d5be9a8bd47..d65d092b700c18ad9f97b07593a603ba1bd9dcdb 100644
--- a/paper/equal.lp
+++ b/paper/equal.lp
@@ -1,6 +1,5 @@
-require open
-personoj.encodings.lhol
-personoj.encodings.pvs_cert
-personoj.paper.prenex
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require personoj.encodings.prenex as P
 
-symbol eq: χ (forall_pt (λT: ϕ ctype, ∇ (T ~> T ~> cbool)))
+symbol eq: P.χ (P.forallS (λT: ϕ {|set|}, P.∇ (T ~> T ~> bool)))