diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
index 97c88564ad27504d87962bb35c3bdd40d290d29a..d89d97ffcbe04449eafb1ff83be3f29cf6e59db0 100644
--- a/encodings/bool_hol.lp
+++ b/encodings/bool_hol.lp
@@ -23,13 +23,13 @@ set builtin "imp" ≔ imp
 set builtin "and" ≔ and
 set builtin "or"  ≔ or
 
-symbol if {s: Set} p: (ε p → η s) → (ε (¬ p) → η s) → η s
+symbol if {s: Set} p: (Prf p → El s) → (Prf (¬ p) → El s) → El s
 rule if {bool} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
 
-symbol eq {s: Set}: η s → η s → η bool
+symbol eq {s: Set}: El s → El s → El bool
 set infix 2 "=" ≔ eq
 set builtin "eq" ≔ eq // FIXME emacs indentation
 
-rule ε ($x = $y) ↪ Πp: η (_ ~> bool), ε (p $x) → ε (p $y)
+rule Prf ($x = $y) ↪ Πp: El (_ ~> bool), Prf (p $x) → Prf (p $y)
 
 definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
diff --git a/encodings/bool_pvs.lp b/encodings/bool_pvs.lp
index 31e9fae61aa24f8748eb90861f6e62bc9340a22b..552784c641a976a569f3cb33144345ca85e44f43 100644
--- a/encodings/bool_pvs.lp
+++ b/encodings/bool_pvs.lp
@@ -6,15 +6,15 @@ require open personoj.encodings.pvs_cert
 definition false ≔ ∀ {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
 
-symbol eq {s: Set}: η s → η s → η bool
+symbol eq {s: Set}: El s → El s → El 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: (Prf p → El s) → (Prf (¬ p) → El s) → El s
+rule Prf (if $p $then $else)
+   ↪ (Πh: Prf $p, Prf ($then h)) → Πh: Prf (¬ $p), Prf ($else h)
 
 definition and p q ≔ if {bool} p q (λ_, false)
 definition or p q ≔ if {bool} p (λ_, true) q
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index c7b18680c657bbdb9d9028e8f8bd0c9586f1629b..115d7713fbb320a9092020b744c600c4b869ee24 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -4,28 +4,28 @@ require open personoj.encodings.bool_hol
 
 constant symbol {|!Number!|}: θ {|set|}
 
-constant symbol zero: η {|!Number!|}
-constant symbol succ: η ({|!Number!|} ~> {|!Number!|})
+constant symbol zero: El {|!Number!|}
+constant symbol succ: El ({|!Number!|} ~> {|!Number!|})
 
 set builtin "0" ≔ zero
 set builtin "+1" ≔ succ
 
 // In PVS, the axipms 1 ≠ 2, 1≠3, ... are built in
 // Here we use the decidable equality
-rule ε (succ $n = succ $m) ↪ ε ($n = $m)
-with ε (zero = succ _) ↪ ε false
-with ε (zero = zero) ↪ ε true
+rule Prf (succ $n = succ $m) ↪ Prf ($n = $m)
+with Prf (zero = succ _) ↪ Prf false
+with Prf (zero = zero) ↪ Prf true
 
 // Define strings as list of numbers
 constant symbol {|!String!|}: θ {|set|}
-constant symbol str_empty: η {|!String!|}
-constant symbol str_cons: η {|!Number!|} → η {|!String!|} → η {|!String!|}
+constant symbol str_empty: El {|!String!|}
+constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|}
 
 set declared "∃"
-definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
+definition ∃ {T: Set} (P: El T → El bool) ≔ ¬ (∀ (λx, ¬ (P x)))
 
 symbol propositional_extensionality:
-  ε (∀ {bool} (λp, (∀ {bool} (λq, (iff p q) ⊃ (λ_, eq {bool} p q)))))
+  Prf (∀ {bool} (λp, (∀ {bool} (λq, (iff p q) ⊃ (λ_, eq {bool} p q)))))
 
 definition neq {t} x y ≔ ¬ (eq {t} x y)
 set infix left 2 "/=" ≔ neq
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index 950f7ba02de67f01b472413ed34a00c5f4735d16..9b1fc41bf21624e2b6a3291a2a13ecc8c0017b63 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -10,4 +10,4 @@ require open personoj.encodings.pvs_cert
 
 constant symbol darr: Set → Kind → Kind
 set infix right 6 "*>" ≔ darr
-rule θ ($t *> $k) ↪ η $t → θ $k
+rule θ ($t *> $k) ↪ El $t → θ $k
diff --git a/encodings/equality.lp b/encodings/equality.lp
index 2714fb14fef6cc594db791db7d8c823a75329013..c3a1e702be18f0ed66d8a53e7118c54f0fc6491c 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}: El T → El T → Bool
 set infix left 6 "=" ≔ eq
 set builtin "eq" ≔ eq
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 7418cef5bd1dad41b1a1bb74acffbbb0e68e7730..8e94c6fcb3819199d0f216171f48ad5017a96a88 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -4,30 +4,28 @@ symbol Set: TYPE
 symbol Bool: TYPE
 
 set declared "θ"
-set declared "η"
-set declared "ε"
 set declared "∀"
 injective symbol θ: Kind → TYPE
-injective symbol η: Set → TYPE
-injective symbol ε: Bool → TYPE
+injective symbol El: Set → TYPE
+injective symbol Prf: Bool → TYPE
 
 constant symbol {|set|}: Kind
 constant symbol bool: Set
 
 rule θ {|set|} ↪ Set
-rule η bool ↪ Bool
+rule El bool ↪ Bool
 
-constant symbol ∀ {x: Set}: (η x → Bool) → Bool
-constant symbol impd {x: Bool}: (ε x → Bool) → Bool
-constant symbol arrd {x: Set}: (η x → Set) → Set
+constant symbol ∀ {x: Set}: (El x → Bool) → Bool
+constant symbol impd {x: Bool}: (Prf x → Bool) → Bool
+constant symbol arrd {x: Set}: (El x → Set) → Set
 
