diff --git a/README.md b/README.md
index 6dec03fa4ac635ba29a1835e468a7be3d4dab538..50c7be9683ecfb1f34fc26fcee50f6659a76bfe2 100644
--- a/README.md
+++ b/README.md
@@ -30,5 +30,5 @@ fda8752584af52cdc8158a7a80bbe7fce5720616
 - Dedukti types are capitalised  
   `Nat: TYPE`
 - Predicates are suffixed with `_p`  
-  `even_p: Nat → Bool`
+  `even_p: Nat → Prop`
 - Documentation is commented with `///`
diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index 0aa7d98dd07c0e727fd901f34edb7cb9ecf43bc5..b4da3392953fa3b33a4420fbbcd1824451a96b96 100644
--- a/encodings/bool_plus.lp
+++ b/encodings/bool_plus.lp
@@ -5,8 +5,8 @@ require open personoj.encodings.logical
 // It may be generalisable to dependent propositions
 theorem and_intro:
   Prf
-  (∀ {bool} (λa,
-   ∀ {bool} (λb,
+  (∀ {prop} (λa,
+   ∀ {prop} (λb,
    a ⊃ (λ_, b ⊃ (λ_, a ∧ (λ_, b))))))
 proof
   assume A B h0 h1 f
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index c09bdab4ba4530ef4f4c31171e4b70ed82b548a0..374e4dcab75d773233a2e3556c6af1e21cdd7c35 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -24,10 +24,10 @@ constant symbol str_empty: El {|!String!|}
 constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|}
 
 set declared "∃"
-definition ∃ {T: Set} (P: El T → El bool) ≔ ¬ (∀ (λx, ¬ (P x)))
+definition ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λx, ¬ (P x)))
 
 symbol propositional_extensionality:
-  Prf (∀ {bool} (λp, (∀ {bool} (λq, (iff p q) ⊃ (λ_, eq {bool} p q)))))
+  Prf (∀ {prop} (λp, (∀ {prop} (λq, (iff p q) ⊃ (λ_, eq {prop} p q)))))
 
 definition neq {t} x y ≔ ¬ (eq {t} x y)
 set infix left 2 "/=" ≔ neq
diff --git a/encodings/equality.lp b/encodings/equality.lp
index 488f6669ce0c07a3a5b39076f0174defae5ee764..304ca8249992b1bcdd4edf1fb977d6ff7473ed62 100644
--- a/encodings/equality.lp
+++ b/encodings/equality.lp
@@ -4,7 +4,7 @@ require open personoj.encodings.logical
 require open personoj.encodings.prenex
 
 // We don't use prenex encoding to have implicit arguments.
-symbol eq {T: Set}: El T → El T → Bool
+symbol eq {T: Set}: El T → El T → Prop
 set infix left 2 "=" ≔ eq
 set builtin "eq" ≔ eq
 
@@ -12,7 +12,7 @@ definition neq {s: Set} (x y: El s) ≔ ¬ (x = y)
 set infix 2 "≠" ≔ neq
 
 // Leibniz equality
-rule Prf ($x = $y) ↪ Πp: El (_ ~> bool), Prf (p $x) → Prf (p $y)
+rule Prf ($x = $y) ↪ Πp: El (_ ~> prop), Prf (p $x) → Prf (p $y)
 
 // Some theorems for equality
 theorem eq_refl {a: Set} (x: El a): Prf (x = x)
diff --git a/encodings/equality_tup.lp b/encodings/equality_tup.lp
index fa573262a7745e9deb6f8738c76f31fce7670df9..ee8d3855a550393ae36dc4ffaa2daf6eb6fbca7a 100644
--- a/encodings/equality_tup.lp
+++ b/encodings/equality_tup.lp
@@ -6,5 +6,5 @@ require open personoj.encodings.logical
 
 // Equality operates on the maximal supertype. It allows to profit
 // from predicate subtyping for free in the propositional equality.
