diff --git a/adlib/bootstrap.lp b/adlib/bootstrap.lp
index c0cef1a09d91e93833419f70621c8d65418b6403..5a2873765ba0efbf80acf262fa08b7e18faa3a1d 100644
--- a/adlib/bootstrap.lp
+++ b/adlib/bootstrap.lp
@@ -5,7 +5,7 @@ definition false ≔ prod bool (λ x, x)
 definition true ≔ prod false (λ _, false)
 
 definition imp (P Q: Term uProp) ≔ prod P (λ_, Q)
-definition forall {T: Term uType} (P: Term T ⇒ Term bool) ≔ prod T P
+definition forall {T: Term uType} (P: Term T → Term bool) ≔ prod T P
 
 definition bnot (P: Term uProp) ≔ prod P (λ _, false)
 set prefix 5 "¬" ≔ bnot
@@ -28,6 +28,6 @@ set builtin "or"  ≔ bor
 set builtin "not" ≔ bnot
 
 // Defined here because ⊑ needs it.
-symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term bool
+symbol eq {T: Term uType}: Term T → Term T → Term bool
 set infix 5 "=" ≔ eq
 // set builtin "eq" ≔ eq
diff --git a/adlib/induction.lp b/adlib/induction.lp
index 932f63bcabbc18cc7dbb75d150bf973ac526edb8..6db6062a553a88d53f4bffb13d02dc701b0bc189 100644
--- a/adlib/induction.lp
+++ b/adlib/induction.lp
@@ -4,5 +4,5 @@ personoj.adlib.bootstrap
 // Allows to make case disjunction in proofs,
 // [refine disjunction P ?Cfalse ?Ctrue]
 // to create two new subgoals
-symbol disjunction (P: Term bool ⇒ Term bool):
-  Term (P false) ⇒ Term (P true) ⇒ ∀ x, Term (P x)
+symbol disjunction (P: Term bool → Term bool):
+  Term (P false) → Term (P true) → Π x, Term (P x)
diff --git a/adlib/subtype.lp b/adlib/subtype.lp
index ae3b19569006e2cf70921ec41414602fb95ba391..54a004be51bf02e2b5f996d57438934c4a41b788 100644
--- a/adlib/subtype.lp
+++ b/adlib/subtype.lp
@@ -2,22 +2,22 @@ require open personoj.encodings.cert_f
         personoj.adlib.bootstrap
 
 // A la rewriting logic
-rule Psub {&A} _ ⊑ &A → true
- and &A ⊑ &A          → true
+rule Psub {$A} _ ⊑ $A ↪ true
+ and $A ⊑ $A          ↪ true
 
 // [eqroot T U] reduces to [true] if [T] and [U] have the same root
-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
+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
 
-symbol eqtype: Term uType ⇒ Term uType ⇒ Term uProp
+symbol eqtype: Term uType → Term uType → Term uProp
 
 symbol refl T: Term (T ⊑ T)
 symbol restr T P: Term (Psub {T} P ⊑ T)
 
 symbol trans (T U V: Term uType):
-  Term (T ⊑ U) ⇒ Term (U ⊑ V) ⇒ Term (T ⊑ V)
+  Term (T ⊑ U) → Term (U ⊑ V) → Term (T ⊑ V)
 
 // [sub {U} P T μ π ρ] proves that, given type [U], [P] predicate from [U],
 // type [T],
@@ -25,19 +25,19 @@ symbol trans (T U V: Term uType):
 // - proof [Ï€] that [T] is a sub-type of [U];
 // - proof [ρ] that any element of [T] verifies [P];
 // [T] is a sub-type of [{x: U | P}].
-symbol sub {U: Term uType} (P: Term U ⇒ Term bool) (T: Term uType)
+symbol sub {U: Term uType} (P: Term U → Term bool) (T: Term uType)
   (_: Term (eqroot T U)) (pr: Term (T ⊑ U)):
-  Term (forall (λx: Term T, P (↑ U pr x))) ⇒ Term (T ⊑ Psub P)
+  Term (forall (λx: Term T, P (↑ U pr x))) → Term (T ⊑ Psub P)
 
 // symbol sub {T S: Term uType}
-//   (P: Term T ⇒ Term bool) (Q: Term S ⇒ Term bool)
+//   (P: Term T → Term bool) (Q: Term S → Term bool)
 //   (psubt: Term (T ⊑ S)): // Proof of T ⊑ S
-//   Term (forall (λx, imp (P x) (Q (↑ S psubt x)))) ⇒
+//   Term (forall (λx, imp (P x) (Q (↑ S psubt x)))) →
 //   Term (Psub T P ⊑ Psub S Q)
 
 // Transitivity of the cast
-rule ↑ {&U} &V &pruv (↑ {&T} &U &prtu &x) →
-  ↑ {&T} &V (trans &T &U &V &prtu &pruv) &x
+rule ↑ {$U} $V $pruv (↑ {$T} $U $prtu $x) ↪
+  ↑ {$T} $V (trans $T $U $V $prtu $pruv) $x
 
 constant symbol cast_trans (A B C: Term uType) (prab: Term (A ⊑ B))
   (prbc: Term (B ⊑ C)) (x: Term A)
diff --git a/alternatives/adlib/core/nat_ops.lp b/alternatives/adlib/core/nat_ops.lp
index b06f59913ed05a41de18b872f740425a1e8351f9..bb5cd0f260853e50f8870354fa247aed61c55740 100644
--- a/alternatives/adlib/core/nat_ops.lp
+++ b/alternatives/adlib/core/nat_ops.lp
@@ -1,13 +1,13 @@
 require open encodings.pvs_core prelude.core.notequal adlib.core.nat
 prelude.core.equalities
 
-symbol times : eta int ⇒ eta int ⇒ eta int
-rule times &n 1  → &n
+symbol times : eta int → eta int → eta int
+rule times $n 1  ↪ $n
 
 set infix left 6 "*" ≔ times
 
-// x =/= 0 ∧ y =/= 0 ⇒ x * y =/= 0
+// x =/= 0 ∧ y =/= 0 → x * y =/= 0
 symbol prod_not_zero (x y: η int) :
-  ε (neq x 0) ⇒ ε (neq y 0) ⇒ ε (neq (x * y) 0)
+  ε (neq x 0) → ε (neq y 0) → ε (neq (x * y) 0)
 
 symbol prod_comm (x y : η int) : ε (eq (x * y) (y * x))
diff --git a/alternatives/prelude/core/boolean_props.lp b/alternatives/prelude/core/boolean_props.lp
index ef0422d971057775dde7b522dc9f1443ce9e33f6..27711eb0d9e1af6e42fe00f4795606ad52e8c8d9 100644
--- a/alternatives/prelude/core/boolean_props.lp
+++ b/alternatives/prelude/core/boolean_props.lp
@@ -1,6 +1,6 @@
 require open encodings.pvs_core
 prelude.core.booleans prelude.core.equalities prelude.core.if_def
 
-theorem excluded_middle : ∀ A : eta bool, eps (bor A (bnot A))
+theorem excluded_middle : Π A : eta bool, eps (bor A (bnot A))
 proof
 admit
diff --git a/alternatives/prelude/core/equalities.lp b/alternatives/prelude/core/equalities.lp
index 863cc7dce0afcc8df18bec9a0fd9cb5d44f431c1..00cd5546b2226a0582b20b638b511a28183129c9 100644
--- a/alternatives/prelude/core/equalities.lp
+++ b/alternatives/prelude/core/equalities.lp
@@ -1,3 +1,3 @@
 require open encodings.pvs_core prelude.core.booleans
 
-symbol eq {T : Type} : eta T ⇒ eta T ⇒ eta bool
+symbol eq {T : Type} : eta T → eta T → eta bool
diff --git a/alternatives/prelude/core/if_def.lp b/alternatives/prelude/core/if_def.lp
index 6e4868bebcdbb119e3b13cb8d76c36e877e8b479..6458644b088382efa8f80f83c5a7da948fe09d1f 100644
--- a/alternatives/prelude/core/if_def.lp
+++ b/alternatives/prelude/core/if_def.lp
@@ -1,4 +1,4 @@
 require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
 prelude.core.notequal
 
-symbol if {T:Type}: η bool ⇒ eta T ⇒ eta T ⇒ eta T
+symbol if {T:Type}: η bool → eta T → eta T → eta T
diff --git a/alternatives/prelude/core/quantifier_props.lp b/alternatives/prelude/core/quantifier_props.lp
index b803f5fc4b3931039a9a8d0e45a41c3d899c0370..73ac1975b5cc3bf1dc5b7f4821711a1e6ca4211e 100644
--- a/alternatives/prelude/core/quantifier_props.lp
+++ b/alternatives/prelude/core/quantifier_props.lp
@@ -1,16 +1,16 @@
 require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
 