-rule ε (∀ {$X} $P) ↪ Πx: η $X, ε ($P x)
-with ε (impd {$H} $P) ↪ Πh: ε $H, ε ($P h)
-with η (arrd {$X} $T) ↪ Πx: η $X, η ($T x)
+rule Prf (∀ {$X} $P) ↪ Πx: El $X, Prf ($P x)
+with Prf (impd {$H} $P) ↪ Πh: Prf $H, Prf ($P h)
+with El (arrd {$X} $T) ↪ Πx: El $X, El ($T x)
 
 constant symbol arr: Set → Set → Set
-rule η (arr $X $Y) ↪ (η $X) → (η $Y)
+rule El (arr $X $Y) ↪ (El $X) → (El $Y)
 set infix right 6 "~>" ≔ arr
 
-set builtin "T" ≔ η
-set builtin "P" ≔ ε
+set builtin "T" ≔ El
+set builtin "P" ≔ Prf
diff --git a/encodings/pairs.lp b/encodings/pairs.lp
index 5957ab8122154217b0714678ff052c5021fb7b17..eb53f18b0892eecbe29fbc84445b4315dab204fd 100644
--- a/encodings/pairs.lp
+++ b/encodings/pairs.lp
@@ -11,17 +11,17 @@ set declared "σfst"
 set declared "σsnd"
 
 constant symbol σ: Set → Set → Set
-symbol σcons {t} {u}: η t → η u → η (σ t u)
-symbol σfst {t} {u}: η (σ t u) → η t
+symbol σcons {t} {u}: El t → El u → El (σ t u)
+symbol σfst {t} {u}: El (σ t u) → El t
 rule σfst (σcons $x _) ↪ $x
-symbol σsnd {t} {u}: η (σ t u) → η u
+symbol σsnd {t} {u}: El (σ t u) → El u
 rule σsnd (σcons _ $y) ↪ $y
 
-constant symbol Σ (t: Set): (η t → Set) → Set
-symbol pair_ss {t: Set} {u: η t → Set} (m: η t): η (u m) → η (Σ t u)
+constant symbol Σ (t: Set): (El t → Set) → Set
+symbol pair_ss {t: Set} {u: El t → Set} (m: El t): El (u m) → El (Σ t u)
 
-symbol fst_ss {t: Set} {u: η t → Set}: η (Σ t u) → η t
-symbol snd_ss {t: Set} {u: η t → Set} (m: η (Σ t u)): η (u (fst_ss m))
+symbol fst_ss {t: Set} {u: El t → Set}: El (Σ t u) → El t
+symbol snd_ss {t: Set} {u: El t → Set} (m: El (Σ t u)): El (u (fst_ss m))
 
 rule fst_ss (pair_ss $m _) ↪ $m
 rule snd_ss (pair_ss _ $n) ↪ $n
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index 4bd990b0bf41fe3d9b685e04ed3ef7c5b5a1fbae..b33c08c81e22507e121d002e0beee202aabceb48 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -28,10 +28,10 @@ rule ϕ (∀K $e) ↪ Πt: Set, ϕ ($e t)
 constant symbol SchemeS: TYPE
 symbol χ: SchemeS → TYPE
 constant symbol scheme_s: Set → SchemeS
-rule χ (scheme_s $X) ↪ η $X
+rule χ (scheme_s $X) ↪ El $X
 
 constant symbol ∀S: (Set → SchemeS) → SchemeS
 rule χ (∀S $e) ↪ Πt: Set, χ ($e t)
 
 constant symbol ∀B: (Set → Bool) → Bool
-rule ε (∀B $p) ↪ Πx: Set, ε ($p x)
+rule Prf (∀B $p) ↪ Πx: Set, Prf ($p x)
diff --git a/encodings/pvs_cert.lp b/encodings/pvs_cert.lp
index de273a910949968ee5759f966e250e52ee3443c4..02b798e0354731bf8b6faa91bdf6b4b7cc35cdf4 100644
--- a/encodings/pvs_cert.lp
+++ b/encodings/pvs_cert.lp
@@ -1,14 +1,14 @@
 // 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}: (El x → Bool) → Set
+symbol pair: Π{t: Set} {p: El t → Bool} (m: El t), Prf (p m) → El (psub p)
+symbol fst: Π{t: Set} {p: El t → Bool}, El (psub p) → El t
 
-symbol snd {t: Set}{p: η t → Bool} (m: η (psub p)): ε (p (fst m))
+symbol snd {t: Set}{p: El t → Bool} (m: El (psub p)): Prf (p (fst m))
 
 // Proof irrelevance
-protected symbol ppair: Π{t: Set} {p: η t → Bool}, η t → η (psub p)
+protected symbol ppair: Π{t: Set} {p: El t → Bool}, El t → El (psub p)
 
 // Reduction
 rule pair $X _ ↪ ppair $X
diff --git a/encodings/pvs_cert_minus.lp b/encodings/pvs_cert_minus.lp
index 5dcf534ff2ecf224419c25f87a3ef61288560a92..d63c35f0db75fc7542e3ed38bed3048ee267b631 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))
-              : η (Σ T U)
+constant symbol Σ (T : Set): (El T → Set) → Set
+constant symbol pair {T: Set} {U: El T → Set} (M: El T) (_: El (U M))
+              : El (Σ T U)
 
-symbol fst {T: Set} {U: η T → Set}: η (Σ T U) → η T
+symbol fst {T: Set} {U: El T → Set}: El (Σ T U) → El T
 rule fst (pair $M _) ↪ $M
 
-symbol snd {T: Set} {U: η T → Set} (M: η (Σ T U)): η (U (fst M))
+symbol snd {T: Set} {U: El T → Set} (M: El (Σ T U)): El (U (fst M))
 rule snd (pair _ $N) ↪ $N
diff --git a/encodings/pvs_core.lp b/encodings/pvs_core.lp
index 219ef31241d5873feba35dfa4553d8043d31ebe4..eee89932a36a56209f7eda6e74ef02148a1aefee 100644
--- a/encodings/pvs_core.lp
+++ b/encodings/pvs_core.lp
@@ -1,43 +1,39 @@
 constant symbol Type : TYPE
 constant symbol Prop : Type
 
-injective symbol eta : Type → TYPE
-injective symbol eps : eta Prop → TYPE
-set declared "η"
-set declared "ε"
-definition ε ≔ eps
-definition η ≔ eta
+injective symbol El : Type → TYPE
+injective symbol Prf : El Prop → TYPE
 
 symbol arr : Type → Type → Type
 set infix right 6 "~>" ≔ arr
 