-symbol eq {t: Set} (_: El (T.t (μ t) (μ t))): Bool
+symbol eq {t: Set} (_: El (T.t (μ t) (μ t))): Prop
 definition neq {t} m ≔ ¬ (@eq t m)
diff --git a/encodings/if.lp b/encodings/if.lp
index 552784c641a976a569f3cb33144345ca85e44f43..8fe288cf2e7ec9addb55b94b63ea1385c4ce7dd3 100644
--- a/encodings/if.lp
+++ b/encodings/if.lp
@@ -3,22 +3,22 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
-definition false ≔ ∀ {bool} (λx, x)
+definition false ≔ ∀ {prop} (λx, x)
 definition true ≔ impd {false} (λ_, false)
 
-symbol eq {s: Set}: El s → El s → El bool
+symbol eq {s: Set}: El s → El s → El prop
 set infix left 6 "=" ≔ eq
 
-definition not p ≔ eq {bool} p false
+definition not p ≔ eq {prop} p false
 set prefix 5 "¬" ≔ not
 
 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
-definition imp p q ≔ if {bool} p q (λ_, true)
+definition and p q ≔ if {prop} p q (λ_, false)
+definition or p q ≔ if {prop} p (λ_, true) q
+definition imp p q ≔ if {prop} p q (λ_, true)
 set infix left 4 "∧" ≔ and
 set infix left 3 "∨" ≔ or
 set infix left 2 "⊃" ≔ imp
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 75843f2598f6f420c849efb602f69f591c16123a..11a2e30d52b931c0969ff38c99b29b9052e52f33 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -1,19 +1,19 @@
 /// Encoding of λHOL
 symbol Kind: TYPE
 symbol Set: TYPE
-symbol Bool: TYPE
+symbol Prop: TYPE
 
 set declared "∀"
 injective symbol El: Set → TYPE
-injective symbol Prf: Bool → TYPE
+injective symbol Prf: Prop → TYPE
 
 constant symbol {|set|}: Kind
-constant symbol bool: Set
+constant symbol prop: Set
 
-rule El bool ↪ Bool
+rule El prop ↪ Prop
 
-constant symbol ∀ {x: Set}: (El x → Bool) → Bool
-constant symbol impd {x: Bool}: (Prf x → Bool) → Bool
+constant symbol ∀ {x: Set}: (El x → Prop) → Prop
+constant symbol impd {x: Prop}: (Prf x → Prop) → Prop
 constant symbol arrd {x: Set}: (El x → Set) → Set
 
 rule Prf (∀ {$X} $P) ↪ Πx: El $X, Prf ($P x)
diff --git a/encodings/logical.lp b/encodings/logical.lp
index 3bfae83ac9b4691774f397c68fce81ee13e6ad93..aa8755b072cfd72d656aee26aec499effd0035ce 100644
--- a/encodings/logical.lp
+++ b/encodings/logical.lp
@@ -1,7 +1,7 @@
 // Definition based on implication
 require open personoj.encodings.lhol
 
-definition false ≔ ∀ {bool} (λx, x)
+definition false ≔ ∀ {prop} (λx, x)
 definition true ≔ impd {false} (λ_, false)
 
 definition not P ≔ impd {P} (λ_, false)
@@ -22,7 +22,7 @@ set builtin "imp" ≔ imp
 set builtin "and" ≔ and
 set builtin "or"  ≔ or
 
-symbol if {s: Set} (p: Bool): (Prf p → El s) → (Prf (¬ p) → El s) → El s
-rule if {bool} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
+symbol if {s: Set} (p: Prop): (Prf p → El s) → (Prf (¬ p) → El s) → El s
+rule if {prop} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
 
 definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index 3ac6e860fb30a540a24650b07bfd3eb4fd04ece4..2b96a639868a80a957c8ffd845860905a183d798 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -11,7 +11,7 @@ require open personoj.encodings.lhol
 set declared "∀K"
 // Quantification for objects of type ‘Set’
 set declared "∀S"
-// Quantification for objects of type ‘Bool’
+// Quantification for objects of type ‘Prop’
 set declared "∀B"
 
 // To interpret PVS sorts
