diff --git a/paper/proof_irr.lp b/paper/proof_irr.lp
index 6de8b6b21206aed34c30d1ece13df785f77e5039..9563c7305bcdae5cdf441a5ec33fa07a41427834 100644
--- a/paper/proof_irr.lp
+++ b/paper/proof_irr.lp
@@ -1,6 +1,7 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.logical
+require open personoj.encodings.equality
 
 
 set declared "â„•"
diff --git a/paper/stack.lp b/paper/stack.lp
index 1561c4185e32a50bdd6d6b6ea85c863275daddd3..04d1544ee328e93a3bf987bd502efccac2ca7234 100644
--- a/paper/stack.lp
+++ b/paper/stack.lp
@@ -1,6 +1,7 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.logical
+require open personoj.encodings.equality
 
 constant symbol stack: Set
 constant symbol empty: El stack
diff --git a/paper/rat_poly.lp b/sandbox/rat_poly.lp
similarity index 100%
rename from paper/rat_poly.lp
rename to sandbox/rat_poly.lp