Replace impd with unicode infix implication

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;

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;

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);

encoding/logical.lp

 // 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;