@@ -34,5 +34,5 @@ rule El_s (scheme_s $X) ↪ El $X
 constant symbol ∀S: (Set → SchemeS) → SchemeS
 rule El_s (∀S $e) ↪ Πt: Set, El_s ($e t)
 
-constant symbol ∀B: (Set → Bool) → Bool
+constant symbol ∀B: (Set → Prop) → Prop
 rule Prf (∀B $p) ↪ Πx: Set, Prf ($p x)
diff --git a/encodings/pvs_cert.lp b/encodings/pvs_cert.lp
index cfa4d10b6a43d1e1790ec17ad0700d87131fce42..7e71a605ee03766e15135e531947038633da4ba3 100644
--- a/encodings/pvs_cert.lp
+++ b/encodings/pvs_cert.lp
@@ -3,18 +3,18 @@ require open personoj.encodings.lhol
 
 set declared "μ"
 
-constant symbol psub {x: Set}: (El x → Bool) → Set
-protected symbol pair': Π(t: Set) (p: El t → Bool), El t → El (psub p)
-symbol fst: Π{t: Set} {p: El t → Bool}, El (psub p) → El t
+constant symbol psub {x: Set}: (El x → Prop) → Set
+protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p)
+symbol fst: Π{t: Set} {p: El t → Prop}, El (psub p) → El t
 
-symbol snd {t: Set}{p: El t → Bool} (m: El (psub p)): Prf (p (fst m))
+symbol snd {t: Set}{p: El t → Prop} (m: El (psub p)): Prf (p (fst m))
 
 // Proof irrelevance