-definition exists {T: Type} (p : eta T ⇒ eta bool) ≔
+definition exists {T: Type} (p : eta T → eta bool) ≔
     (bnot (all T (λ x, (bnot (p x)))))
 
 set declared "∃"
 definition ∃ {T: Type} ≔ @exists T
 
-theorem exists_not (T: Type) (p: η T ⇒ η bool):
+theorem exists_not (T: Type) (p: η T → η bool):
   ε (eq (∃ (λ x, ¬ (p x))) (¬ (all T p)))
 proof
 admit
 
-theorem exists_or (T: Type) (p q: η T ⇒ η bool):
+theorem exists_or (T: Type) (p q: η T → η bool):
   ε (eq (∃ (λ x, (p x) ∨ (q x))) ((∃ p) ∨ (∃ q)))
 proof admit
diff --git a/alternatives/sandbox/core/rat.lp b/alternatives/sandbox/core/rat.lp
index 94fb232afa0007d6c39cc5fb157abc949853ebee..34c84542d7970438778f83e6767fbf7828f12975 100644
--- a/alternatives/sandbox/core/rat.lp
+++ b/alternatives/sandbox/core/rat.lp
@@ -7,14 +7,14 @@ constant symbol zrat : η rat
 
 definition intnz ≔ psub int (λ x, neq 0 x)
 
-symbol frac : η int ⇒ η intnz ⇒ η rat
+symbol frac : η int → η intnz → η rat
 
-symbol times : η rat ⇒ η rat ⇒ η rat
+symbol times : η rat → η rat → η rat
 set infix 5 "*" ≔ times
-rule times (frac &a &b) (frac &c &d) → frac (N.times &a &c) (N.times &b &d)
+rule times (frac $a $b) (frac $c $d) ↪ frac (N.times $a $c) (N.times $b $d)
 
-symbol rateq : η rat ⇒ η rat ⇒ η bool
-rule rateq (frac &a &b) (frac &c &d) → eq (N.times &a &d) (N.times &b &c)
+symbol rateq : η rat → η rat → η bool
+rule rateq (frac $a $b) (frac $c $d) ↪ eq (N.times $a $d) (N.times $b $c)
 
 theorem right_cancellation (a : η int) (b : η intnz) :
   ε (rateq ((frac a b) * (frac b 1)) (frac a 1))
diff --git a/alternatives/sandbox/core/rat_explicit.lp b/alternatives/sandbox/core/rat_explicit.lp
index 4a03b1df40283a31ef4b2804c8e6b5f55d01c53c..9295fab3916c7a7af3d77736fb0c5feae72c9c3b 100644
--- a/alternatives/sandbox/core/rat_explicit.lp
+++ b/alternatives/sandbox/core/rat_explicit.lp
@@ -7,17 +7,17 @@ constant symbol zero : η rat
 
 symbol frac (_ m : η int) (pi : ε (neq m 0)) : η rat
 
-symbol div : η rat ⇒ η rat ⇒ η rat
-symbol times : η rat ⇒ η rat ⇒ η rat
+symbol div : η rat → η rat → η rat
+symbol times : η rat → η rat → η rat
 set infix 5 "*" ≔ times
 set infix 6 "/" ≔ div
 
-rule times (frac &A &B &X) (frac &C &D &Y) →
-  frac (N.times &A &C) (N.times &B &D) (N.prod_not_zero &B &D &X &Y)
+rule times (frac $A $B $X) (frac $C $D $Y) ↪
+  frac (N.times $A $C) (N.times $B $D) (N.prod_not_zero $B $D $X $Y)
 
