diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
index 586c9e13b37da5716f96fa2a7d45b28905d231f2..338788c0d99d697a481a8fb69796b78b70d415f7 100644
--- a/encodings/bool_hol.lp
+++ b/encodings/bool_hol.lp
@@ -2,7 +2,7 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
-definition false ≔ forall {bool} (λx, x)
+definition false ≔ ∀ {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
 
 definition not P ≔ impd {P} (λ_, false)
diff --git a/encodings/bool_pvs.lp b/encodings/bool_pvs.lp
index b94bc4434a23a79108d4f56df9e02f9b23d69ae8..31e9fae61aa24f8748eb90861f6e62bc9340a22b 100644
--- a/encodings/bool_pvs.lp
+++ b/encodings/bool_pvs.lp
@@ -3,7 +3,7 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
-definition false ≔ forall {bool} (λx, x)
+definition false ≔ ∀ {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
 
 symbol eq {s: Set}: η s → η s → η bool
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 51cf4439a98fd3ddad142427b90b62523e12e5f9..7dabafd973d5133e6018d5ec333c8f62828d8ab6 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -6,6 +6,7 @@ symbol Bool: TYPE
 set declared "Ï•"
 set declared "η"
 set declared "ε"
+set declared "∀"
 injective symbol ϕ: Kind → TYPE
 injective symbol η: Set → TYPE
 injective symbol ε: Bool → TYPE
@@ -16,11 +17,11 @@ symbol bool: Set
 rule ϕ {|set|} ↪ Set
 rule η bool ↪ Bool
 
-symbol forall {x: Set}: (η x → Bool) → Bool
+symbol ∀ {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)
+rule ε (∀ {$X} $P) ↪ Πx: η $X, ε ($P x)
 with ε (impd {$H} $P) ↪ Πh: ε $H, ε ($P h)
 with η (arrd {$X} $T) ↪ Πx: η $X, η ($T x)
 
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 05fba28db1dc785e2e37b749d4024413ef4f4df4..ccf8593834208c68bd9eeb6165cd3cc50a0e87f9 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -16,7 +16,7 @@ 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))
+     : ε (∀ (λx, (r1 x) ⊑ (r2 x))) → ε ((arrd r1) ⊑ (arrd r2))
 
 // Maximal supertype
 symbol μ: Set → Set
@@ -47,7 +47,7 @@ symbol downcast {A: Set} {B: Set} (_: ε (B ⊑ A))
 definition ↓ {A} {B} ≔ downcast {A} {B}
 
 set flag "print_implicits" on
-rule π {$T ~> $U} ↪ λx: η $T → η (μ $U), forall (λy, π {$U} (x y))
+rule π {$T ~> $U} ↪ λx: η $T → η (μ $U), ∀(λ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))
diff --git a/encodings/subtype2.lp b/encodings/subtype2.lp
index 246d456c6d939318c614ddddbeca7dd32211e919..4204d2a8e3660913f291f785f64a44ba7ca0d9aa 100644
--- a/encodings/subtype2.lp
+++ b/encodings/subtype2.lp
@@ -25,9 +25,9 @@ definition ↓ {t} ≔ downcast {t}
 
 // rule η (maxcast (maxcast $t)) ↪ η (maxcast $t)
 
-rule ε (π {$t ~> $u}) ↪ ε (λx: η $t → η (μ $u), forall (λy, π (x y)))
+rule ε (π {$t ~> $u}) ↪ ε (λx: η $t → η (μ $u), ∀ (λy, π (x y)))
 with ε (π {psub {$t} $a}) ↪ ε (λx: η (μ $t), (π x) ∧ (λy: ε (π x), $a (↓ x y)))
-with ε (π {arrd $b}) ↪ ε (λx: η (arrd (λx, μ ($b x))), forall (λy, π (x y)))
+with ε (π {arrd $b}) ↪ ε (λx: η (arrd (λx, μ ($b x))), ∀ (λy, π (x y)))
 
 rule ε (π (maxcast _)) ↪ ε true // FIXME: to  be justified
 