-definition pair {t: Set} {p: El t → Bool} (m: El t) (_: Prf (p m))
+definition pair {t: Set} {p: El t → Prop} (m: El t) (_: Prf (p m))
          ≔ pair' t p m
 
 rule fst (pair' _ _ $M) ↪ $M
 
 symbol μ (_: Set): Set
 rule μ (@psub $t _) ↪ μ $t
-with μ bool ↪ bool
+with μ prop ↪ prop
diff --git a/encodings/unif_rules.lp b/encodings/unif_rules.lp
index da819d58e0c9b7834d98ad4d22c352837e66f9ae..ba75150680d33d0b2e75b052e1ffbfc21cc3095f 100644
--- a/encodings/unif_rules.lp
+++ b/encodings/unif_rules.lp
@@ -1,3 +1,3 @@
 require open personoj.encodings.lhol
 
-set unif_rule El $t ≡ Bool ↪ $t ≡ bool
+set unif_rule El $t ≡ Prop ↪ $t ≡ prop
diff --git a/paper/proof_irr.lp b/paper/proof_irr.lp
index 9563c7305bcdae5cdf441a5ec33fa07a41427834..a641fd7865150379e00bbd21e898321410034966 100644
--- a/paper/proof_irr.lp
+++ b/paper/proof_irr.lp
@@ -8,7 +8,7 @@ set declared "â„•"
 constant symbol â„•: Set
 constant symbol z: El â„•
 constant symbol s (_: El â„•): El â„•
-constant symbol leq: El ℕ → El ℕ → Bool
+constant symbol leq: El ℕ → El ℕ → Prop
 set infix left 3 "≤" ≔ leq
 
 // Agda manual
@@ -32,7 +32,7 @@ proof
   refine eq_refl l₁
 qed
 
-constant symbol even_p: El ℕ → Bool
+constant symbol even_p: El ℕ → Prop
 definition even ≔ psub even_p
 
 // Proof irrelevance without K
diff --git a/paper/rat.lp b/paper/rat.lp
index fa213f7f9d5a5c5d12ffca2809af1e93dfa9882b..f9c78a8b079a3b632b1813ed1acb38a210c212b1 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -4,25 +4,25 @@ require open personoj.encodings.pvs_cert
 // Prelude with some logics operator
 definition imp P Q ≔ impd {P} (λ_, Q)
 set infix right 6 "⇒" ≔ imp
-definition false ≔ ∀ {bool} (λx, x)
+definition false ≔ ∀ {prop} (λx, x)
 definition true ≔ false ⇒ false
-symbol not: Bool → Bool
+symbol not: Prop → Prop
 set prefix 8 "¬" ≔ not
-rule Prf (¬ $x) ↪ Prf $x → Π(z: Bool), Prf z
+rule Prf (¬ $x) ↪ Prf $x → Π(z: Prop), Prf z
 
 // Nat top type
 constant symbol nat: Set
 // Presburger arithmetics
 constant symbol s: El (nat ~> nat)
 constant symbol z: El nat
-constant symbol eqnat: El (nat ~> nat ~> bool)
+constant symbol eqnat: El (nat ~> nat ~> prop)
 symbol plus_nat: El (nat ~> nat ~> nat)
 set infix left 4 "+" ≔ plus_nat
 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:
-  Prf (∀ {nat ~> bool} (λp, (p z) ⇒ (∀ (λn, p n ⇒ p (s n))) ⇒ (∀ (λn, p n))))
+  Prf (∀ {nat ~> prop} (λp, (p z) ⇒ (∀ (λn, p n ⇒ p (s n))) ⇒ (∀ (λn, p n))))
 
 // System T
 symbol rec_nat: El nat → El nat → (El nat → El nat → El nat) → El nat
@@ -40,7 +40,7 @@ with _ * z ↪ z // (times_z_left)
 // Declaration of a top type
 constant symbol frac: Set
 
-symbol eqfrac: El (frac ~> frac ~> bool)
+symbol eqfrac: El (frac ~> frac ~> prop)
 
 theorem z_plus_n_n: Prf (∀ (λn, eqnat (z + n) n))
 proof
diff --git a/prelude/logic.lp b/prelude/logic.lp
index d74831bb1189588104fc0f17bd6914ea4441affa..b2ee5924ae0c18167f069ccda0bcfb7f5674e77d 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -5,7 +5,7 @@ require open personoj.encodings.equality
 require open personoj.encodings.prenex
 require open personoj.encodings.builtins
 //
-// Booleans
+// Propeans
 // In [adlib.cert_f.bootstrap]
 
 //
@@ -16,7 +16,7 @@ require open personoj.encodings.builtins
 // Notequal
 //
 // definition neq {T: Set} (x y: El T) ≔ ¬ (x = y)
-// symbol neq: χ (∀S (λt, scheme (t ~> t ~> bool)))
+// symbol neq: χ (∀S (λt, scheme (t ~> t ~> prop)))
 // rule neq _ $x $y ↪ ¬ ($x = $y)
 // set infix left 2 "/=" ≔ neq
 // set infix left 2 "≠" ≔ neq
@@ -27,13 +27,13 @@ require open personoj.encodings.builtins
 //
 
 //
-// boolean_props
+// propean_props
 // Slightly modified from the prelude
-constant symbol bool_exclusive: Prf (neq {bool} false true)
-constant symbol bool_inclusive:
-  Prf (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
+constant symbol prop_exclusive: Prf (neq {prop} false true)
+constant symbol prop_inclusive:
+  Prf (∀ {prop} (λa, ((eq {prop} a false) ∨ (λ_, eq {prop} a true))))
 
-theorem excluded_middle: Prf (∀ {bool} (λa, a ∨ (λ_, ¬ a)))
+theorem excluded_middle: Prf (∀ {prop} (λa, a ∨ (λ_, ¬ a)))
 proof
   assume x f
   refine f
@@ -42,13 +42,13 @@ qed
 //
 // xor_def
 //
-definition xor (a b: El bool) ≔ neq {bool} a b
+definition xor (a b: El prop) ≔ neq {prop} a b
 
 // PVS solves that kind of things thanks to the (bddsimp) tactic which uses an
 // external C program
 theorem xor_def:
-  Prf (∀ {bool} (λa, ∀ {bool} (λb, eq {bool} (xor a b)
-                                    (if {bool} a (λ_, ¬ b) (λ_, b)))))
+  Prf (∀ {prop} (λa, ∀ {prop} (λb, eq {prop} (xor a b)
+                                    (if {prop} a (λ_, ¬ b) (λ_, b)))))
 proof
   set prover "Alt-Ergo"
   set prover_timeout 12
@@ -61,7 +61,7 @@ admit
 //
 // Defined types
 //
-definition pred: El_k (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> bool
+definition pred: El_k (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> prop
 definition PRED ≔ pred
 definition predicate ≔ pred
 definition PREDICATE ≔ pred
@@ -83,7 +83,7 @@ symbol If_false
      : Prf (∀B (λt, ∀ (λx, ∀ {t} (λy, if false (λ_, x) (λ_, y) = y))))
 
 theorem if_same
-      : Prf (∀B (λt, ∀ {bool} (λb, ∀ (λx: El t, if b (λ_, x) (λ_, x) = x))))
+      : Prf (∀B (λt, ∀ {prop} (λb, ∀ (λx: El t, if b (λ_, x) (λ_, x) = x))))
 proof
 admit
 
@@ -101,7 +101,7 @@ symbol symmetry_of_equals
      : Prf (∀B (λt, ∀ (λx: El t, (∀ (λy: El t, (x = y) ⊃ (λ_, y = x))))))
 
 // Not in prelude!
-theorem eqind {t} x y: Prf (x = y) → Πp: El t → Bool, Prf (p y) → Prf (p x)
+theorem eqind {t} x y: Prf (x = y) → Πp: El t → Prop, Prf (p y) → Prf (p x)
 proof
   assume t x y heq
   apply symmetry_of_equals t x y heq
@@ -115,7 +115,7 @@ set builtin "eqind" ≔ eqind
 theorem lift_if1:
   Prf (∀B (λs: Ty {|set|},
            ∀B (λt: Ty {|set|},
-                 ∀ {bool}
+                 ∀ {prop}
                    (λa,
                       ∀ (λx: El s,
                            ∀ (λy: El s,
@@ -127,15 +127,15 @@ admit
 
 theorem lift_if2:
   Prf (∀B (λs,
-           ∀ {bool}
+           ∀ {prop}
              (λa,
-                ∀ {bool}
+                ∀ {prop}
                   (λb,
-                     ∀ {bool}
+                     ∀ {prop}
                        (λc,
                           ∀ (λx: El s,
                                ∀ (λy: El s,
-                                    if (if {bool} a (λ_, b) (λ_, c))
+                                    if (if {prop} a (λ_, b) (λ_, c))
                                        (λ_, x)
                                        (λ_, y)
                                      = if a
diff --git a/sandbox/boolops.lp b/sandbox/boolops.lp
index fc9ae23ec7cd89b6f6c1d9197aa4574d1ee47c15..d3ed0e98a8fa899544eb7b82c5a9a97bb5dabbf2 100644
--- a/sandbox/boolops.lp
+++ b/sandbox/boolops.lp
@@ -3,14 +3,14 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.equality
-require open personoj.encodings.bool_hol
+require open personoj.encodings.prop_hol
 
 require personoj.paper.rat as Q
 
 set builtin "0" ≔ Q.z
 set builtin "+1" ≔ Q.s
 
-theorem exfalso (_: Prf false) (P: Bool): Prf P
+theorem exfalso (_: Prf false) (P: Prop): Prf P
 proof
   assume false P
   refine false P
diff --git a/sandbox/cert_star.lp b/sandbox/cert_star.lp
index a89c98b147ddb90af961b358250ddc79c8c55d93..16b64f796a969daf3781ec0ece90242e509d57e7 100644
--- a/sandbox/cert_star.lp
+++ b/sandbox/cert_star.lp
@@ -1,17 +1,17 @@
 require open personoj.encodings.lhol
-require open personoj.encodings.bool_hol
+require open personoj.encodings.prop_hol
 require open personoj.encodings.tuple
 require open personoj.encodings.pairs
 require open personoj.encodings.prenex
 
-constant symbol psub {t: Set}: (El t → Bool) → Set
+constant symbol psub {t: Set}: (El t → Prop) → Set
 
 // Returns the top type of any type
 symbol pull: Set → Set
 rule pull (psub {$T} _) ↪ pull $T
 with pull (pull $T) ↪ pull $T
 
-symbol tcc (t: Set) (_: El (pull t)): Bool
+symbol tcc (t: Set) (_: El (pull t)): Prop
 
 symbol fst {t: Set} (_: El t): El (pull t)
 
@@ -23,12 +23,12 @@ rule fst (pair' _ $m) ↪ $m
 rule tcc (psub {$t} $a) $x
    ↪ (tcc $t $x) ∧ (λy: Prf (tcc $t $x), $a (pair $t $x y))
 
-rule pull bool ↪ bool
-rule tcc bool _ ↪ true
-rule fst {bool} $x ↪ $x
-rule pair' bool $x _ ↪ $x
+rule pull prop ↪ prop
+rule tcc prop _ ↪ true
+rule fst {prop} $x ↪ $x
+rule pair' prop $x _ ↪ $x
 
-constant symbol equivalent: Set → Set → Bool
+constant symbol equivalent: Set → Set → Prop
 constant symbol eqv_refl (t: Set): Prf (equivalent t t)
 definition compatible t u ≔ equivalent (pull t) (pull u)
 set infix left 2 "~" ≔ compatible
diff --git a/sandbox/numbers.lp b/sandbox/numbers.lp
index 4f0a8977596c8d8b10535d8b6119ee13841b52e0..3f5986d1abed43c6de673de771ccc8e159c046d3 100644
--- a/sandbox/numbers.lp
+++ b/sandbox/numbers.lp
@@ -1,6 +1,6 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.prop_hol
 require open personoj.encodings.prenex
 require open personoj.prelude.logic
 require open personoj.encodings.builtins
@@ -70,7 +70,7 @@ symbol Num_real: Prf (∀ (λx: El {|!Number!|}, real_pred (insertnum x)))
 // // With polymorphic plus
 // rule ty_plus real real ↪ real
 
-// symbol lt (x y: Term real): Term bool
+// symbol lt (x y: Term real): Term prop
 // set infix 6 "<" ≔ lt
 // definition leq (x y: Term real) ≔ (lt x y) ∨ (eq {real} x y)
 // set infix 6 "<=" ≔ leq
@@ -107,7 +107,7 @@ symbol Num_real: Prf (∀ (λx: El {|!Number!|}, real_pred (insertnum x)))
 //   apply S.restr _ _
 // qed
 
-// definition nonzero_rational_pred (x: Term rational): Term bool ≔
+// definition nonzero_rational_pred (x: Term rational): Term prop ≔
 //   neq zero (↑ real rat_is_real x)
 // definition nonzero_rational ≔ Psub nonzero_rational_pred
 // definition nzrat ≔ nonzero_rational
diff --git a/sandbox/rat_generalised.lp b/sandbox/rat_generalised.lp
index ba2082fb18e5abe5147d6abed7582c146715a079..f48b33019896958e9a831bb094ef92b34d239b5b 100644
--- a/sandbox/rat_generalised.lp
+++ b/sandbox/rat_generalised.lp
@@ -1,5 +1,5 @@
 require open personoj.encodings.lhol
-require open personoj.encodings.bool_hol
+require open personoj.encodings.prop_hol
 require open personoj.encodings.cert_star
 
 set infix right 2 "⇒" ≔ imp
@@ -10,10 +10,10 @@ rule tcc rat _ ↪ true
 rule pair' rat $x ↪ $x
 
 constant symbol z: El rat
-symbol eq: El (rat ~> rat ~> bool)
+symbol eq: El (rat ~> rat ~> prop)
 set infix 3 "=" ≔ eq
 
-symbol nat_p : El (rat ~> bool)
+symbol nat_p : El (rat ~> prop)
 definition nat ≔ psub nat_p
 
 constant symbol z_nat : Prf (nat_p z)
diff --git a/sandbox/rat_poly.lp b/sandbox/rat_poly.lp
index 44cab5d31d303277c6d3ffc6908d07e29b249f25..fff47cc1df03583521e35c8e52a238e38a8f4b84 100644
--- a/sandbox/rat_poly.lp
+++ b/sandbox/rat_poly.lp
@@ -1,7 +1,7 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.subtype_poly
-require open personoj.encodings.bool_hol
+require open personoj.encodings.prop_hol
 
 set infix right 2 "⇒" ≔ imp
 
@@ -14,11 +14,11 @@ rule μ rat ↪ rat
 
 constant symbol z: El rat
 
-constant symbol eq: El (rat ~> rat ~> bool)
+constant symbol eq: El (rat ~> rat ~> prop)
 set infix 3 "=" ≔ eq
 
 // Definition of a sub-type of ‘rat’
-symbol nat_p: El (rat ~> bool) // Recogniser
+symbol nat_p: El (rat ~> prop) // Recogniser
 definition nat ≔ psub nat_p
 
 // z is a natural number
@@ -66,7 +66,7 @@ proof
 admit
 
 // symbol nat_ind:
-//   Prf (∀ {nat ~> bool}
+//   Prf (∀ {nat ~> prop}
 //        (λp, (p (cast nat (λx, x) z _))
 //             ⇒ (λ_, (∀ {nat} (λn, p n ⇒ (λ_, p (s n))))) ⇒ (λ_, (∀ {nat} (λn, p n)))))
 
diff --git a/sandbox/subtype_poly.lp b/sandbox/subtype_poly.lp
index 4aad17f492a0ee80b48ab5daadf20cd597482f08..e21c8a8b54a2b4915da39f4d5cc2479af6eb1c32 100644
--- a/sandbox/subtype_poly.lp
+++ b/sandbox/subtype_poly.lp
@@ -1,7 +1,7 @@
 /// Sub-type polymorphism
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.prop_hol
 require open personoj.encodings.tuple
 require open personoj.encodings.pairs
 require open personoj.encodings.prenex
@@ -20,7 +20,7 @@ with μ (σ $T $U) ↪ σ (μ $T) (μ $U)
 with μ (arrd $b) ↪ arrd (λx, μ ($b x))
 with μ (μ $T) ↪ μ $T // FIXME: can be proved
 
-symbol π (T: Set): El (μ T) → Bool
+symbol π (T: Set): El (μ T) → Prop
 rule π ($t ~> $u) ↪ λx: El $t → El (μ $u), ∀ (λy, π $u (x y))
 with π (σ $t $u)
    ↪ λx: El (σ (μ $t) (μ $u)), π $t (σfst x) ∧ (λ_, π $u (σsnd x))
@@ -36,7 +36,7 @@ rule topcast {psub {$t} _} $u ↪ topcast {$t} (fst $u)
 with topcast {$a ~> _} $f ↪ λ(x: El $a), topcast ($f x)
 // TODO: add tuple topcast
 
-symbol top_comp: Set → Set → Bool
+symbol top_comp: Set → Set → Prop
 set infix 6 "≃" ≔ top_comp
 
 definition compatible (t u: Set) ≔ μ t ≃ μ u
@@ -73,7 +73,7 @@ definition cast {fr_t} to_t comp (m: El fr_t) cstr ≔
 theorem comp_same_cstr_cast
         (fr to: Set)
         (comp: Prf (μ fr ≃ μ to))
-        (_: Prf (eq {μ fr ~> bool}
+        (_: Prf (eq {μ fr ~> prop}
                   (Ï€ fr)
                   (λx, π to (@eqcast fr to comp x))))
         (x: El fr)
@@ -88,7 +88,7 @@ rule $t ≃ $t ↪ true
 rule ($t1 ~> $u1) ≃ ($t2 ~> $u2)
    ↪ (μ $t1 ≃ μ $t2)
      ∧ (λh,
-        (eq {μ $t1 ~> bool} (π $t1)
+        (eq {μ $t1 ~> prop} (π $t1)
             (λx: El (μ $t1), π $t2 (@eqcast $t1 $t2 h x)))
         ∧ (λ_, $u1 ≃ $u2))
 rule σ $t1 $u1 ≃ σ $t2 $u2
@@ -96,7 +96,7 @@ rule σ $t1 $u1 ≃ σ $t2 $u2
 with (arrd {$t1} $u1) ≃ (arrd {$t2} $u2)
    ↪ (μ $t1 ≃ μ $t2)
      ∧ (λh,
-        (eq {μ $t1 ~> bool} (π $t1) (λx, π $t2 (@eqcast $t1 $t2 h x)))
+        (eq {μ $t1 ~> prop} (π $t1) (λx, π $t2 (@eqcast $t1 $t2 h x)))
         ∧ (λh', ∀
             (λx: El $t1,
              ($u1 x) ≃ ($u2 (cast {$t1} $t2 h x
diff --git a/sandbox/subtyping.lp b/sandbox/subtyping.lp
index c450cb49919379e536653c60944b0cce5eec0004..d4943191b0764a1d982afc8fe702aa22a3c2a5a1 100644
--- a/sandbox/subtyping.lp
+++ b/sandbox/subtyping.lp
@@ -1,7 +1,7 @@
 /// Sub-type polymorphism
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
+require open personoj.encodings.prop_hol
 require open personoj.encodings.tuple
 require open personoj.encodings.pairs
 require open personoj.encodings.prenex
@@ -23,7 +23,7 @@ definition EqvRefl (t: Set) ≔ CompRefl (Pull t)
 
 // [Dive_p t m] generates the proposition gathering all the predicate
 // on the path to type [t].
-symbol Dive_p (t: Set) (_: El (Pull t)): Bool
+symbol Dive_p (t: Set) (_: El (Pull t)): Prop
 // [dive t m h] types term [m: El (Pull t)] as [El t], with [h] the proof that
 // [m] validates all predicates generated by [Dive_p t m]. It rewrites to a
 // succession of pairs, given a reduction rule below. Proof irrelevant in
@@ -44,7 +44,7 @@ rule Dive_p (psub {$t} $a) $x
 theorem below:
   Prf
   (∀B (λt,
-   ∀ {t ~> bool} (λa,
+   ∀ {t ~> prop} (λa,
    ∀ {Pull t} (λm,
      Dive_p (psub {t} a) m ⊃ (λ_, Dive_p t m)))))
 proof
@@ -57,7 +57,7 @@ admit
 theorem top:
   Prf
   (∀B (λt,
-   ∀ {t ~> bool} (λa,
+   ∀ {t ~> prop} (λa,
    ∀ {Pull t} (λm,
    Dive_p (psub {t} a) m ⊃ (λh, a (dive t m (below t a m h)))))))
 proof
@@ -79,8 +79,8 @@ definition cast {fr_t: Set} (to_t: Set)
                                                comp (pull m))))
          ≔ dive to_t (transfer (Pull fr_t) (Pull to_t) comp (pull m)) tcc
 
-// Some rules on top types are needed, we give them for [bool]
-rule Pull bool ↪ bool // Can't go above [bool]
-with pull bool $x ↪ $x // A term can't be pulled higher than [bool]
-rule Dive_p bool _ ↪ true // A term compatible with [bool] can always be [bool]
-with dive bool $x _ ↪ $x // Diving to [bool] is immediate
+// Some rules on top types are needed, we give them for [prop]
+rule Pull prop ↪ prop // Can't go above [prop]
+with pull prop $x ↪ $x // A term can't be pulled higher than [prop]
+rule Dive_p prop _ ↪ true // A term compatible with [prop] can always be [prop]
+with dive prop $x _ ↪ $x // Diving to [prop] is immediate