-symbol rateq : η rat ⇒ η rat ⇒ η Prop
-rule rateq (frac &A &B _) (frac &C &D _) →
-  eq (N.times &A &D) (N.times &B &C)
+symbol rateq : η rat → η rat → η Prop
+rule rateq (frac $A $B _) (frac $C $D _) ↪
+  eq (N.times $A $D) (N.times $B $C)
 
 // (a/b) * (b/1) = (a/1)
 theorem right_cancellation (a b : η int) (pi : ε (neq b 0)) (pi' : ε (neq 1 0)):
diff --git a/encodings/ad_hoc.lp b/encodings/ad_hoc.lp
index 03028c01b3b49f5da1fc569318c3a917969f3bc0..fbbd9d3df33a7cac44ce614f8f0fa23daf02fdae 100644
--- a/encodings/ad_hoc.lp
+++ b/encodings/ad_hoc.lp
@@ -4,8 +4,8 @@ require open personoj.encodings.pvs_cert
 require personoj.encodings.prenex as P
 require open personoj.encodings.subtype
 
-constant symbol forallS: Set ⇒ (Set ⇒ Scheme) ⇒ Scheme
-rule P.χ (forallS &T &C) → ∀U: Set, ε (U ⊑ &T) ⇒ P.χ (&C U)
+constant symbol forallS: Set → (Set → Scheme) → Scheme
+rule P.χ (forallS $T $C) ↪ ΠU: Set, ε (U ⊑ $T) → P.χ ($C U)
 
-constant symbol forallB: Set ⇒ (Set ⇒ Bool) ⇒ Bool
-rule ε (forallB &T &C) → ∀U: Set, ε (U ⊑ &T) ⇒ ε (&C U)
+constant symbol forallB: Set → (Set → Bool) → Bool
+rule ε (forallB $T $C) ↪ ΠU: Set, ε (U ⊑ $T) → ε ($C U)
diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
index ac2f5c121fc93b5263e88d2f918ebb40b230f73f..383773dc5b410cfb6dd10662b3c97363cf134bdb 100644
--- a/encodings/bool_hol.lp
+++ b/encodings/bool_hol.lp
@@ -11,8 +11,8 @@ set prefix 5 "¬" ≔ not
 definition imp P Q ≔ impd {P} Q
 set infix 2 "⊃" ≔ imp
 
-definition {|and|} P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
-set infix 4 "∧" ≔ {|and|}
+definition and P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
+set infix 4 "∧" ≔ and
 definition or P Q ≔ (¬ P) ⊃ Q
 set infix 3 "∨" ≔ or
 
@@ -20,8 +20,8 @@ set builtin "bot" ≔ false
 set builtin "top" ≔ true
 set builtin "not" ≔ not
 set builtin "imp" ≔ imp
-set builtin "and" ≔ {|and|}
+set builtin "and" ≔ and
 set builtin "or"  ≔ or
 
-symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
-rule if {bool} &p &then &else → (&p ⊃ &then) ⊃ (λ_, ¬ &p ⊃ &else)
+symbol if {s: Set} p: (ε p → η s) → (ε (¬ p) → η s) → η s
+rule if {bool} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
diff --git a/encodings/bool_pvs.lp b/encodings/bool_pvs.lp
index 00941455718072b284cae6d81e5ba88bd3eaaab3..b94bc4434a23a79108d4f56df9e02f9b23d69ae8 100644
--- a/encodings/bool_pvs.lp
+++ b/encodings/bool_pvs.lp
@@ -6,20 +6,20 @@ require open personoj.encodings.pvs_cert
 definition false ≔ forall {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
 
-symbol eq {s: Set}: η s ⇒ η s ⇒ η bool
+symbol eq {s: Set}: η s → η s → η bool
 set infix left 6 "=" ≔ eq
 
 definition not p ≔ eq {bool} p false
 set prefix 5 "¬" ≔ not
 
-constant symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
-rule ε (if &p &then &else)
-   → (∀h: ε &p, ε (&then h)) ⇒ ∀h: ε (¬ &p), ε (&else h)
+constant symbol if {s: Set} p: (ε p → η s) → (ε (¬ p) → η s) → η s
+rule ε (if $p $then $else)
+   ↪ (Πh: ε $p, ε ($then h)) → Πh: ε (¬ $p), ε ($else h)
 
-definition {|and|} p q ≔ if {bool} p q (λ_, false)
+definition and p q ≔ if {bool} p q (λ_, false)
 definition or p q ≔ if {bool} p (λ_, true) q
 definition imp p q ≔ if {bool} p q (λ_, true)
-set infix left 4 "∧" ≔ {|and|}
+set infix left 4 "∧" ≔ and
 set infix left 3 "∨" ≔ or
 set infix left 2 "⊃" ≔ imp
 
@@ -27,5 +27,5 @@ set builtin "bot" ≔ false
 set builtin "top" ≔ true
 set builtin "not" ≔ not
 set builtin "imp" ≔ imp
-set builtin "and" ≔ {|and|}
+set builtin "and" ≔ and
 set builtin "or"  ≔ or
diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index 0f48d20b8f247336184e9bbac70acefc85dff921..7f460ed1b17acf75872c4551a5303e51c8b31bbb 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -1,6 +1,6 @@
 // PVS cert with functional PTS
 constant symbol Sort : TYPE
-constant symbol Univ : Sort ⇒ TYPE
+constant symbol Univ : Sort → TYPE
 
 constant symbol Kind : Sort
 constant symbol Type : Sort
@@ -16,37 +16,37 @@ constant symbol uType : Univ Kind
 // (Prop, Prop, Prop), (Type, Type, Type), (Type, Prop, Prop)
 // Since the PTS is functional, [Rule s1 s2] rewrites the the 3rd element
 // of the rule.
-symbol Rule : Sort ⇒ Sort ⇒ Sort
-rule Rule Prop Prop → Prop
- and Rule Type Type → Type
- and Rule Type Prop → Prop
+symbol Rule : Sort → Sort → Sort
+rule Rule Prop Prop ↪ Prop
+ and Rule Type Type ↪ Type
+ and Rule Type Prop ↪ Prop
 
 // [Term s t] decodes term [t] of encoded sort [s]
-injective symbol Term {s: Sort}: Univ s ⇒ TYPE
-rule Term uProp → Univ Prop
- and Term uType → Univ Type
+injective symbol Term {s: Sort}: Univ s → TYPE
+rule Term uProp ↪ Univ Prop
+ and Term uType ↪ Univ Type
 
 // [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)
+  (Term A → Univ sB) → Univ (Rule sA sB)
 
-rule Term (prod {&sA} {&sB} &A &B) → ∀x: Term {&sA} &A, Term {&sB} (&B x)
+rule Term (prod {$sA} {$sB} $A $B) ↪ Πx: Term {$sA} $A, Term {$sB} ($B x)
 
 // Predicate subtyping
 // can be seen as a dependant pair type with
 // - first element is a term of some type [A] and
 // - second is a predicate on [A] verified by the first element.
-constant symbol Psub {T: Term uType}: (Term T ⇒ Term uProp) ⇒ Term uType
+constant symbol Psub {T: Term uType}: (Term T → Term uProp) → Term uType
 
 // Γ ⊢ M : { v : T | P }
 // —————————————————————PROJl
 //      Γ ⊢ fst(M) : T
-symbol fst {T: Univ Type} {P: Term T ⇒ Univ Prop}: Term (Psub P) ⇒ Term T
+symbol fst {T: Univ Type} {P: Term T → Univ Prop}: Term (Psub P) → Term T
 
 //  Γ ⊢ M : { v : T | P }
 // ——————————————————————————PROJr
 // Γ ⊢ snd(M) : P[v ≔ fst(M)]
-constant symbol snd {T: Univ Type} {P: Term T ⇒ Univ Prop}
+constant symbol snd {T: Univ Type} {P: Term T → Univ Prop}
   (M: Term (Psub P)):
   Term (P (fst M))
 
@@ -55,31 +55,31 @@ constant symbol snd {T: Univ Type} {P: Term T ⇒ Univ Prop}
 // Γ ⊢ M : T    Γ ⊢ N : P[v ≔ M]    Γ ⊢ { v : T | P }
 // ——————————————————————————————————————————————————PAIR
 //           Γ ⊢ ⟨M, N⟩ : {v : T | P}
-symbol pair {T: Univ Type} (P: Term T ⇒ Univ Prop) (M: Term T):
-  Term (P M) ⇒ Term (Psub P)
+symbol pair {T: Univ Type} (P: Term T → Univ Prop) (M: Term T):
+  Term (P M) → Term (Psub P)
 
 // opair is a pair forgetting its snd argument
-protected symbol opair (T: Univ Type) (P: Term T ⇒ Univ Prop) (M: Term T):
+protected symbol opair (T: Univ Type) (P: Term T → Univ Prop) (M: Term T):
   Term (Psub P)
 
 // Two pairs are convertible if their first element is
-rule pair {&T} &P &M _ → opair &T &P &M
+rule pair {$T} $P $M _ ↪ opair $T $P $M
 
-rule fst (opair _ _ &M) → &M
-// and opair _ &P (fst {_} {&P} &X) → &X // Surjective pairing
+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
+symbol subtype: Term uType → Term uType → Term uProp
 set infix left 6 "⊑" ≔ subtype
 
 // [↑ {T} U p t] casts element [t] from type [T] to type [U] given
 // the proof [p] that [T] is a subtype of [U]
 set declared "↑"
-symbol ↑ {T: Term uType} (U: Term uType): Term (T ⊑ U) ⇒ Term T ⇒ Term U
-rule ↑ {&T} &T _ &x → &x // Identity cast
+symbol ↑ {T: Term uType} (U: Term uType): Term (T ⊑ U) → Term T → Term U
+rule ↑ {$T} $T _ $x ↪ $x // Identity cast
 // NOTE: a cast from a type [{x: A | P}] to type [A] is a [fst],
-and ↑ {Psub {&T} &P} &T _ → fst {&T} {&P}
+and ↑ {Psub {$T} $P} $T _ ↪ fst {$T} {$P}
 // and a "downcast" is the pair constructor
 set declared "↓"
 
diff --git a/encodings/deferred.lp b/encodings/deferred.lp
index 877588854926bd17378f001d948215c575812622..a004713b5ff3fe539f5bf0c6004bf5a61e66179d 100644
--- a/encodings/deferred.lp
+++ b/encodings/deferred.lp
@@ -5,19 +5,19 @@ require open
   personoj.encodings.booleans
 
 /// Type carried with  the encoded terms
-constant symbol t: Set ⇒ TYPE
-constant symbol quote {T: Set}: η T ⇒ t T
-injective symbol unquote {T: Set}: t T ⇒ η T
-rule unquote (quote &t) → &t
+constant symbol t: Set → TYPE
+constant symbol quote {T: Set}: η T → t T
+injective symbol unquote {T: Set}: t T → η T
+rule unquote (quote $t) ↪ $t
 
 // Coding of applied types
-constant symbol APP: Set ⇒ ∀U: Set, t U ⇒ Set
-rule η (APP (arrd {&T} &bU) &T &y) → η (&bU (unquote &y))
+constant symbol APP: Set → ΠU: Set, t U → Set
+rule η (APP (arrd {$T} $bU) $T $y) ↪ η ($bU (unquote $y))
 
 // Quoted terms application
-constant symbol app {T: Set} {S: Set}: t T ⇒ ∀y: t S, t (APP T S y)
-rule unquote (app {arrd {&a} &b} {&a} &t &u) → (unquote &t) (unquote &u)
+constant symbol app {T: Set} {S: Set}: t T → Πy: t S, t (APP T S y)
+rule unquote (app {arrd {$a} $b} {$a} $t $u) ↪ (unquote $t) (unquote $u)
 
-constant symbol p: Bool ⇒ TYPE
-constant symbol quote_p {P: Bool}: ε P ⇒ p P
-symbol unquote_p {P: Bool}: p P ⇒ ε P
+constant symbol p: Bool → TYPE
+constant symbol quote_p {P: Bool}: ε P → p P
+symbol unquote_p {P: Bool}: p P → ε P
diff --git a/encodings/deferred_erasure.lp b/encodings/deferred_erasure.lp
index 81efc1587b343f772c4694aaa9e0f0005743dede..6dbc56c4863302a7a0f1861e90c809953c37292b 100644
--- a/encodings/deferred_erasure.lp
+++ b/encodings/deferred_erasure.lp
@@ -7,20 +7,20 @@ require open
   personoj.encodings.booleans
 
 constant symbol t: TYPE
-constant symbol quote {T: Set}: η T ⇒ t
-injective symbol app: t ⇒ t ⇒ t
-constant symbol abs: (t ⇒ t) ⇒ t
+constant symbol quote {T: Set}: η T → t
+injective symbol app: t → t → t
+constant symbol abs: (t → t) → t
 
-rule app (abs &b) &a → &b &a
+rule app (abs $b) $a ↪ $b $a
 
-symbol unquote (T: Set): t ⇒ η T
-symbol quote_B {P: Bool}: ε P ⇒ t
-symbol unquote_B (P: Bool): t ⇒ ε P
+symbol unquote (T: Set): t → η T
+symbol quote_B {P: Bool}: ε P → t
+symbol unquote_B (P: Bool): t → ε P
 
-rule unquote (arrd &b) &f &x → unquote (&b &x) (app &f (quote &x))
- and unquote_B (impd &b) &h &x → unquote_B (&b &x) (app &h (quote_B &x))
- and unquote_B (forall &b) &f &x → unquote_B (&b &x) (app &f (quote &x))
+rule unquote (arrd $b) $f $x ↪ unquote ($b $x) (app $f (quote $x))
+ and unquote_B (impd $b) $h $x ↪ unquote_B ($b $x) (app $h (quote_B $x))
+ and unquote_B (forall $b) $f $x ↪ unquote_B ($b $x) (app $f (quote $x))
 
-symbol if (T: Set) (p: Bool): t ⇒ t ⇒ η T
-rule if &T true &then _ → unquote &T &then
- and if &T false _ &else → unquote &T &else
+symbol if (T: Set) (p: Bool): t → t → η T
+rule if $T true $then _ ↪ unquote $T $then
+ and if $T false _ $else ↪ unquote $T $else
diff --git a/encodings/equality.lp b/encodings/equality.lp
index 961a81b001b0d791982509a1e798dfa7bc64ef20..2714fb14fef6cc594db791db7d8c823a75329013 100644
--- a/encodings/equality.lp
+++ b/encodings/equality.lp
@@ -1,5 +1,5 @@
 require open personoj.encodings.lhol
 
-symbol eq {T: Set}: η T ⇒ η T ⇒ Bool
+symbol eq {T: Set}: η T → η T → Bool
 set infix left 6 "=" ≔ eq
 set builtin "eq" ≔ eq
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index a4f4793fb2221a9a8f98682b74ba954e63b0b723..51cf4439a98fd3ddad142427b90b62523e12e5f9 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -6,26 +6,26 @@ symbol Bool: TYPE
 set declared "Ï•"
 set declared "η"
 set declared "ε"
-injective symbol ϕ: Kind ⇒ TYPE
-injective symbol η: Set ⇒ TYPE
-injective symbol ε: Bool ⇒ TYPE
+injective symbol ϕ: Kind → TYPE
+injective symbol η: Set → TYPE
+injective symbol ε: Bool → TYPE
 
 symbol {|set|}: Kind
 symbol bool: Set
 
-rule ϕ {|set|} → Set
-rule η bool → Bool
+rule ϕ {|set|} ↪ Set
+rule η bool ↪ Bool
 
-symbol forall {x: Set}: (η x ⇒ Bool) ⇒ Bool
-symbol impd {x: Bool}: (ε x ⇒ Bool) ⇒ Bool
-symbol arrd {x: Set}: (η x ⇒ Set) ⇒ Set
+symbol forall {x: Set}: (η x → Bool) → Bool
+symbol impd {x: Bool}: (ε x → Bool) → Bool
+symbol arrd {x: Set}: (η x → Set) → Set
 
-rule ε (forall {&X} &P) → ∀x: η &X, ε (&P x)
- and ε (impd {&H} &P) → ∀h: ε &H, ε (&P h)
- and η (arrd {&X} &T) → ∀x: η &X, η (&T x)
+rule ε (forall {$X} $P) ↪ Πx: η $X, ε ($P x)
+with ε (impd {$H} $P) ↪ Πh: ε $H, ε ($P h)
+with η (arrd {$X} $T) ↪ Πx: η $X, η ($T x)
 
-symbol arr: Set ⇒ Set ⇒ Set
-rule η (arr &X &Y) → (η &X) ⇒ (η &Y)
+symbol arr: Set → Set → Set
+rule η (arr $X $Y) ↪ (η $X) → (η $Y)
 set infix right 6 "~>" ≔ arr
 
 set builtin "T" ≔ η
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index 7c701eaf8f14317a143c9729b9c1355addc268de..b6222b04d43b485a866deb03a3a77e6d89b37e13 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -5,12 +5,12 @@ require open personoj.encodings.pvs_cert
 set declared "χ"
 set declared "∇"
 symbol Scheme: TYPE
-symbol χ: Scheme ⇒ TYPE
-symbol ∇: Set ⇒ Scheme
-rule χ (∇ &X) → η &X
+symbol χ: Scheme → TYPE
+symbol ∇: Set → Scheme
+rule χ (∇ $X) ↪ η $X
 
-constant symbol forallS: (Set ⇒ Scheme) ⇒ Scheme
-rule χ (forallS &p) → ∀T: Set, χ (&p T)
+constant symbol forallS: (Set → Scheme) → Scheme
+rule χ (forallS $p) ↪ ΠT: Set, χ ($p T)
 
-constant symbol forallB: (Set ⇒ Bool) ⇒ Bool
-rule ε (forallB &P) → ∀x: Set, ε (&P x)
+constant symbol forallB: (Set → Bool) → Bool
+rule ε (forallB $P) ↪ Πx: Set, ε ($P x)
diff --git a/encodings/pvs_cert.lp b/encodings/pvs_cert.lp
index 3e550d942ea386debf158b2516aac2c8188a34ac..de273a910949968ee5759f966e250e52ee3443c4 100644
--- a/encodings/pvs_cert.lp
+++ b/encodings/pvs_cert.lp
@@ -1,19 +1,19 @@
 // PVS-Cert
 require open personoj.encodings.lhol
 
-constant symbol psub {x: Set}: (η x ⇒ Bool) ⇒ Set
-symbol pair: ∀{t: Set} {p: η t ⇒ Bool} (m: η t), ε (p m) ⇒ η (psub p)
-symbol fst: ∀{t: Set} {p: η t ⇒ Bool}, η (psub p) ⇒ η t
+constant symbol psub {x: Set}: (η x → Bool) → Set
+symbol pair: Π{t: Set} {p: η t → Bool} (m: η t), ε (p m) → η (psub p)
+symbol fst: Π{t: Set} {p: η t → Bool}, η (psub p) → η t
 
-symbol snd {t: Set}{p: η t ⇒ Bool} (m: η (psub p)): ε (p (fst m))
+symbol snd {t: Set}{p: η t → Bool} (m: η (psub p)): ε (p (fst m))
 
 // Proof irrelevance
-protected symbol ppair: ∀{t: Set} {p: η t ⇒ Bool}, η t ⇒ η (psub p)
+protected symbol ppair: Π{t: Set} {p: η t → Bool}, η t → η (psub p)
 
 // Reduction
-rule pair &X _ → ppair &X
-rule fst (ppair &M) → &M
+rule pair $X _ ↪ ppair $X
+rule fst (ppair $M) ↪ $M
 
 // Sub-typing relation
-symbol subtype : Set ⇒ Set ⇒ Bool
+symbol subtype : Set → Set → Bool
 set infix left 6 "⊑" ≔ subtype
diff --git a/encodings/pvs_cert_minus.lp b/encodings/pvs_cert_minus.lp
index 2ad17267324f203b62847b1ece2ad9e27e3de216..fb0f7d0ddebf24bd596557dba0bc9c4b34b3389d 100644
--- a/encodings/pvs_cert_minus.lp
+++ b/encodings/pvs_cert_minus.lp
@@ -2,12 +2,12 @@
 require open personoj.encodings.lhol
 
 set declared "Σ"
-constant symbol Σ (T : Set): (η T ⇒ Set) ⇒ Set
-constant symbol pair {T: Set} {U: η T ⇒ Set} (M: η T) (_: η (U M))
+constant symbol Σ (T : Set): (η T → Set) → Set
+constant symbol pair {T: Set} {U: η T → Set} (M: η T) (_: η (U M))
 : η (Σ T U)
 
-symbol fst {T: Set} {U: η T ⇒ Set}: η (Σ T U) ⇒ η T
-rule fst (pair &M _) → &M
+symbol fst {T: Set} {U: η T → Set}: η (Σ T U) → η T
+rule fst (pair $M _) ↪ $M
 
-symbol snd {T: Set} {U: η T ⇒ Set} (M: η (Σ T U)): η (U (fst M))
-rule snd (pair _ &N) → &N
+symbol snd {T: Set} {U: η T → Set} (M: η (Σ T U)): η (U (fst M))
+rule snd (pair _ $N) ↪ $N
diff --git a/encodings/pvs_core.lp b/encodings/pvs_core.lp
index c54b8bba2aaee420c9e8c685f5dd5103c1308bbc..219ef31241d5873feba35dfa4553d8043d31ebe4 100644
--- a/encodings/pvs_core.lp
+++ b/encodings/pvs_core.lp
@@ -1,42 +1,42 @@
 constant symbol Type : TYPE
 constant symbol Prop : Type
 
-injective symbol eta : Type ⇒ TYPE
-injective symbol eps : eta Prop ⇒ TYPE
+injective symbol eta : Type → TYPE
+injective symbol eps : eta Prop → TYPE
 set declared "η"
 set declared "ε"
 definition ε ≔ eps
 definition η ≔ eta
 
-symbol arr : Type ⇒ Type ⇒ Type
+symbol arr : Type → Type → Type
 set infix right 6 "~>" ≔ arr
 
-rule eta (&A ~> &B) → eta &A ⇒ eta &B
+rule eta ($A ~> $B) ↪ eta $A → eta $B
 
-// symbol psub : ∀ A : Type, eta (A ~> Prop) ⇒ Type
-symbol psub : ∀ A : Type, (eta A ⇒ eta Prop) ⇒ Type
+// symbol psub : Π A : Type, eta (A ~> Prop) → Type
+symbol psub : Π A : Type, (eta A → eta Prop) → Type
 
-constant symbol cast : Type ⇒ Type
-rule eta (cast (psub &A _)) → eta &A
+constant symbol cast : Type → Type
+rule eta (cast (psub $A _)) ↪ eta $A
 
 symbol psubElim1 (A : Type) (P : eta (A ~> Prop)):
-  eta (psub A P) ⇒ eta A
+  eta (psub A P) → eta A
 
 symbol imp : eta (Prop ~> Prop ~> Prop)
 set infix right 6 "I>" ≔ imp
 
-symbol impIntro : ∀ (p q : eta Prop), (eps p ⇒ eps q) ⇒ eps (p I> q)
-symbol impElim : ∀ p q : eta Prop, eps (p I> q) ⇒ eps p ⇒ eps q
+symbol impIntro : Π (p q : eta Prop), (eps p → eps q) → eps (p I> q)
+symbol impElim : Π p q : eta Prop, eps (p I> q) → eps p → eps q
 
-symbol all (A : Type): eta (A ~> Prop) ⇒ eta Prop
-rule eta (all &A &P) → ∀ x : eta &A, eta (&P x)
+symbol all (A : Type): eta (A ~> Prop) → eta Prop
+rule eta (all $A $P) ↪ Π x : eta $A, eta ($P x)
 
 // Forall intro
 symbol allIntro (A: Type) (p: eta (A ~> Prop)) (x: eta A):
-  eps (p x) ⇒ eps (all A p)
+  eps (p x) → eps (all A p)
 // Forall elim
 symbol allElim (A: Type) (t: eta A) (p: eta (A ~> Prop)):
-  eps (all A p) ⇒ eps (p t)
+  eps (all A p) → eps (p t)
 
 // Subtype elim 2
 symbol psubElim (A: Type) (p: η (A ~> Prop)) (t: η (cast (psub A p))):
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 9aabd5a54655ee57d03caec74c3e278dccddad3c..2b15562dde6fd13a98e054775dcd95d48cfdb3b6 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -9,42 +9,43 @@ set declared "μ₀"
 set declared "Ï€"
 
 symbol S_Refl (a: Set): ε (a ⊑ a)
-symbol S_Trans (s t u: Set): ε (s ⊑ t) ⇒ ε (t ⊑ u) ⇒ ε (s ⊑ u)
+symbol S_Trans (s t u: Set): ε (s ⊑ t) → ε (t ⊑ u) → ε (s ⊑ u)
 
-symbol S_Restr {a: Set} (p: η a ⇒ Bool): ε (psub p ⊑ a)
+symbol S_Restr {a: Set} (p: η a → Bool): ε (psub p ⊑ a)
 
-symbol S_Arr (t u1 u2: Set): ε (u1 ⊑ u2) ⇒ ε ((t ~> u1) ⊑ (t ~> u2))
-symbol S_Darr (d: Set) (r1: η d ⇒ Set) (r2: η d ⇒ Set)
-: ε (forall (λx, (r1 x) ⊑ (r2 x))) ⇒ ε ((arrd r1) ⊑ (arrd r2))
+symbol S_Arr (t u1 u2: Set): ε (u1 ⊑ u2) → ε ((t ~> u1) ⊑ (t ~> u2))
+symbol S_Darr (d: Set) (r1: η d → Set) (r2: η d → Set)
+     : ε (forall (λx, (r1 x) ⊑ (r2 x))) → ε ((arrd r1) ⊑ (arrd r2))
 
 // Maximal supertype
-symbol μ: Set ⇒ Set
-rule μ (psub {&T} _) → μ &T
- and μ (&T ~> &U) → &T ~> (μ &U)
- and μ (μ &T) → μ &T // FIXME: can be proved
+symbol μ: Set → Set
+rule μ (psub {$T} _) ↪ μ $T
+with μ ($T ~> $U) ↪ $T ~> (μ $U)
+with μ (μ $T) ↪ μ $T // FIXME: can be proved
 // Direct super-type
-symbol μ₀: Set ⇒ Set
-rule μ₀ (psub {&T} _) → μ₀ &T
+symbol μ₀: Set → Set
+rule μ₀ (psub {$T} _) ↪ μ₀ $T
 
 compute λT: Set, μ (μ T)
 
 // Constraints
-symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
+symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) → η A → η B
 definition ↑ {A} {B} ≔ upcast {A} {B}
-rule upcast {&t} {&t} _ &x → &x
+rule upcast {$t} {$t} _ $x ↪ $x
 
 theorem sub_of_sup A: ε (A ⊑ μ A)
 proof
 admit
 
-symbol π {T: Set}: η (μ T) ⇒ Bool
+symbol π {T: Set}: η (μ T) → Bool
 symbol downcast {A: Set} {B: Set} (_: ε (B ⊑ A))
-                (a: η A) (_: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a))): η B
+                (a: η A) (_: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a)))
+     : η B
 definition ↓ {A} {B} ≔ downcast {A} {B}
 
 set flag "print_implicits" on