-rule eta ($A ~> $B) ↪ eta $A → eta $B
+rule El ($A ~> $B) ↪ El $A → El $B
 
-// symbol psub : Π A : Type, eta (A ~> Prop) → Type
-symbol psub : Π A : Type, (eta A → eta Prop) → Type
+// symbol psub : Π A : Type, El (A ~> Prop) → Type
+symbol psub : Π A : Type, (El A → El Prop) → Type
 
 constant symbol cast : Type → Type
-rule eta (cast (psub $A _)) ↪ eta $A
+rule El (cast (psub $A _)) ↪ El $A
 
-symbol psubElim1 (A : Type) (P : eta (A ~> Prop)):
-  eta (psub A P) → eta A
+symbol psubElim1 (A : Type) (P : El (A ~> Prop)):
+  El (psub A P) → El A
 
-symbol imp : eta (Prop ~> Prop ~> Prop)
+symbol imp : El (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 : El Prop), (Prf p → Prf q) → Prf (p I> q)
+symbol impElim : Π p q : El Prop, Prf (p I> q) → Prf p → Prf 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): El (A ~> Prop) → El Prop
+rule El (all $A $P) ↪ Π x : El $A, El ($P x)
 
 // Forall intro
-symbol allIntro (A: Type) (p: eta (A ~> Prop)) (x: eta A):
-  eps (p x) → eps (all A p)
+symbol allIntro (A: Type) (p: El (A ~> Prop)) (x: El A):
+  Prf (p x) → Prf (all A p)
 // Forall elim
-symbol allElim (A: Type) (t: eta A) (p: eta (A ~> Prop)):
-  eps (all A p) → eps (p t)
+symbol allElim (A: Type) (t: El A) (p: El (A ~> Prop)):
+  Prf (all A p) → Prf (p t)
 
 // Subtype elim 2
-symbol psubElim (A: Type) (p: η (A ~> Prop)) (t: η (cast (psub A p))):
-  ε (p t)
+symbol psubElim (A: Type) (p: El (A ~> Prop)) (t: El (cast (psub A p))):
+  Prf (p t)
diff --git a/encodings/subtype_poly.lp b/encodings/subtype_poly.lp
index 27742bce174f1cc7f10d07beb0c7128fc51e7906..4f7683dfca8917f53f28561792fb84bc3bbb2aea 100644
--- a/encodings/subtype_poly.lp
+++ b/encodings/subtype_poly.lp
@@ -20,16 +20,16 @@ with μ (σ $T $U) ↪ σ (μ $T) (μ $U)
 with μ (arrd $b) ↪ arrd (λx, μ ($b x))
 with μ (μ $T) ↪ μ $T // FIXME: can be proved
 
-symbol π (T: Set): η (μ T) → Bool
-rule π ($t ~> $u) ↪ λx: η $t → η (μ $u), ∀ (λy, π $u (x y))
+symbol π (T: Set): El (μ T) → Bool
+rule π ($t ~> $u) ↪ λx: El $t → El (μ $u), ∀ (λy, π $u (x y))
 with π (σ $t $u)
-   ↪ λx: η (σ (μ $t) (μ $u)), π $t (σfst x) ∧ (λ_, π $u (σsnd x))
+   ↪ λx: El (σ (μ $t) (μ $u)), π $t (σfst x) ∧ (λ_, π $u (σsnd x))
 with π (arrd $b)
-   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π ($b y) (x y))
+   ↪ λx: El (arrd (λx, μ ($b x))), ∀ (λy, π ($b y) (x y))
 
 
 /// Casting a symbol from its type to its top-type
-symbol topcast {t: Set}: η t → η (μ t)
+symbol topcast {t: Set}: El t → El (μ t)
 definition ⇑ {t} ≔ topcast {t}
 
 symbol top_comp: Set → Set → Bool
@@ -40,40 +40,40 @@ set infix 6 "~" ≔ compatible
 
 /// Casting between top-types ‘t’ and ‘u’ provided a proof that they are
 /// equivalent.
-symbol eqcast {t: Set} (u: Set): ε (t ~ u) → η (μ t) → η (μ u)
-symbol eqcast_ {t: Set} (u: Set): η (μ t) → η (μ u) // Proof irrelevant
+symbol eqcast {t: Set} (u: Set): Prf (t ~ u) → El (μ t) → El (μ u)
+symbol eqcast_ {t: Set} (u: Set): El (μ t) → El (μ u) // Proof irrelevant
 rule eqcast {$t} $u _ $m ↪ eqcast_ {$t} $u $m
 rule eqcast_ {$t} $t $x ↪ $x
 
 // Casting from/to maximal supertype
-symbol downcast (t: Set) (x: η (μ t)): ε (π t x) → η t
+symbol downcast (t: Set) (x: El (μ t)): Prf (π t x) → El t
 definition ↓ t ≔ downcast t
-symbol downcast_ (t: Set): η (μ t) → η t
+symbol downcast_ (t: Set): El (μ t) → El t
 rule downcast $t $x _ ↪ downcast_ $t $x
 
 rule downcast_ $t (eqcast_ _ (topcast {$t} $x)) ↪ $x
 
 rule π (psub {$t} $a)
-   ↪ λx: η (μ $t), (π $t x) ∧ (λy: ε (π $t x), $a (↓ $t x y))
+   ↪ λx: El (μ $t), (π $t x) ∧ (λy: Prf (π $t x), $a (↓ $t x y))
 
 /// A term ‘x’ that has been cast up still validates the properties to be of its
 /// former type.
-symbol cstr_topcast_idem: ε (∀B (λt, ∀ {t} (λx, π t (⇑ x))))
+symbol cstr_topcast_idem: Prf (∀B (λt, ∀ {t} (λx, π t (⇑ x))))
 // or as a rewrite-rule:
-// rule ε (π _ (topcast _)) ↪ ε true
+// rule Prf (π _ (topcast _)) ↪ Prf true
 
 // The one true cast
-definition cast {fr_t} to_t comp (m: η fr_t) cstr ≔
+definition cast {fr_t} to_t comp (m: El fr_t) cstr ≔
   ↓ to_t (eqcast {fr_t} to_t comp (⇑ m)) cstr
 
 theorem comp_same_cstr_cast
         (fr to: Set)
