From 41f1e8704dff753fc5e144f00f2a10eaae896387 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Mon, 30 Nov 2020 14:07:44 +0100
Subject: [PATCH] fixed import, use maximal supertype

---
 encodings/pair_equality.lp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/encodings/pair_equality.lp b/encodings/pair_equality.lp
index 976d5b3..3da34c1 100644
--- a/encodings/pair_equality.lp
+++ b/encodings/pair_equality.lp
@@ -1,6 +1,7 @@
 require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
 require open personoj.encodings.pairs
 require open personoj.encodings.logical
 
-symbol peq {t: Set} (_: El (σ t t)): Bool
-definition pneq  {t: Set} (m: El (σ t t)) ≔ ¬ (@peq t m)
+symbol peq {t: Set} (_: El (σ (μ t) (μ t))): Bool
+definition pneq  {t} m ≔ ¬ (@peq t m)
-- 
GitLab