-rule π {&T ~> &U} → λx: η &T ⇒ η (μ &U), forall (λy, π {&U} (x y))
-// rule π {psub {&T} &a} → λx: η (μ &T), π {&T} x
-rule π {psub {&T} &a}
-   → λx: η (μ &T), (π {&T} x) ∧ (λy: ε (π {&T} x), &a (↓ {μ &T} {&T} _ x y))
-// FIXME: does not type check because μ (μ &T) is not reduced to μ &T
+rule π {$T ~> $U} ↪ λx: η $T → η (μ $U), forall (λy, π {$U} (x y))
+// rule π {psub {$T} $a} ↪ λx: η (μ $T), π {$T} x
+rule π {psub {$T} $a}
+   ↪ λx: η (μ $T), (π {$T} x) ∧ (λy: ε (π {$T} x), $a (↓ {μ $T} {$T} _ x y))
+// FIXME: does not type check because μ (μ $T) is not reduced to μ $T
diff --git a/paper/rat.lp b/paper/rat.lp
index 2596d33578d1db69b9051ce9214d37a11cf3f361..cd34b423a0e26bc1813cab6b38cf3b82f24d477d 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -20,23 +20,24 @@ set infix left 4 "+" ≔ plus_nat
 symbol times_nat: η (ℕ ~> ℕ ~> ℕ)
 set infix left 5 "*" ≔ times_nat
 // Some properties of product
