diff --git a/adlib/cert_f/subtype.lp b/adlib/cert_f/subtype.lp
index 86999fd105e585c6154977311fd92ebd0e8382d4..57b4d041676d35138932c8057ae0d5626fe4b695 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 61d55370b404594d51c4b1a58941f4695747430d..4cdd088491c99f187208b2f23dec4a0d0d8d41e0 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)