From f84a48c8b815613fb8542a7977ff112905a4e0a6 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Thu, 12 Mar 2020 11:33:10 +0100
Subject: [PATCH] fix in subtype, infix functions

---
 adlib/cert_f/subtype.lp     | 2 +-
 prelude/cert_f/functions.lp | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/adlib/cert_f/subtype.lp b/adlib/cert_f/subtype.lp
index 86999fd..57b4d04 100644
--- a/adlib/cert_f/subtype.lp
+++ b/adlib/cert_f/subtype.lp
@@ -12,7 +12,7 @@ set flag "print_implicits" on
 symbol eqroot: Term uType ⇒ Term uType ⇒ Term uProp
 rule eqroot &X &X → true // NOTE: non linear
  and eqroot (Psub {&T} _) &U → eqroot &T &U
- and eqroot &T (Psub &U _) → eqroot &T &U
+ and eqroot &T (Psub {&U} _) → eqroot &T &U
 
 symbol eqtype: Term uType ⇒ Term uType ⇒ Term uProp
 
diff --git a/prelude/cert_f/functions.lp b/prelude/cert_f/functions.lp
index 61d5537..4cdd088 100644
--- a/prelude/cert_f/functions.lp
+++ b/prelude/cert_f/functions.lp
@@ -9,11 +9,11 @@ definition arrow (D R: Term uType) ≔ prod D (λ_, R)
 // functions [D, R: TYPE]
 //
 
-definition {|injective?|} {D: Term uType} {R:Term uType} (f: Term (arrow D R))
-  ≔ forall (λx1, forall (λx2, imp (eq (f x1) (f x2)) (eq x1 x2)))
+definition {|injective?|} {D} {R} (f: Term (arrow D R))
+  ≔ forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))
 
 definition {|surjective?|} {D: Term uType} {R: Term uType} (f: Term (arrow D R))
-  ≔ forall (λy, ∃ (λx, eq (f x) y))
+  ≔ forall (λy, ∃ (λx, (f x) = y))
 
 definition {|bijective?|} {D: Term uType} {R: Term uType} (f: Term (arrow D R))
   ≔ ({|injective?|} f) ∧ ({|surjective?|} f)
-- 
GitLab