-rule Z + &n → &n
- and &m + S &n → S (&m + &n)
- and &n + Z → &n
- and S &m + &n → S (&m + &n)
-rule Z * _ → Z
- and &m * (S &n) → &m + (&m * &n)
- and _ * Z → Z
- and (S &m) * &n → &n + (&m * &n)
-
-symbol nat_induction: ∀P: η ℕ ⇒ Bool, ε (P 0) ⇒ (∀n, ε (P n) ⇒ ε (P (S n))) ⇒ ∀n, ε (P n)
-
-symbol ¬: Bool ⇒ Bool
-rule ε (¬ &x) → ε &x ⇒ ∀(z: Bool), ε z
+rule Z + $n ↪ $n
+with $m + S $n ↪ S ($m + $n)
+with $n + Z ↪ $n
+with S $m + $n ↪ S ($m + $n)
+rule Z * _ ↪ Z
+with $m * (S $n) ↪ $m + ($m * $n)
+with _ * Z ↪ Z
+with (S $m) * $n ↪ $n + ($m * $n)
+
+symbol nat_induction: ΠP: η ℕ → Bool,
+                        ε (P 0) → (Πn, ε (P n) → ε (P (S n))) → Πn, ε (P n)
+
+symbol ¬: Bool → Bool
+rule ε (¬ $x) ↪ ε $x → Π(z: Bool), ε z
 symbol eqnat: η (ℕ ~> ℕ ~> bool)
 set infix left 3 "=ℕ" ≔ eqnat
 
