fix in subtype, infix functions

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
 

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)