diff --git a/paper/equal.lp b/paper/equal.lp
new file mode 100644
index 0000000000000000000000000000000000000000..d7770401b05289811b105f3c3a005d5be9a8bd47
--- /dev/null
+++ b/paper/equal.lp
@@ -0,0 +1,6 @@
+require open
+personoj.encodings.lhol
+personoj.encodings.pvs_cert
+personoj.paper.prenex
+
+symbol eq: χ (forall_pt (λT: ϕ ctype, ∇ (T ~> T ~> cbool)))