-symbol s_not_z: ∀x: η ℕ, ε (¬ (Z =ℕ (S x)))
+symbol s_not_z: Πx: η ℕ, ε (¬ (Z =ℕ (S x)))
 
 theorem times_comm: ε (forall (λa, forall (λb, (a * b) =ℕ (b * a))))
 proof
@@ -47,30 +48,31 @@ definition ℕ* ≔ psub {|nznat?|}
 
 definition Onz ≔ pair {ℕ} {{|nznat?|}} (S Z) (s_not_z Z) // One not zero
 
-symbol Snz: η ℕ* ⇒ η ℕ* // Successor not zero
+symbol Snz: η ℕ* → η ℕ* // Successor not zero
 symbol nznat_induction:
-  ∀P: η ℕ* ⇒ Bool, ε (P Onz) ⇒ (∀n, ε (P n) ⇒ ε (P (Snz n))) ⇒ ∀n, ε (P n)
+  ΠP: η ℕ* → Bool, ε (P Onz) → (Πn, ε (P n) → ε (P (Snz n))) → Πn, ε (P n)
 
 symbol div: η (ℕ ~> ℕ* ~> ℚ+)
 set infix left 6 "/" ≔ div
 
 symbol eqrat: η (ℚ+ ~> ℚ+ ~> bool)
 set infix left 7 "=ℚ" ≔ eqrat
-rule (&a / &b) =ℚ (&c / &d) → (&a * (fst &d)) =ℕ ((fst &b) * &c)
+rule ($a / $b) =ℚ ($c / $d) ↪ ($a * (fst $d)) =ℕ ((fst $b) * $c)
 
 definition imp P Q ≔ impd {P} (λ_, Q)
 set infix left 6 "⊃" ≔ imp
 definition false ≔ forall {bool} (λx, x)
 
