From 5a8a37866a3d0657a5f864f83d90606cadd8d038 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 28 Feb 2020 15:28:26 +0100
Subject: [PATCH] removed buggy rule

---
 encodings/cert_f.lp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index 758b3c7..edd1076 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -39,8 +39,6 @@ rule Term (@prod &s1 &s2 &A &B) → ∀ x : @Term &s1 &A, @Term &s2 (&B x)
 // - second is a predicate on [A] verified by the first element.
 symbol ePsub (A : Term uType) : (Term A ⇒ Term uProp) ⇒ Term uType
 
-rule Term (ePsub _ _) → Univ Type
-
 // Γ ⊢ M : { v : T | U }
 // —————————————————————PROJl
 //      Γ ⊢ fst(M) : T
-- 
GitLab