-        (comp: ε (μ fr ≃ μ to))
-        (_: ε (eq {μ fr ~> bool}
+        (comp: Prf (μ fr ≃ μ to))
+        (_: Prf (eq {μ fr ~> bool}
                   (Ï€ fr)
                   (λx, π to (@eqcast fr to comp x))))
-        (x: η fr)
-      : ε (π to (@eqcast fr to comp (⇑ x)))
+        (x: El fr)
+      : Prf (π to (@eqcast fr to comp (⇑ x)))
 proof
   assume fr to comp eq_cstr x
   refine eq_cstr (λf, f (topcast x)) _
@@ -85,7 +85,7 @@ rule ($t1 ~> $u1) ≃ ($t2 ~> $u2)
    ↪ (μ $t1 ≃ μ $t2)
      ∧ (λh,
         (eq {μ $t1 ~> bool} (π $t1)
-            (λx: η (μ $t1), π $t2 (@eqcast $t1 $t2 h x)))
+            (λx: El (μ $t1), π $t2 (@eqcast $t1 $t2 h x)))
         ∧ (λ_, $u1 ≃ $u2))
 rule σ $t1 $u1 ≃ σ $t2 $u2
    ↪ $t1 ≃ $t2 ∧ (λ_, $u1 ≃ $u2)
@@ -94,7 +94,7 @@ with (arrd {$t1} $u1) ≃ (arrd {$t2} $u2)
      ∧ (λh,
         (eq {μ $t1 ~> bool} (π $t1) (λx, π $t2 (@eqcast $t1 $t2 h x)))
         ∧ (λh', ∀
-            (λx: η $t1,
+            (λx: El $t1,
              ($u1 x) ≃ ($u2 (cast {$t1} $t2 h x
                                             (comp_same_cstr_cast
                                              $t1 $t2 h h' x))))))
diff --git a/encodings/tuple.lp b/encodings/tuple.lp
index 2906db46a71b6e2b7bfdc715c7bb52b98be08006..e24bd8d8c2df16e33a76ae7e3a135a6ff043cd93 100644
--- a/encodings/tuple.lp
+++ b/encodings/tuple.lp
@@ -4,15 +4,15 @@ require open personoj.encodings.pvs_cert
 
 // Non dependent tuples
 constant symbol tuple_t: Set → Set → Set
-constant symbol tuple {t} {u}: η t → η u → η (tuple_t t u)
-symbol p1 {t} {u}: η (tuple_t t u) → η t
-symbol p2 {t} {u}: η (tuple_t t u) → η u
+constant symbol tuple {t} {u}: El t → El u → El (tuple_t t u)
+symbol p1 {t} {u}: El (tuple_t t u) → El t
+symbol p2 {t} {u}: El (tuple_t t u) → El u
 rule p1 (tuple $m _) ↪ $m
 rule p2 (tuple _ $n) ↪ $n
 
 constant symbol set_t: Set
-constant symbol set_nil: η set_t
-constant symbol set_cons: Set → η set_t → η set_t
+constant symbol set_nil: El set_t
+constant symbol set_cons: Set → El set_t → El set_t
 // TODO rewrite rules that transform (t, u, v) ~> w in t ~> u ~> v ~> w
 
 constant symbol TypeList: TYPE
@@ -25,10 +25,10 @@ rule type_car (type_cons $hd _) ↪ $hd
 
 constant symbol Tuple: TypeList → TYPE
 constant symbol tuple_nil: Tuple type_nil
-constant symbol tuple_cons (t: Set) (_: η t) (tl: TypeList) (_: Tuple tl):
+constant symbol tuple_cons (t: Set) (_: El t) (tl: TypeList) (_: Tuple tl):
   Tuple (type_cons t tl)
 
-symbol tuple_car (tl: TypeList): Tuple tl → η (type_car tl)
+symbol tuple_car (tl: TypeList): Tuple tl → El (type_car tl)
 rule tuple_car (type_cons $t _) (tuple_cons $t $x _) ↪ $x
 symbol tuple_cdr (tl: TypeList): Tuple tl → Tuple (type_cdr tl)
 rule tuple_cdr _ (tuple_cons _ _ _ $tup) ↪ $tup
diff --git a/encodings/unif_rules.lp b/encodings/unif_rules.lp
index c4998bac5f81e017c4341bc9456340c340ea85d3..da819d58e0c9b7834d98ad4d22c352837e66f9ae 100644
--- a/encodings/unif_rules.lp
+++ b/encodings/unif_rules.lp
@@ -1,3 +1,3 @@
 require open personoj.encodings.lhol
 
-set unif_rule η $t ≡ Bool ↪ $t ≡ bool
+set unif_rule El $t ≡ Bool ↪ $t ≡ bool
diff --git a/paper/rat.lp b/paper/rat.lp
index 22a5f4d4eee22ba55b835183860412cfe8cb92af..fa213f7f9d5a5c5d12ffca2809af1e93dfa9882b 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -8,30 +8,30 @@ definition false ≔ ∀ {bool} (λx, x)
 definition true ≔ false ⇒ false
 symbol not: Bool → Bool
 set prefix 8 "¬" ≔ not
-rule ε (¬ $x) ↪ ε $x → Π(z: Bool), ε z
+rule Prf (¬ $x) ↪ Prf $x → Π(z: Bool), Prf z
 
 // Nat top type
 constant symbol nat: Set
 // Presburger arithmetics
-constant symbol s: η (nat ~> nat)
-constant symbol z: η nat
-constant symbol eqnat: η (nat ~> nat ~> bool)
-symbol plus_nat: η (nat ~> nat ~> nat)
+constant symbol s: El (nat ~> nat)
+constant symbol z: El nat
+constant symbol eqnat: El (nat ~> nat ~> bool)
+symbol plus_nat: El (nat ~> nat ~> nat)
 set infix left 4 "+" ≔ plus_nat
-constant symbol s_not_z: ε (∀ (λx, ¬ (eqnat z (s x))))
-rule ε (eqnat (s $n) (s $m)) ↪ ε (eqnat $n $m) with ε (eqnat z z) ↪ ε true
+constant symbol s_not_z: Prf (∀ (λx, ¬ (eqnat z (s x))))
+rule Prf (eqnat (s $n) (s $m)) ↪ Prf (eqnat $n $m) with Prf (eqnat z z) ↪ Prf true
 rule $n + z ↪ $n with $n + s $m ↪ s ($n + $m)
 symbol nat_ind:
-  ε (∀ {nat ~> bool} (λp, (p z) ⇒ (∀ (λn, p n ⇒ p (s n))) ⇒ (∀ (λn, p n))))
+  Prf (∀ {nat ~> bool} (λp, (p z) ⇒ (∀ (λn, p n ⇒ p (s n))) ⇒ (∀ (λn, p n))))
 
 // System T
-symbol rec_nat: η nat → η nat → (η nat → η nat → η nat) → η nat
+symbol rec_nat: El nat → El nat → (El nat → El nat → El nat) → El nat
 rule rec_nat z $t0 _ ↪ $t0
 rule rec_nat (s $u) $t0 $ts ↪ $ts $u (rec_nat $u $t0 $ts)
 
 definition mult a b ≔ rec_nat a z (λ_ r, b + r)
 
-symbol times_nat: η (nat ~> nat ~> nat)
+symbol times_nat: El (nat ~> nat ~> nat)
 set infix left 5 "*" ≔ times_nat
 rule z * _ ↪ z
 with $n * (s $m) ↪ $n + ($n * $m)
@@ -40,13 +40,13 @@ with _ * z ↪ z // (times_z_left)
 // Declaration of a top type
 constant symbol frac: Set
 
-symbol eqfrac: η (frac ~> frac ~> bool)
+symbol eqfrac: El (frac ~> frac ~> bool)
 
-theorem z_plus_n_n: ε (∀ (λn, eqnat (z + n) n))
+theorem z_plus_n_n: Prf (∀ (λn, eqnat (z + n) n))
 proof
   assume n
   refine nat_ind (λn, eqnat (z + n) n) _ _ n
-  refine λx: ε false, x
+  refine λx: Prf false, x
   assume n0 Hn
   apply Hn
 qed
@@ -54,35 +54,35 @@ qed
 // The following theorem allows to remove rule (times_z_left)
 // but doing so would require to have eqnat transitivity, which requires some
 // more work. So it is left for now.
-theorem n_times_z_z: ε (∀ (λn, eqnat (z * n) z))
+theorem n_times_z_z: Prf (∀ (λn, eqnat (z * n) z))
 proof
   assume n
   refine nat_ind (λn, eqnat (z * n) z) _ _ n
-  refine λx: ε false, x
+  refine λx: Prf false, x
   assume n0 Hn
   refine Hn
 qed
 
-theorem times_comm: ε (∀ (λa, ∀ (λb, eqnat (a * b) (b * a))))
+theorem times_comm: Prf (∀ (λa, ∀ (λb, eqnat (a * b) (b * a))))
 proof
 admit
 
 definition nznat_p ≔ λn, ¬ (eqnat z n)
 definition nznat ≔ psub nznat_p
 
-theorem nzprod: ε (∀ {nznat} (λx, ∀ {nznat} (λy, nznat_p (fst x * fst y))))
+theorem nzprod: Prf (∀ {nznat} (λx, ∀ {nznat} (λy, nznat_p (fst x * fst y))))
 proof
 admit
 
 // Building rationals from natural numbers
-symbol div: η (nat ~> nznat ~> frac)
+symbol div: El (nat ~> nznat ~> frac)
 set infix left 6 "/" ≔ div
 rule eqfrac ($a / $b) ($c / $d) ↪ eqnat ($a * (fst $d)) ((fst $b) * $c)
 
-// rule ε (nat_p ($n / pair $n _)) ↪ ε true
+// rule Prf (nat_p ($n / pair $n _)) ↪ Prf true
 // Non linear rules break confluence
 
-symbol times_frac: η (frac ~> frac ~> frac)
+symbol times_frac: El (frac ~> frac ~> frac)
 rule times_frac ($a / $b) ($c / $d)
    ↪ let denom ≔ fst $b * (fst $d) in
      let prf ≔ nzprod $b $d in
@@ -92,7 +92,7 @@ rule times_frac ($a / $b) ($c / $d)
 definition one_nz ≔ pair {nat} {nznat_p} (s z) (s_not_z z)
 
 theorem right_cancel:
-  ε (∀ (λa, ∀ (λb, eqfrac (times_frac (a / b) (fst b / one_nz)) (a / one_nz))))
+  Prf (∀ (λa, ∀ (λb, eqfrac (times_frac (a / b) (fst b / one_nz)) (a / one_nz))))
 proof
   assume x y
   simpl
diff --git a/paper/rat_poly.lp b/paper/rat_poly.lp
index 4828761cda528b9c11644f48b271580d9492675c..44cab5d31d303277c6d3ffc6908d07e29b249f25 100644
--- a/paper/rat_poly.lp
+++ b/paper/rat_poly.lp
@@ -12,39 +12,39 @@ rule μ rat ↪ rat
 // rule topcast {rat} $x ↪ $x
 // rule downcast_ rat $e ↪ $e
 
-constant symbol z: η rat
+constant symbol z: El rat
 
-constant symbol eq: η (rat ~> rat ~> bool)
+constant symbol eq: El (rat ~> rat ~> bool)
 set infix 3 "=" ≔ eq
 
 // Definition of a sub-type of ‘rat’
-symbol nat_p: η (rat ~> bool) // Recogniser
+symbol nat_p: El (rat ~> bool) // Recogniser
 definition nat ≔ psub nat_p
 
 // z is a natural number
-constant symbol z_nat: ε (nat_p z)
+constant symbol z_nat: Prf (nat_p z)
 
 // Presburger arithmetics
-constant symbol s: η (nat ~> nat)
-symbol plus: η (rat ~> rat ~> rat)
+constant symbol s: El (nat ~> nat)
+symbol plus: El (rat ~> rat ~> rat)
 set infix left 4 "+" ≔ plus
 
 constant symbol s_not_z:
-  ε (∀ {nat} (λx, ¬ (z = (cast rat (λx, x) (s x) (λx, x)))))
+  Prf (∀ {nat} (λx, ¬ (z = (cast rat (λx, x) (s x) (λx, x)))))
 
-rule ε (z = z) ↪ ε true
-rule ε ((cast rat _ (s $n) _) = (cast rat _ (s $m) _))
-   ↪ ε ((cast rat (λx, x) $n (λx, x)) = (cast rat (λx, x) $m (λx, x)))
+rule Prf (z = z) ↪ Prf true
+rule Prf ((cast rat _ (s $n) _) = (cast rat _ (s $m) _))
+   ↪ Prf ((cast rat (λx, x) $n (λx, x)) = (cast rat (λx, x) $m (λx, x)))
 
 theorem plus_closed_nat:
-  ε (∀ {nat} (λn, (∀ {nat} (λm, nat_p ((cast rat (λx, x) n (λx, x))
+  Prf (∀ {nat} (λn, (∀ {nat} (λm, nat_p ((cast rat (λx, x) n (λx, x))
                                        + (cast rat (λx, x) m (λx, x)))))))
 proof
 admit
 
 // It’s just true ∧ plus_closed_nat n m
 theorem tcc1:
-  ε (∀ {nat} (λn, (∀ {nat}
+  Prf (∀ {nat} (λn, (∀ {nat}
                      (λm, true
                           ∧ (λ_, nat_p (plus (cast rat (λx, x) n (λx, x))
                                              (cast rat (λx, x) m (λx, x))))))))
@@ -61,52 +61,52 @@ with (cast {nat} rat _ $n _) + (cast {nat} rat _ (s $m) _)
               (tcc1 $n $m)))
           (λx, x)
 
-theorem tcc2: ε (true ∧ (λ_, nat_p z))
+theorem tcc2: Prf (true ∧ (λ_, nat_p z))
 proof
 admit
 
 // symbol nat_ind:
-//   ε (∀ {nat ~> bool}
+//   Prf (∀ {nat ~> bool}
 //        (λp, (p (cast nat (λx, x) z _))
 //             ⇒ (λ_, (∀ {nat} (λn, p n ⇒ (λ_, p (s n))))) ⇒ (λ_, (∀ {nat} (λn, p n)))))
 
-// theorem z_plus_n_n: ε (∀ (λn, eqnat (z + n) n))
+// theorem z_plus_n_n: Prf (∀ (λn, eqnat (z + n) n))
 // proof
 //   assume n
 //   refine nat_ind (λn, eqnat (z + n) n) _ _ n
-//   refine λx: ε false, x
+//   refine λx: Prf false, x
 //   assume n0 Hn
 //   apply Hn
 // qed
 
-symbol times: η (rat ~> rat ~> rat)
+symbol times: El (rat ~> rat ~> rat)
 set infix left 5 "*" ≔ times
 rule z * _ ↪ z
 with _ * z ↪ z // (times_z_left)
 
-theorem times_comm: ε (∀ (λa, ∀ (λb, eq (a * b) (b * a))))
+theorem times_comm: Prf (∀ (λa, ∀ (λb, eq (a * b) (b * a))))
 proof
 admit
 
-definition nznat_p (n: η nat) ≔ ¬ (eq z (cast rat (λx, x) n (λx, x)))
+definition nznat_p (n: El nat) ≔ ¬ (eq z (cast rat (λx, x) n (λx, x)))
 definition nznat ≔ psub nznat_p
 
-symbol frac: η (nat ~> nznat ~> rat)
+symbol frac: El (nat ~> nznat ~> rat)
 set infix left 6 "/" ≔ frac
-rule ε (eq ($a / $b) ($c / $d))
-   ↪ ε (eq (times (cast rat (λx, x) $a (λx, x))
+rule Prf (eq ($a / $b) ($c / $d))
+   ↪ Prf (eq (times (cast rat (λx, x) $a (λx, x))
                   (cast rat (λx, x) $d (λx, x)))
            (times (cast rat (λx, x) $b (λx, x))
                   (cast rat (λx, x) $c (λx, x))))
 
 theorem prod_closed_nat:
-  ε (∀ {nat} (λn, ∀ {nat} (λm, nat_p (times (cast rat (λx, x) n (λx, x))
+  Prf (∀ {nat} (λn, ∀ {nat} (λm, nat_p (times (cast rat (λx, x) n (λx, x))
                                             (cast rat (λx, x) m (λx, x))))))
 proof
 admit
 
 theorem tcc4:
-  ε (∀ {nznat} (λn, ∀ {nznat} (λm, and true
+  Prf (∀ {nznat} (λn, ∀ {nznat} (λm, and true
                                        (λ_, nat_p
                                             (times (cast {nznat} rat (λx, x) n (λx, x))
                                                    (cast {nznat} rat (λx, x) m (λx, x)))))))
@@ -114,7 +114,7 @@ proof
 admit
 
 theorem tcc3:
-  ε (∀ {nznat}
+  Prf (∀ {nznat}
        (λn, (∀ {nznat}
                (λm, true
                     ∧ (λ_, nznat_p
@@ -125,7 +125,7 @@ proof
 admit
 
 theorem tcc5:
-  ε (∀ {nat} (λn, ∀ {nat} (λm, and true
+  Prf (∀ {nat} (λn, ∀ {nat} (λm, and true
                                    (λ_,
                                     nat_p (times (cast {nat} rat (λx, x) n (λx, x))
                                                  (cast {nat} rat (λx, x) m (λx ,x)))))))
@@ -147,12 +147,12 @@ admit
 //                        (cast {nznat} rat (λx, x) $d (λx, x)))
 //                 (tcc3 $b $d))
 
-theorem tcc6: ε (and true (λ_, nat_p z))
+theorem tcc6: Prf (and true (λ_, nat_p z))
 proof
 admit
 definition one ≔ s (cast nat (λx, x) z tcc6)
 // FIXME: same as above
-// theorem tcc7: ε (and true
+// theorem tcc7: Prf (and true
 //                      (λ_, and (nat_p (cast rat (λx, x) one (λx, x)))
 //                               (λ_, nznat_p one)) )
 // proof
diff --git a/prelude/functions.lp b/prelude/functions.lp
index efdf9dd8cd482387eb6aed582f24cbc647dd94a2..fe6835edd13415c91740791151cdf10f8d57e2c2 100644
--- a/prelude/functions.lp
+++ b/prelude/functions.lp
@@ -8,9 +8,9 @@ require open personoj.prelude.logic
 //
 
 symbol extensionality_postulate:
-  ε (∀B (λD, ∀B (λR,
-                 ∀ (λf: η (D ~> R),
-                    ∀ (λg: η (D ~> R), iff (∀ (λx, f x = g x)) (f = g))))))
+  Prf (∀B (λD, ∀B (λR,
+                 ∀ (λf: El (D ~> R),
+                    ∀ (λg: El (D ~> R), iff (∀ (λx, f x = g x)) (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 ffcae6ffcdc7abdd6be1762c41d7ea97b27bcae5..856bce41fd9fb5a94e7815aaf9f040cf20974fee 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -14,7 +14,7 @@ require open personoj.encodings.builtins
 //
 // Notequal
 //
-// definition neq {T: Set} (x y: η T) ≔ ¬ (x = y)
+// definition neq {T: Set} (x y: El T) ≔ ¬ (x = y)
 // symbol neq: χ (∀S (λt, scheme (t ~> t ~> bool)))
 // rule neq _ $x $y ↪ ¬ ($x = $y)
 // set infix left 2 "/=" ≔ neq
@@ -28,11 +28,11 @@ require open personoj.encodings.builtins
 //
 // boolean_props
 // Slightly modified from the prelude
-constant symbol bool_exclusive: ε (neq {bool} false true)
+constant symbol bool_exclusive: Prf (neq {bool} false true)
 constant symbol bool_inclusive:
-  ε (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
+  Prf (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
 
-theorem excluded_middle: ε (∀ {bool} (λa, a ∨ (λ_, ¬ a)))
+theorem excluded_middle: Prf (∀ {bool} (λa, a ∨ (λ_, ¬ a)))
 proof
   assume x f
   refine f
@@ -41,12 +41,12 @@ qed
 //
 // xor_def
 //
-definition xor (a b: η bool) ≔ neq {bool} a b
+definition xor (a b: El bool) ≔ neq {bool} a b
 
 // PVS solves that kind of things thanks to the (bddsimp) tactic which uses an
 // external C program
 theorem xor_def:
-  ε (∀ {bool} (λa, ∀ {bool} (λb, eq {bool} (xor a b)
+  Prf (∀ {bool} (λa, ∀ {bool} (λb, eq {bool} (xor a b)
                                     (if {bool} a (λ_, ¬ b) (λ_, b)))))
 proof
   set prover "Alt-Ergo"
@@ -76,32 +76,32 @@ definition SETOF ≔ pred
 //
 constant
 symbol If_true
-     : ε (∀B (λt, ∀ (λx, ∀ {t} (λy, if true (λ_, x) (λ_, y) = x))))
+     : Prf (∀B (λt, ∀ (λx, ∀ {t} (λy, if true (λ_, x) (λ_, y) = x))))
 constant
 symbol If_false
-     : ε (∀B (λt, ∀ (λx, ∀ {t} (λy, if false (λ_, x) (λ_, y) = y))))
+     : Prf (∀B (λt, ∀ (λx, ∀ {t} (λy, if false (λ_, x) (λ_, y) = y))))
 
 theorem if_same
-      : ε (∀B (λt, ∀ {bool} (λb, ∀ (λx: η t, if b (λ_, x) (λ_, x) = x))))
+      : Prf (∀B (λt, ∀ {bool} (λb, ∀ (λx: El t, if b (λ_, x) (λ_, x) = x))))
 proof
 admit
 
-constant symbol reflexivity_of_equals: ε (∀B (λt, ∀ (λx: η t, x = x)))
+constant symbol reflexivity_of_equals: Prf (∀B (λt, ∀ (λx: El t, x = x)))
 set builtin "refl" ≔ reflexivity_of_equals
 
 constant
 symbol transitivity_of_equals
-     : ε (∀B (λt,
-                ∀(λx: η t,
-                    ∀(λy: η t,
-                        ∀(λz: η t, (x = y) ∧ (λ_, y = z) ⊃ (λ_, x = z))))))
+     : Prf (∀B (λt,
+                ∀(λx: El t,
+                    ∀(λy: El t,
+                        ∀(λz: El t, (x = y) ∧ (λ_, y = z) ⊃ (λ_, x = z))))))
 
 constant
 symbol symmetry_of_equals
-     : ε (∀B (λt, ∀ (λx: η t, (∀ (λy: η t, (x = y) ⊃ (λ_, y = x))))))
+     : Prf (∀B (λt, ∀ (λx: El t, (∀ (λy: El t, (x = y) ⊃ (λ_, y = x))))))
 
 // Not in prelude!
-theorem eqind {t} x y: ε (x = y) → Πp: η t → Bool, ε (p y) → ε (p x)
+theorem eqind {t} x y: Prf (x = y) → Πp: El t → Bool, Prf (p y) → Prf (p x)
 proof
   assume t x y heq
   apply symmetry_of_equals t x y heq
@@ -113,28 +113,28 @@ set builtin "eqind" ≔ eqind
 //
 
 theorem lift_if1:
-  ε (∀B (λs: θ {|set|},
+  Prf (∀B (λs: θ {|set|},
            ∀B (λt: θ {|set|},
                  ∀ {bool}
                    (λa,
-                      ∀ (λx: η s,
-                           ∀ (λy: η s,
-                                ∀ (λf: η (s ~> t),
+                      ∀ (λx: El s,
+                           ∀ (λy: El s,
+                                ∀ (λf: El (s ~> t),
                                      f (if a (λ_, x) (λ_, y))
                                      = if a (λ_, f x) (λ_, f y))))))))
 proof
 admit
 
 theorem lift_if2:
-  ε (∀B (λs,
+  Prf (∀B (λs,
            ∀ {bool}
              (λa,
                 ∀ {bool}
                   (λb,
                      ∀ {bool}
                        (λc,
-                          ∀ (λx: η s,
-                               ∀ (λy: η s,
+                          ∀ (λx: El s,
+                               ∀ (λy: El s,
                                     if (if {bool} a (λ_, b) (λ_, c))
                                        (λ_, x)
                                        (λ_, y)
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index fb5dd5e5eca93e1eb30d9127db15706d0278bb93..4f0a8977596c8d8b10535d8b6119ee13841b52e0 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -10,21 +10,21 @@ require open personoj.encodings.subtype_poly
 // Theory numbers
 //
 constant symbol number: θ {|set|}
-rule η (μ number) ↪ η number
+rule El (μ number) ↪ El number
 
 //
 // Theory number_fields
 //
-constant symbol field_pred: η (PRED number)
+constant symbol field_pred: El (PRED number)
 definition number_field ≔ psub field_pred
 // number_field is an uninterpreted subtype
 definition numfield ≔ number_field
 
-symbol insertnum: η {|!Number!|} → η numfield
+symbol insertnum: El {|!Number!|} → El numfield
 
-symbol {|+|}: η (numfield ~> numfield ~> numfield)
+symbol {|+|}: El (numfield ~> numfield ~> numfield)
 set infix left 6 "+" ≔ {|+|}
-symbol {|-|}: η (numfield ~> numfield ~> numfield)
+symbol {|-|}: El (numfield ~> numfield ~> numfield)
 set infix 6 "-" ≔ {|-|}
 
 // Other way to extend type of functions,
@@ -35,10 +35,10 @@ set infix 6 "-" ≔ {|-|}
 // rule ty_plus numfield numfield ↪ numfield
 
 constant
-symbol commutative_add : ε (∀ (λx, ∀ (λy, x + y = y + x)))
+symbol commutative_add : Prf (∀ (λx, ∀ (λy, x + y = y + x)))
 constant
 symbol associative_add
-     : ε (∀ (λx, ∀ (λy, ∀ (λz, x + (y + z) = (x + y) + z))))
+     : Prf (∀ (λ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)
 
@@ -46,17 +46,17 @@ symbol associative_add
 //
 // reals
 //
-constant symbol real_pred: η (pred numfield)
+constant symbol real_pred: El (pred numfield)
 definition real ≔ psub real_pred
 
-symbol Num_real: ε (∀ (λx: η {|!Number!|}, real_pred (insertnum x)))
+symbol Num_real: Prf (∀ (λx: El {|!Number!|}, real_pred (insertnum x)))
 
 // Built in the PVS typechecker
 
 // TODO: metavariables left
 // definition nonzero_real ≔
 //   psub {real}
-//        (λx: η real,
+//        (λx: El real,
 //         neq {_} x (cast {_} {real} (λx, x) (insertnum 0) _))
 
 // symbol closed_plus_real: Π(x y: Term real),
diff --git a/sandbox/boolops.lp b/sandbox/boolops.lp
index 51d92349bd86e37a32abe83e0aa9531f01f9ddff..fc9ae23ec7cd89b6f6c1d9197aa4574d1ee47c15 100644
--- a/sandbox/boolops.lp
+++ b/sandbox/boolops.lp
@@ -10,7 +10,7 @@ require personoj.paper.rat as Q
 set builtin "0" ≔ Q.z
 set builtin "+1" ≔ Q.s
 
-theorem exfalso (_: ε false) (P: Bool): ε P
+theorem exfalso (_: Prf false) (P: Bool): Prf P
 proof
   assume false P
   refine false P
@@ -18,15 +18,15 @@ qed
 
 // Computes ⊥ ⊃ (1/0 = 1/0)
 compute false ⊃ (λh,
-                 let ooz ≔ Q.frac 1 (pair 0 (exfalso h (Q.nznat_p 0))) in
+                 let ooz ≔ Q.div 1 (pair 0 (exfalso h (Q.nznat_p 0))) in
                  eq ooz ooz)
 
-definition Qone ≔ Q.frac 1 (pair 1 (Q.s_not_z 0))
+definition Qone ≔ Q.div 1 (pair 1 (Q.s_not_z 0))
 
 // If ⊥ then 1/0 else 1/1
-compute if false (λh: ε false,
+compute if false (λh: Prf false,
                   let z ≔ pair 0 (exfalso h (Q.nznat_p 0)) in
-                  Q.frac 1 z)
+                  Q.div 1 z)
                  (λ_, Qone)
 
 // TODO: some work with excluded middle to have the same proposition
diff --git a/tests/pairs.lp b/tests/pairs.lp
index 869f3d4193bad1fb08bce14d57707c0c56e01cff..102cfce39ed5b4db0ee8d79bfc2e645c8b27a9b2 100644
--- a/tests/pairs.lp
+++ b/tests/pairs.lp
@@ -5,11 +5,11 @@ require open personoj.encodings.prenex
 require open personoj.encodings.pairs
 
 symbol nat: Set
-symbol plus: η ((Σ nat (λ_, nat)) ~> nat)
+symbol plus: El ((Σ nat (λ_, nat)) ~> nat)
 
-symbol z: η nat
-symbol s: η (nat ~> nat)
+symbol z: El nat
+symbol s: El (nat ~> nat)
 set builtin "0" ≔ z
 set builtin "+1" ≔ s
 
-assert plus (pair_ss 3 4): η nat
+assert plus (pair_ss 3 4): El nat
diff --git a/tests/tuple.lp b/tests/tuple.lp
index 32c925b36d621cd4d27ff5ea273be7d007ee1de8..87b4280aef5622acea2fb360a7295ad746e0fa06 100644
--- a/tests/tuple.lp
+++ b/tests/tuple.lp
@@ -9,7 +9,7 @@ constant symbol rat: Set
 
 
 set verbose 3
-constant symbol zn: η nat
-constant symbol zq: η rat
+constant symbol zn: El nat
+constant symbol zq: El rat
 definition tuple_zz ≔ tuple_cons _ zn _ (tuple_cons _ zq _ tuple_nil)
 // assert tuple_car (type_cons nat _) (tuple_cons _ zn _ (tuple_cons _ zq _ tuple_nil)) ≡ zn
diff --git a/tests/vect.lp b/tests/vect.lp
index 865eee4da027d42143bc41b75245a2a054b9806d..cb234bfda28a89a4ac8ae0841a11cc99e0f23b77 100644
--- a/tests/vect.lp
+++ b/tests/vect.lp
@@ -5,4 +5,4 @@ require open personoj.encodings.prenex
 
 symbol nat: θ {|set|}
 symbol vect: ϕ (∀K (λ_, scheme_k (nat *> {|set|})))
-assert vect: Set → η nat → Set
+assert vect: Set → El nat → Set