-theorem nzprod: ε (forall
-                     {â„•*}
-                     (λx, forall {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
+theorem nzprod:
+  ε (forall
+       {â„•*}
+       (λx, forall {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
 proof
   refine nznat_induction
-         (λx, forall (λy: η ℕ*, (Z =ℕ (fst x * fst y)) ⊃ false)) ?xOnz ?xSnz
+           (λx, forall (λy: η ℕ*, (Z =ℕ (fst x * fst y)) ⊃ false)) ?xOnz ?xSnz
   // x = 1
   refine nznat_induction
-         (λy, (Z =ℕ (fst Onz * fst y)) ⊃ false) ?yOnz ?ySnz
+           (λy, (Z =ℕ (fst Onz * fst y)) ⊃ false) ?yOnz ?ySnz
   simpl
   apply s_not_z Z
   // x = S n
@@ -79,17 +81,17 @@ proof
   refine snd (Snz n)
   assume n Hn
   refine nznat_induction
-         (λz, (Z =ℕ (fst (Snz n) * (fst z))) ⊃ false) ?zOnz[n,Hn] ?zSnz[n,Hn]
+           (λz, (Z =ℕ (fst (Snz n) * (fst z))) ⊃ false) ?zOnz[n,Hn] ?zSnz[n,Hn]
   simpl
   refine snd (Snz n)
   assume m Hm
 admit
 
 symbol times_rat: η (ℚ+ ~> ℚ+ ~> ℚ+)
-rule times_rat (&a / &b) (&c / &d) →
-  let denom ≔ fst &b * (fst &d) in
-  let prf ≔ nzprod &b &d in
-  (&a * &c) / (pair denom prf)
+rule times_rat ($a / $b) ($c / $d) ↪
+  let denom ≔ fst $b * (fst $d) in
+  let prf ≔ nzprod $b $d in
+  ($a * $c) / (pair denom prf)
 
 theorem right_cancel:
   ε (forall
diff --git a/prelude/functions.lp b/prelude/functions.lp
index 4d42e7d5d565212f2ac4d698b196f3a47e4e5c1d..8c0f07af1cebe09a179606d2632e4eed5a66b6e3 100644
--- a/prelude/functions.lp
+++ b/prelude/functions.lp
@@ -31,7 +31,7 @@ proof
 admit
 
 symbol domain {D: Term uType} {R: Term uType} (f: Term (D ~> R)): Term uType
-rule domain {&D} {_} _ → &D
+rule domain {$D} {_} _ ↪ $D
 
 //
 // restrict[T: TYPE, S: TYPE FROM T, R: TYPE]
@@ -39,10 +39,10 @@ rule domain {&D} {_} _ → &D
 symbol restrict {T: Term uType} (S: Term uType) {R: Term uType}
                 (f: Term (T ~> R)) (_: Term (S ⊑ T)) (s: Term S):
   Term R
-rule restrict {&T} _ {_} &f &pr &s → &f (↑ &T &pr &s)
+rule restrict {$T} _ {_} $f $pr $s ↪ $f (↑ $T $pr $s)
 
 theorem injective_restrict {T} S {R} (f: Term (T ~> R)) (pr: Term (S ⊑ T)):
-  Term ({|injective?|} f) ⇒ Term ({|injective?|} (restrict S f pr))
+  Term ({|injective?|} f) → Term ({|injective?|} (restrict S f pr))
 proof
 admit
 
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 0e2831e99ec32d380305003fbf1148d91934494e..f875f5b3f78163b8bad5bcd97211be5dc4fe4be3 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -22,7 +22,7 @@ set infix left 6 "≠" ≔ neq
 //
 // if_def
 //
-symbol if {T: Term uType}: Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
+symbol if {T: Term uType}: Term uProp → Term T → Term T → Term T
 // The reduction rules for if are in [equality_props]
 
 //
@@ -64,7 +64,7 @@ admit
 //
 set declared "∃"
 // Declared as a lemma in the prelude
-definition ∃ {eT: Term uType} (P: Term eT ⇒ Term bool) ≔
+definition ∃ {eT: Term uType} (P: Term eT → Term bool) ≔
 ¬ (forall (λx, ¬ (P x)))
 
 //
@@ -84,8 +84,8 @@ definition SETOF ≔ pred
 //
 // equality_props
 //
-rule if true &t  _ → &t
- and if false _ &f → &f
+rule if true $t  _ ↪ $t
+ and if false _ $f ↪ $f
 
 constant symbol If_true {T} (x y: Term T): Term ((if true x y) = x)
 constant symbol If_false {T} (x y: Term T): Term ((if false x y) = y)
@@ -107,15 +107,15 @@ symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
 // set builtin "refl" ≔ reflexivity_of_equal
 
 symbol transitivity_of_equal T (x y z: Term T):
-  Term ((x = y) ∧ (y = z)) ⇒ Term (eq x z)
+  Term ((x = y) ∧ (y = z)) → Term (eq x z)
 
-symbol symmetry_of_equal T (x y: Term T): Term (x = y) ⇒ Term (y = x)
+symbol symmetry_of_equal T (x y: Term T): Term (x = y) → Term (y = x)
 
 //
 // if_props
 //
 theorem lift_if1 (S T: Term uType) (a: Term bool) (x y: Term S)
-  (f: Term S ⇒ Term T):
+  (f: Term S → Term T):
   Term ((f (if a x y)) = (if a (f x) (f y)))
 proof
 print
diff --git a/prelude/logic2.lp b/prelude/logic2.lp
index d2803a31f4f30a46ba40d7c6b8011d0a9484df1b..6d300fbfbf1054fbd9633617059bce6bdef030b8 100644
--- a/prelude/logic2.lp
+++ b/prelude/logic2.lp
@@ -46,7 +46,7 @@ admit
 //
 set declared "∃"
 // Declared as a lemma in the prelude
-definition ∃ {T: Set} (P: η T ⇒ η bool) ≔ ¬ (forall (λx, ¬ (P x)))
+definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (forall (λx, ¬ (P x)))
 
 //
 // Defined types
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index c137f2fa708b5d5a4c11c3ca4337b68d72314c4e..963a0039eb0c389d7b50582cc5c451ce6d55978b 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -11,22 +11,22 @@ constant symbol number: Term uType
 //
 // Theory number_fields
 //
-symbol field_pred: Term number ⇒ Univ Prop
+symbol field_pred: Term number → Univ Prop
 definition number_field ≔ Psub field_pred
 // number_field is an uninterpreted subtype
 definition numfield ≔ number_field
 
-symbol {|+|}: Term numfield ⇒ Term numfield ⇒ Term numfield
+symbol {|+|}: Term numfield → Term numfield → Term numfield
 set infix left 6 "+" ≔ {|+|}
-symbol {|-|}: Term numfield ⇒ Term numfield ⇒ Term numfield
+symbol {|-|}: Term numfield → Term numfield → Term numfield
 set infix left 6 "-" ≔ {|-|}
 
 // Other way to extend type of functions,
-symbol ty_plus: Term uType ⇒ Term uType ⇒ Term uType
+symbol ty_plus: Term uType → Term uType → Term uType
 symbol polyplus {T: Term uType} {U: Term uType}
-: Term T ⇒ Term U ⇒ Term (ty_plus T U)
+: Term T → Term U → Term (ty_plus T U)
 // plus is defined on numfield
-rule ty_plus numfield numfield → numfield
+rule ty_plus numfield numfield ↪ numfield
 
 symbol commutativ_add (x y: Term numfield): Term ((x + y) = (y + x))
 symbol associative_add (x y z: Term numfield): Term (x + (y + z) = (x + y) + z)
@@ -51,16 +51,16 @@ theorem nonzero_real_not_empty: Term (∃ nonzero_real_pred)
 proof admit
 definition nzreal ≔ nonzero_real
 
-symbol closed_plus_real: ∀(x y: Term real),
+symbol closed_plus_real: Π(x y: Term real),
   let pr ≔ S.restr numfield real_pred in
   let xnf ≔ ↑ numfield pr x in
   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
+rule ty_plus real real ↪ real
 
 symbol lt (x y: Term real): Term bool
 set infix 6 "<" ≔ lt
@@ -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 _ _
@@ -111,7 +111,7 @@ symbol closed_plus_rat (x y: Term rat):
   let ynf ≔ ↑ numfield (S.restr numfield real_pred) yreal in
   let sum ≔ xnf + ynf in
   Term (rational_pred (↓ real_pred sum (closed_plus_real xreal yreal)))
-rule ty_plus rat rat → rat
+rule ty_plus rat rat ↪ rat
 
 definition nonneg_rat_pred (x: Term rational) ≔ (↑ real rat_is_real x) >= zero
 definition nonneg_rat ≔ Psub nonneg_rat_pred
@@ -127,7 +127,7 @@ qed
 definition posrat_pred (x: Term nonneg_rat) ≔ (↑ real nonneg_rat_is_real x) > zero
 definition posrat ≔ Psub posrat_pred
 
-symbol div: Term real ⇒ Term nonzero_real ⇒ Term real
+symbol div: Term real → Term nonzero_real → Term real
 set infix left 8 "/" ≔ div
 
 /// NOTE: any expression of the type below would generate a TCC to prove
diff --git a/sandbox/boolops.lp b/sandbox/boolops.lp
index e5cde104d7bfbbf778aafcaba66c2bc36e1c1627..622485ed9726e7e62c3bc06e7dbafedbc62daf9a 100644
--- a/sandbox/boolops.lp
+++ b/sandbox/boolops.lp
@@ -5,9 +5,6 @@ require open personoj.encodings.pvs_cert
 require open personoj.encodings.equality
 require open personoj.encodings.bool_hol
 
-symbol imp: ∀P: Bool, (ε P ⇒ η bool) ⇒ η bool
-set infix left 6 "⊃" ≔ imp
-
 require personoj.paper.rat as Q
 
 set builtin "0" ≔ Q.Z
diff --git a/sandbox/boolops_if.lp b/sandbox/boolops_if.lp
index 735934d90859da7e3f503e35bf6895a8a96c6d98..987a03069647938d9d4b512e21f604414435e499 100644
--- a/sandbox/boolops_if.lp
+++ b/sandbox/boolops_if.lp
@@ -1,6 +1,6 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_pvs
+require open personoj.encodings.boolops_if
 
 theorem trivial (P: η bool): ε (P ⊃ (λ_, P))
 proof
diff --git a/sandbox/even.lp b/sandbox/even.lp
index ff5c8073a5eb5156677e3bf2c1e6d2bdeeb06988..3fb9f909debbae7c17c5d24637ae015c1e88c292 100644
--- a/sandbox/even.lp
+++ b/sandbox/even.lp
@@ -3,10 +3,10 @@ prelude.cert_f.equalities
 prelude.cert_f.naturalnumbers
 adlib.cert_f.nat
 
-symbol mod2: Term nat ⇒ Term nat
-rule mod2 (&n + 2) → mod2 &n
- and mod2 ( _ + 1) → 1
- and mod2       0  → 0
+symbol mod2: Term nat → Term nat
+rule mod2 ($n + 2) ↪ mod2 $n
+ and mod2 ( _ + 1) ↪ 1
+ and mod2       0  ↪ 0
 
 definition is_even (n: Term nat) ≔ eq (mod2 n) 0
 
diff --git a/sandbox/ifs.lp b/sandbox/ifs.lp
index 9379a03097fd736ec6da1b777297395923e31146..92c5032caa07fd2f31c8f6268d4f8bd5e21faa3d 100644
--- a/sandbox/ifs.lp
+++ b/sandbox/ifs.lp
@@ -5,15 +5,15 @@ require personoj.encodings.deferred as Deferred
 require open personoj.encodings.subtype //FIXME: why must it be the last import?
 
 symbol if {U: Set} {V: Set} (S: Set)
-: ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ η U ⇒ η V ⇒ η S
+: ε (U ⊑ S) → ε (V ⊑ S) → Bool → η U → η V → η S
 
 symbol lif {U: Set} {V: Set} (S: Set)
-: Deferred.p (U ⊑ S) ⇒ Deferred.p (V ⊑ S) ⇒ Bool ⇒ Deferred.t U ⇒ Deferred.t V ⇒ η S
+: Deferred.p (U ⊑ S) → Deferred.p (V ⊑ S) → Bool → Deferred.t U → Deferred.t V → η S
 
 // lazy if
 set flag "print_implicits" on
-rule lif _ &pr _ true &t _ → ↑ (Deferred.unquote_p &pr) (Deferred.unquote &t)
-rule lif _ _ &pr false _ &f → ↑ (Deferred.unquote_p &pr) (Deferred.unquote &f)
+rule lif _ $pr _ true $t _ ↪ ↑ (Deferred.unquote_p $pr) (Deferred.unquote $t)
+rule lif _ _ $pr false _ $f ↪ ↑ (Deferred.unquote_p $pr) (Deferred.unquote $f)
 
 // The if is lazy, that is, the expression [if true 2 (1/0)] must type check and
 // return 2. For this, we use the [Deferred.t] datatype. But remember that [if]
@@ -22,27 +22,27 @@ rule lif _ _ &pr false _ &f → ↑ (Deferred.unquote_p &pr) (Deferred.unquote &
 // of this super-types. Since these arguments are deferred and can be ill-typed,
 // we want to defer the verification of sub-type as well. Therefore, we
 // introduce the [lifSet] type to type the [lif].
-// [lifset &T &F &S p] reduces to the type of the function that maps a proof of
-// &T is a sub-type of &S to &S if [p] is true and the function that maps a
-// proof of &F is a sub-type of &S if [p] is false.
+// [lifset $T $F $S p] reduces to the type of the function that maps a proof of
+// $T is a sub-type of $S to $S if [p] is true and the function that maps a
+// proof of $F is a sub-type of $S if [p] is false.
 // The result of [lif S true e1 e2] is the function that maps the proof of
 // sub-typing [Te1 ⊑ S] to the evaluation (or unquoting) of [e1].
-type λ (T S: Set), ε (T ⊑ S) ⇒ η S
-symbol lifSet (T U S: Set): Bool ⇒ TYPE
+type λ (T S: Set), ε (T ⊑ S) → η S
+symbol lifSet (T U S: Set): Bool → TYPE
 symbol tt: Bool
 symbol ff: Bool
-rule lifSet &U _ &S true → ε (&U ⊑ &S) ⇒ η &S
-rule lifSet _ &F &S false → ε (&F ⊑ &S) ⇒ η &S
+rule lifSet $U _ $S true ↪ ε ($U ⊑ $S) → η $S
+rule lifSet _ $F $S false ↪ ε ($F ⊑ $S) → η $S
 
 compute λ(U V S: Set), lifSet U V S tt
 
 symbol lifn {U: Set} {V: Set} (S: Set) (p: Bool)
-: Deferred.t U ⇒ Deferred.t V ⇒ lifSet U V S p
+: Deferred.t U → Deferred.t V → lifSet U V S p
 
-rule lifn {&U} {&V} &S true &t &f → λh:ε (&U ⊑ &S), ↑ {&U} {&S} h (Deferred.unquote &t)
+rule lifn {$U} {$V} $S true $t $f ↪ λh:ε ($U ⊑ $S), ↑ {$U} {$S} h (Deferred.unquote $t)
 
 symbol if3 {u: Set} {v: Set} (s: Set) (_: ε (u ⊑ s)) (_: ε (v ⊑ s)) (p: Bool):
-  (ε p ⇒ η u) ⇒ (ε (¬ p) ⇒ η v) ⇒ η s
+  (ε p → η u) → (ε (¬ p) → η v) → η s
 
-rule if3 &s &pr _ true &bh _ → ↑ &pr (&bh (λx, x))
- and if3 &s _ &pr false _ &bh → ↑ &pr (&bh (λx, x))
+rule if3 $s $pr _ true $bh _ ↪ ↑ $pr ($bh (λx, x))
+ and if3 $s _ $pr false _ $bh ↪ ↑ $pr ($bh (λx, x))
diff --git a/sandbox/nat.lp b/sandbox/nat.lp
index f714630b34eef606d5a5475886d81397cf37a1af..bbbf705a7596f396532002929f291e0510f4a390 100644
--- a/sandbox/nat.lp
+++ b/sandbox/nat.lp
@@ -4,25 +4,25 @@ require open
     personoj.prelude.logic
 
 constant symbol Nat: Term uType
-injective symbol succ: Term Nat ⇒ Term Nat
+injective symbol succ: Term Nat → Term Nat
 constant symbol zero: Term Nat
 set builtin "0" ≔ zero
 set builtin "+1" ≔ succ
 
-symbol times : Term Nat ⇒ Term Nat ⇒ Term Nat
-symbol plus : Term Nat ⇒ Term Nat ⇒ Term Nat
+symbol times : Term Nat → Term Nat → Term Nat
+symbol plus : Term Nat → Term Nat → Term Nat
 set infix left 6 "+" ≔ plus
 set infix left 7 "*" ≔ times
 
-rule (succ &n) +       &m  → succ (&n + &m)
- and        0  +       &m  → &m
- and       &n  + (succ &m) → succ (&n + &m)
- and       &n  +        0  → &n
+rule (succ $n) +       $m  ↪ succ ($n + $m)
+ and        0  +       $m  ↪ $m
+ and       $n  + (succ $m) ↪ succ ($n + $m)
+ and       $n  +        0  ↪ $n
 
-rule (succ &n) *       &m  → &n * &m + &m
- and        0  *        _  → 0
- and       &n  * (succ &m) → &n * &m + &n
- and        _  * 0         → 0
+rule (succ $n) *       $m  ↪ $n * $m + $m
+ and        0  *        _  ↪ 0
+ and       $n  * (succ $m) ↪ $n * $m + $n
+ and        _  * 0         ↪ 0
 
 symbol prod_comm (x y: Term Nat): Term ((x * y) = (y * x))
 
@@ -33,7 +33,7 @@ symbol prod_comm (x y: Term Nat): Term ((x * y) = (y * x))
 
 definition not_zero ≔ neq 0
 symbol prod_not_zero (x y: Term Nat):
-  Term (not_zero x) ⇒ Term (not_zero y) ⇒ Term (not_zero (times x y))
+  Term (not_zero x) → Term (not_zero y) → Term (not_zero (times x y))
 
 definition Nznat ≔ Psub not_zero
 
@@ -43,15 +43,15 @@ definition nznat (x: Term Nat) (h: Term (not_zero x)) : Term Nznat ≔
 
 symbol one_not_zero: Term (not_zero 1)
 
-symbol induction (P: Term Nat ⇒ Term bool):
-  ∀n, Term (P 0) ⇒ Term (P (n + 1)) ⇒ ∀m, Term (P m)
+symbol induction (P: Term Nat → Term bool):
+  Πn, Term (P 0) → Term (P (n + 1)) → Πm, Term (P m)
 
 // Divisions
 definition div (x y: Term Nat) ≔ ∃ (λk, x * k = y)
 definition even (x: Term Nat) ≔ div 2 x
 definition Even ≔ Psub even
 
-theorem even_stable_double: ∀x: Term Even, Term (even (2 * (fst x)))
+theorem even_stable_double: Πx: Term Even, Term (even (2 * (fst x)))
 proof
     assume x h
     refine (h (fst x) _)
@@ -59,13 +59,13 @@ proof
     refine reflexivity_of_equal _ ((fst x) + (fst x))
 qed
 
-symbol surjective_pairing T (p: Term T ⇒ Term bool):
-       ∀x: Term (Psub p), Term (pair p (fst x) (snd x) = x)
+symbol surjective_pairing T (p: Term T → Term bool):
+       Πx: Term (Psub p), Term (pair p (fst x) (snd x) = x)
 
 //symbol app_thm (D R: Term uType) (f: Term (D ~> R))
-//     : ∀x y: Term D, Term (x = y) ⇒ Term (f x = f y)
+//     : Πx y: Term D, Term (x = y) → Term (f x = f y)
 
-theorem fst_injective: ∀x y: Term Even, Term (fst x = fst y) ⇒ Term (x = y)
+theorem fst_injective: Πx y: Term Even, Term (fst x = fst y) → Term (x = y)
 proof
     assume x y h
     refine transitivity_of_equal Even x (pair even (fst x) (snd x)) y _
@@ -84,9 +84,9 @@ proof
 
 abort
 
-rule &x = &x → true
-theorem prf_irrelevance T (p: Term T ⇒ Term bool)
-: ∀(x: Term T) (pr: Term (p x)) (pr': Term (p x)), Term (pair p x pr = pair p x pr')
+rule $x = $x ↪ true
+theorem prf_irrelevance T (p: Term T → Term bool)
+: Π(x: Term T) (pr: Term (p x)) (pr': Term (p x)), Term (pair p x pr = pair p x pr')
 proof
     assume T p x pr0 pr1
     simpl
diff --git a/sandbox/quote.lp b/sandbox/quote.lp
index 4084a62e6b7a4a7e95577de05d1582d91e38d397..afcfb532c8abdd8dcf672494095f4beb8d6341b2 100644
--- a/sandbox/quote.lp
+++ b/sandbox/quote.lp
@@ -21,7 +21,7 @@ compute Deferred.unquote qu_ok
 
 compute Deferred.quote {T ~> T} (λx:η T, f x)
 
-symbol lor: Deferred.t bool ⇒ Deferred.t bool ⇒ Bool
+symbol lor: Deferred.t bool → Deferred.t bool → Bool
 
 compute let f' ≔ Deferred.quote f in
         let t' ≔ Deferred.quote t in
diff --git a/sandbox/rat.lp b/sandbox/rat.lp
index cab1f9924923ef74704a71a963ae4e2d36097c61..26a1f14e47b5e3a0da834c0a1625984db212c59d 100644
--- a/sandbox/rat.lp
+++ b/sandbox/rat.lp
@@ -11,26 +11,26 @@ set builtin "+1" ≔ N.succ
 constant symbol Rat : Term uType
 constant symbol zero : Term Rat
 
-symbol rat : Term N.Nat ⇒ Term N.Nznat ⇒ Term Rat
+symbol rat : Term N.Nat → Term N.Nznat → Term Rat
 set infix 8 "/" ≔ rat
 
-symbol times : Term Rat ⇒ Term Rat ⇒ Term Rat
+symbol times : Term Rat → Term Rat → Term Rat
 
-rule times (rat &a &b) (rat &c &d) →
-  let bv ≔ fst &b in
-  let dv ≔ fst &d in
+rule times (rat $a $b) (rat $c $d) ↪
+  let bv ≔ fst $b in
+  let dv ≔ fst $d in
   rat
-   (N.times &a &c)
+   (N.times $a $c)
    (N.nznat
     (N.times bv dv)
     (N.prod_not_zero bv dv
-     (snd &b)
-     (snd &d)))
+     (snd $b)
+     (snd $d)))
 
-symbol rateq : Term Rat ⇒ Term Rat ⇒ Term bool
-rule rateq (&a / &b) (&c / &d) →
+symbol rateq : Term Rat → Term Rat → Term bool
+rule rateq ($a / $b) ($c / $d) ↪
   let nzval x ≔ fst x in
-  (N.times &a (nzval &d)) = (N.times (nzval &b) &c)
+  (N.times $a (nzval $d)) = (N.times (nzval $b) $c)
 
 definition onz : Term N.Nznat ≔ N.nznat 1 N.one_not_zero
 
@@ -41,7 +41,7 @@ definition onz : Term N.Nznat ≔ N.nznat 1 N.one_not_zero
 // engine would instantiate _ accordingly, but it is not likely since it is
 // based on non linearity, and hints are linear.
 // We rather reduce the proof to the trivial proof
-rule &x = &x → true
+rule $x = $x ↪ true
 theorem right_cancellation (a: Term N.Nat) (b: Term N.Nznat):
     Term (rateq (times (a / b) ((fst b) / onz)) (a / onz))
 proof