diff --git a/README.md b/README.md
index 61186d6902cfb4d76a84625ca30685d0069570e1..a9937b73373e4de28c00a95217e8efdfa18e8738 100644
--- a/README.md
+++ b/README.md
@@ -13,7 +13,7 @@ library, also known as _Prelude_. The prelude is available
 
 
 ## Requirements
-- [`lambdapi`](https://github.com/gabrielhdt/lambdapi.git) on the `unif_hint`
+- [`lambdapi`](https://github.com/gabrielhdt/lambdapi.git) on the `heavy-let`
   branch
 
 ## Structure
diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index 6558d9fc84eb1934d4a1ff4cde21f77a4153f00f..0f48d20b8f247336184e9bbac70acefc85dff921 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -26,8 +26,6 @@ injective symbol Term {s: Sort}: Univ s ⇒ TYPE
 rule Term uProp → Univ Prop
  and Term uType → Univ Type
 
-hint Term &x ≡ Univ Prop → &x ≡ uProp
-
 // [prod s1 s2 A B] encodes [Π x : (A: s1). (B: s2)]
 symbol prod {sA: Sort} {sB: Sort} (A: Univ sA):
   (Term A ⇒ Univ sB) ⇒ Univ (Rule sA sB)
@@ -68,6 +66,8 @@ protected symbol opair (T: Univ Type) (P: Term T ⇒ Univ Prop) (M: Term T):
 rule pair {&T} &P &M _ → opair &T &P &M
 
 rule fst (opair _ _ &M) → &M
+// and opair _ &P (fst {_} {&P} &X) → &X // Surjective pairing
+//NOTE: can we remove non linearity?
 
 // The subtype relation
 symbol subtype: Term uType ⇒ Term uType ⇒ Term uProp
diff --git a/prelude/functions.lp b/prelude/functions.lp
index a2f29e769c2dc1061f1cda1297c6beb3944cdfd6..7f87e40cd78b4c1cd69d14f2289b256d57b4fd99 100644
--- a/prelude/functions.lp
+++ b/prelude/functions.lp
@@ -7,6 +7,10 @@ require personoj.adlib.subtype as S
 // functions [D, R: TYPE]
 //
 
+// symbol
+// extensionality_postulate (D R: Term uType) (f g: Term (D ~> R))
+// : Term (biff (forall (λx: Term D, f x = g ) (f = g)))
+
 definition {|injective?|} {D} {R} (f: Term (D ~> R))
   ≔ forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))
 
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 2d062b3f021df622dc6a0142f3bd36e33c09302e..ba69e89fb50c02087a594bc6a600e45d589c30cf 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -28,8 +28,9 @@ symbol if {T: Term uType}: Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
 //
 // boolean_props
 // Slightly modified from the prelude
-constant symbol bool_exclusive: Term (neq false true)
-constant symbol bool_inclusive A: Term ((eq A false) ∨ (eq A true))
+constant symbol bool_exclusive: Term (neq {bool} false true)
+constant symbol
+bool_inclusive A: Term ((eq {bool} A false) ∨ (eq {bool} A true))
 
 theorem excluded_middle (A: Term bool): Term (A ∨ ¬ A)
 proof
@@ -45,16 +46,16 @@ qed
 //
 // xor_def
 //
-definition xor (a b: Term bool) ≔ neq a b
+definition xor (a b: Term bool) ≔ neq {bool} a b
 
 theorem xor_def (a b: Term bool):
-  Term (eq (xor a b) (if a (bnot b) b))
+  Term (eq {bool} (xor a b) (if {bool} a (bnot b) b))
 proof
 refine I.disjunction
-  (λa: Term bool, forall (λb, eq (xor a b) (if a (bnot b) b)))
+  (λa: Term bool, forall {bool} (λb, eq {bool} (xor a b) (if {bool} a (bnot b) b)))
   ?Cf ?Ct
 refine I.disjunction
-  (λ b, eq (xor false b) (if false (bnot b) b))
+  (λ b, eq {bool} (xor false b) (if {bool} false (bnot b) b))
   ?Ccf ?Cct
 admit
 
@@ -122,6 +123,6 @@ print
 admit
 
 theorem lift_if2 (S: Term uType) (a b c: Term bool) (x y: Term S):
-  Term ((if (if a b c) x y) = (if a (if b x y) (if c x y)))
+  Term ((if (if {bool} a b c) x y) = (if a (if b x y) (if c x y)))
 proof
 admit
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index a471a2af1eb5eed3aa900780cf73bdad1659d261..c137f2fa708b5d5a4c11c3ca4337b68d72314c4e 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -57,7 +57,7 @@ symbol closed_plus_real: ∀(x y: Term real),
   let ynf ≔ ↑ numfield pr y in
   Term (real_pred (xnf + ynf))
 
-hint Term &x ≡ Univ Type → &x ≡ uType
+// hint Term &x ≡ Univ Type → &x ≡ uType
 
 // With polymorphic plus
 rule ty_plus real real → real
@@ -93,7 +93,7 @@ proof
   refine S.restr real rational_pred
 qed
 
-hint Psub &x ⊑ &y ≡ rational ⊑ real → &x ≡ rational_pred, &y ≡ real
+// hint Psub &x ⊑ &y ≡ rational ⊑ real → &x ≡ rational_pred, &y ≡ real
 theorem rat_is_real_auto: Term (rational ⊑ real)
 proof
   apply S.restr _ _