diff --git a/encoding/examples/rat.lp b/encoding/examples/rat.lp
index 885c5b5eda1d47bf915fe543627dc36ebac71e5c..598b58b28d4c594ce306a68a691100f24aa66633 100644
--- a/encoding/examples/rat.lp
+++ b/encoding/examples/rat.lp
@@ -2,7 +2,7 @@ require open personoj.lhol;
 require open personoj.pvs_cert;
 
 // Prelude with some logics operator
-symbol ⇒ P Q ≔ impd {P} (λ _, Q);
+symbol ⇒ P Q ≔ P ⇒ (λ _, Q); // Use a non dependent implication
 notation ⇒ infix right 6;
 symbol false ≔ ∀ {prop} (λ x, x);
 symbol true ≔ false ⇒ false;
diff --git a/encoding/extra/if.lp b/encoding/extra/if.lp
index 2c770928d0ad5df32ef85beb94148239075a1b13..34db71d165b8479bdc546bf828791a80c9c3624e 100644
--- a/encoding/extra/if.lp
+++ b/encoding/extra/if.lp
@@ -4,7 +4,7 @@ require open personoj.lhol
              personoj.pvs_cert;
 
 symbol false ≔ ∀ {prop} (λ x, x);
-symbol true ≔ impd {false} (λ _, false);
+symbol true ≔ false ⇒ (λ _, false);
 
 symbol eq {s: Set}: El s → El s → El prop;
 symbol = {s} ≔ @eq s;
diff --git a/encoding/lhol.lp b/encoding/lhol.lp
index c9af629f6a4b471913b710ae8d38b0dcba7722d5..d834dced6918df1d6095448901ba9f41529b3c83 100644
--- a/encoding/lhol.lp
+++ b/encoding/lhol.lp
@@ -11,8 +11,8 @@ rule El prop ↪ Prop;
 constant symbol ∀ {x: Set}: (El x → Prop) → Prop;
 rule Prf (∀ {$X} $P) ↪ Π x: El $X, Prf ($P x);
 
-constant symbol impd {x: Prop}: (Prf x → Prop) → Prop;
-rule Prf (impd {$H} $P) ↪ Π h: Prf $H, Prf ($P h);
+constant symbol ⇒ (p: Prop): (Prf p → Prop) → Prop; notation ⇒ infix right 2;
+rule Prf ($P ⇒ $Q) ↪ Π h: Prf $P, Prf ($Q h);
 
 constant symbol arrd (x: Set): (El x → Set) → Set;
 rule El (arrd $X $T) ↪ Π x: El $X, El ($T x);
diff --git a/encoding/logical.lp b/encoding/logical.lp
index c7ebe31dd1470f4d79b8cd4bf34d4e5c2485607b..a711962dbd431ceaf26be8608e9b8ff735dace02 100644
--- a/encoding/logical.lp
+++ b/encoding/logical.lp
@@ -1,10 +1,9 @@
 // Definition based on implication
 require open personoj.lhol;
 
-symbol ⇒ P Q ≔ impd {P} Q;             notation ⇒ infix right 2;
-symbol false ≔ ∀ {prop} (λ x, x);
-symbol true ≔ false ⇒ (λ _, false);
-symbol ¬ P ≔ impd {P} (λ _, false);    notation ¬ prefix 5;
+symbol false ≔ ∀ {prop} (λ x: El prop, x);
+symbol true ≔ false ⇒ (λ _: Prf false, false);
+symbol ¬ P ≔ P ⇒ (λ _, false);         notation ¬ prefix 5;
 symbol ∧ P Q ≔ ¬ (P ⇒ (λ h, ¬ (Q h))); notation ∧ infix 4;
 symbol ∨ P Q ≔ (¬ P) ⇒ Q;              notation ∨ infix 3;