From 767587851fe81937ff5021b77acea393fd9bbc7c Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Mon, 6 Apr 2020 17:21:30 +0200
Subject: [PATCH] encoding of polymorphic equality

---
 paper/equal.lp | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 paper/equal.lp

diff --git a/paper/equal.lp b/paper/equal.lp
new file mode 100644
index 0000000..d777040
--- /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)))
-- 
GitLab