@@ -74,7 +74,7 @@ with ε ((arrd {$t1} $u1) ≃ (arrd {$t2} $u2))
    ↪ ε ((μ $t1 ≃ μ $t2)
         ∧ (λh,
            (eq {μ $t1 ~> bool} π (λx, π (eqcast h x)))
-           ∧ (λh', forall
+           ∧ (λh', ∀
                (λx: η $t1,
                 ($u1 x) ≃ ($u2 (cast {$t1} {$t2} h x
                                      (comp_same_cstr_cast $t1 $t2 h h' x)))))))
diff --git a/paper/rat.lp b/paper/rat.lp
index cd34b423a0e26bc1813cab6b38cf3b82f24d477d..6e46ddf9380e87534f73264ae5f63cb42cdaf9d6 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -39,7 +39,7 @@ set infix left 3 "=ℕ" ≔ eqnat
 
 symbol s_not_z: Πx: η ℕ, ε (¬ (Z =ℕ (S x)))
 
-theorem times_comm: ε (forall (λa, forall (λb, (a * b) =ℕ (b * a))))
+theorem times_comm: ε (∀ (λa, ∀ (λb, (a * b) =ℕ (b * a))))
 proof
 admit
 
@@ -61,15 +61,14 @@ 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)
+definition false ≔ ∀ {bool} (λx, x)
 
 theorem nzprod:
-  ε (forall
-       {â„•*}
-       (λx, forall {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
+  ε (∀ {ℕ*}
+       (λx, ∀ {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
 proof
   refine nznat_induction
-           (λx, forall (λy: η ℕ*, (Z =ℕ (fst x * fst y)) ⊃ false)) ?xOnz ?xSnz
+           (λx, ∀ (λy: η ℕ*, (Z =ℕ (fst x * fst y)) ⊃ false)) ?xOnz ?xSnz
   // x = 1
   refine nznat_induction
            (λy, (Z =ℕ (fst Onz * fst y)) ⊃ false) ?yOnz ?ySnz
@@ -94,9 +93,7 @@ rule times_rat ($a / $b) ($c / $d) ↪
   ($a * $c) / (pair denom prf)
 
 theorem right_cancel:
-  ε (forall
-       (λa, forall
-              (λb, eqrat (times_rat (a / b) (fst b / Onz)) (a / Onz))))
+  ε (∀ (λa, ∀ (λb, eqrat (times_rat (a / b) (fst b / Onz)) (a / Onz))))
 proof
   assume x y
   simpl
diff --git a/prelude/logic.lp b/prelude/logic.lp
index ae3b846c235e14f76f1a25abc571e1c329ae4816..0daaf1acfa5eddbf5a4872b0bf79d4ce778dc7ef 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -29,9 +29,9 @@ set infix left 2 "≠" ≔ neq
 constant symbol bool_exclusive: ε (neq bool false true)
 constant
 symbol bool_inclusive
-     : ε (forall {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
+     : ε (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
 
-theorem excluded_middle: ε (forall {bool} (λa, a ∨ (λ_, ¬ a)))
+theorem excluded_middle: ε (∀ {bool} (λa, a ∨ (λ_, ¬ a)))
 proof
   assume x f
   refine f
@@ -43,10 +43,10 @@ qed
 definition xor (a b: η bool) ≔ neq bool a b
 
 set flag "print_implicits" on
-theorem xor_def: ε (forall
+theorem xor_def: ε (∀
                       {bool}
                       (λa,
-                         forall
+                         ∀
                            {bool}
                            (λb, eq {bool} (xor a b)
                                    (if {bool} a (λ_, ¬ b) (λ_, b)))))
@@ -58,7 +58,7 @@ admit
 // Quantifier props[t: TYPE]
 //
 set declared "∃"
-definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (forall (λx, ¬ (P x)))
+definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
 
 //
 // Defined types
@@ -84,37 +84,37 @@ definition SETOF ≔ pred
 constant
 symbol If_true
      : ε (∀B
-           (λt, forall
-                  (λx, forall {t} (λy, if true (λ_, x) (λ_, y) = x))))
+           (λt, ∀
+                  (λx, ∀ {t} (λy, if true (λ_, x) (λ_, y) = x))))
 constant
 symbol If_false
      : ε (∀B
-           (λt, forall
-                  (λx, forall {t} (λy, if false (λ_, x) (λ_, y) = y))))
+           (λt, ∀
+                  (λx, ∀ {t} (λy, if false (λ_, x) (λ_, y) = y))))
 
 theorem if_same
       : ε (∀B (λt,
-                 forall {bool} (λb, forall (λx: η t,
+                 ∀ {bool} (λb, ∀ (λx: η t,
                                               if b (λ_, x) (λ_, x) = x))))
 proof
 admit
 
-constant symbol reflexivity_of_equals: ε (∀B (λt, forall (λx: η t, x = x)))
+constant symbol reflexivity_of_equals: ε (∀B (λt, ∀ (λx: η t, x = x)))
 set builtin "refl" ≔ reflexivity_of_equals
 
 constant
 symbol transitivity_of_equals
      : ε (∀B (λt,
-                forall
+                ∀
                   (λx: η t,
-                     forall
+                     ∀
                        (λy: η t,
-                          forall
+                          ∀
                             (λz: η t, (x = y) ∧ (λ_, y = z) ⊃ (λ_, x = z))))))
 
 constant
 symbol symmetry_of_equals
-     : ε (∀B (λt, forall (λx: η t, (forall (λy: η t, (x = y) ⊃ (λ_, y = x))))))
+     : ε (∀B (λt, ∀ (λx: η t, (∀ (λy: η t, (x = y) ⊃ (λ_, y = x))))))
 
 // Not in prelude!
 theorem eqind {t} x y: ε (x = y) → Πp: η t → Bool, ε (p y) → ε (p x)
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index e4854b3a09325ae32fe8bffd6063dc46c467ee4f..c6e066031859c579db240f24946bb50dad7aa692 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -30,10 +30,10 @@ set infix 6 "-" ≔ {|-|}
 // rule ty_plus numfield numfield ↪ numfield
 
 constant
-symbol commutative_add : ε (forall (λx, forall (λy, x + y = y + x)))
+symbol commutative_add : ε (∀ (λx, ∀ (λy, x + y = y + x)))
 constant
 symbol associative_add
-     : ε (forall (λx, forall (λy, forall (λz, x + (y + z) = (x + y) + z))))
+     : ε (∀ (λx, ∀ (λy, ∀ (λz, x + (y + z) = (x + y) + z))))
 // FIXME add a cast on zero?
 // symbol identity_add (x: Term numfield): Term (x + zero = x)