diff --git a/encodings/ad_hoc.lp b/encodings/ad_hoc.lp
index d8576235fbd0b9ea6dcd3a9afc2d20ad92b3f7a5..1301bf0ae54ca35bf83c1094e7054775194499c8 100644
--- a/encodings/ad_hoc.lp
+++ b/encodings/ad_hoc.lp
@@ -1,6 +1,6 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require open personoj.encodings.subtype2
+require open personoj.encodings.subtype
 
 // A possible encoding of ad-hoc polymorphism.
 // Should be made prenex.
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index ccf8593834208c68bd9eeb6165cd3cc50a0e87f9..f01d8af4fd320bdab7459107cf913dabd12d7dfa 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -2,69 +2,88 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.bool_hol
 
-set declared "↑"
-set declared "↓"
-set declared "↕"
 set declared "μ"
 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_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)
-     : ε (∀ (λx, (r1 x) ⊑ (r2 x))) → ε ((arrd r1) ⊑ (arrd r2))
+set declared "↑"
+set declared "↓"
 
 // Maximal supertype
 symbol μ: Set → Set
 rule μ (psub {$T} _) ↪ μ $T
 with μ ($T ~> $U) ↪ $T ~> (μ $U)
+with μ (arrd $b) ↪ arrd (λx, μ ($b x) )
 with μ (μ $T) ↪ μ $T // FIXME: can be proved
 
-rule μ bool ↪ bool
-// Direct super-type
-symbol μ₀: Set → Set
-rule μ₀ (psub {$T} _) ↪ μ₀ $T
+set unif_rule μ $x ≡ μ $y ↪ $x ≡ $y
+// set unif_rule μ $x ≡ $y ↪ μ $x ≡ μ $y
 
-compute λT: Set, μ (μ T)
+symbol π {T: Set}: η (μ T) → Bool
 
-// Constraints
-symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) → η A → η B
-definition ↑ {A} {B} ≔ upcast {A} {B}
-rule upcast {$t} {$t} _ $x ↪ $x
+// Casting from/to maximal supertype
+constant symbol maxcast {t: Set}: η t → η (μ t)
+constant symbol downcast {t: Set} (x: η (μ t)): ε (π {μ t} x) → η t
+definition ↑ {t} ≔ maxcast {t}
+definition ↓ {t} ≔ downcast {t}
 
-theorem sub_of_sup A: ε (A ⊑ μ A)
-proof
-admit
-
-symbol π {T: Set}: η (μ T) → Bool
-symbol downcast {A: Set} {B: Set} (_: ε (B ⊑ A))
-                (a: η A) (_: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a)))
-     : η B
-definition ↓ {A} {B} ≔ downcast {A} {B}
+// rule η (maxcast (maxcast $t)) ↪ η (maxcast $t)
 
 set flag "print_implicits" on
-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))
-// FIXME: does not type check because μ (μ $T) is not reduced to μ $T
+set debug +u
+rule π {$t ~> $u} ↪ λx: η $t → η (μ $u), ∀ (λy, π (x y))
+with π {psub {$t} $a}
+   ↪ λx: η (μ $t), (π {μ $t} x) ∧ (λy: ε (π {μ $t} x), $a (↓ x y))
+with π {arrd $b}
+   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π {μ ($b y)} (x y))
+
+rule ε (π (maxcast _)) ↪ ε true // FIXME: to  be justified
+
+// FIXME: is protected needed?
+protected constant symbol max_eq: Set → Set → Bool
+set infix 6 "≃" ≔ max_eq
 
-constant symbol compatible: Set → Set → Bool
-set infix left 6 "≃" ≔ compatible
-constant symbol compcast {t: Set} {u: Set}: ε (t ≃ u) → η t → η u
-definition ↕ {t} {u} ≔ compcast {t} {u}
+injective symbol eqcast {fr: Set} {to: Set}: ε (fr ≃ to) → η fr → η to
 
-definition comp (t: Set) (u: Set) ≔ μ t ≃ μ u
-set infix 6 "∼" ≔ comp
+definition compatible (t u: Set) ≔ μ t ≃ μ u
+set infix 6 "~" ≔ compatible
 
-rule ε (bool ≃ bool) ↪ ε true
+// The one true cast
+injective symbol cast {fr: Set} {to: Set} (comp: ε (fr ~ to)) (x: η fr):
+// Proof that [x] verifies the constraints of [to]
+  let xtop : η (μ fr) ≔ maxcast x in
+  let x_to_top: η (μ to) ≔ eqcast comp xtop in
+  ε (π x_to_top) → η to
 
+rule cast {$t} {$t} _ $x _ ↪ $x
+
+theorem comp_same_cstr_cast
+        (fr to: Set)
+        (comp: ε (μ fr ≃ μ to))
+        (_: ε (eq {μ fr ~> bool}
+                  (Ï€ {fr})
+                  (λx, π {to} (eqcast comp x))))
+        (x: η fr)
+      : let xtop ≔ maxcast x in
+        let x_to_top ≔ eqcast comp xtop in
+        ε (π x_to_top)
+proof
+  assume fr to comp eq_cstr x
+  refine eq_cstr (λf, f (maxcast x)) _
+  refine λx: ε false, x
+qed
+
+set flag "print_implicits" on
+rule ε ($t ≃ $t) ↪ ε true
 rule ε (($t1 ~> $u1) ≃ ($t2 ~> $u2))
    ↪ ε ((μ $t1 ≃ μ $t2)
         ∧ (λh,
-           (eq {μ $t1 ~> bool} (π {$t1}) (λx: η (μ $t1), π {$t2} (↕ h x)))
-               ∧ (λ_, $u1 ≃ $u2)))
+           (eq {μ $t1 ~> bool} (π {$t1}) (λx: η (μ $t1), π {$t2} (eqcast h x)))
+          ∧ (λ_, $u1 ≃ $u2)))
+with ε ((arrd {$t1} $u1) ≃ (arrd {$t2} $u2))
+   ↪ ε ((μ $t1 ≃ μ $t2)
+        ∧ (λh,
+           (eq {μ $t1 ~> bool} π (λx, π (eqcast h x)))
+           ∧ (λh', ∀
+               (λx: η $t1,
+                ($u1 x) ≃ ($u2 (cast {$t1} {$t2} h x
+                                     (comp_same_cstr_cast $t1 $t2 h h' x)))))))
diff --git a/encodings/subtype2.lp b/encodings/subtype2.lp
deleted file mode 100644
index f01d8af4fd320bdab7459107cf913dabd12d7dfa..0000000000000000000000000000000000000000
--- a/encodings/subtype2.lp
+++ /dev/null
@@ -1,89 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
-
-set declared "μ"
-set declared "μ₀"
-set declared "Ï€"
-set declared "↑"
-set declared "↓"
-
-// Maximal supertype
-symbol μ: Set → Set
-rule μ (psub {$T} _) ↪ μ $T
-with μ ($T ~> $U) ↪ $T ~> (μ $U)
-with μ (arrd $b) ↪ arrd (λx, μ ($b x) )
-with μ (μ $T) ↪ μ $T // FIXME: can be proved
-
-set unif_rule μ $x ≡ μ $y ↪ $x ≡ $y
-// set unif_rule μ $x ≡ $y ↪ μ $x ≡ μ $y
-
-symbol π {T: Set}: η (μ T) → Bool
-
-// Casting from/to maximal supertype
-constant symbol maxcast {t: Set}: η t → η (μ t)
-constant symbol downcast {t: Set} (x: η (μ t)): ε (π {μ t} x) → η t
-definition ↑ {t} ≔ maxcast {t}
-definition ↓ {t} ≔ downcast {t}
-
-// rule η (maxcast (maxcast $t)) ↪ η (maxcast $t)
-
-set flag "print_implicits" on
-set debug +u
-rule π {$t ~> $u} ↪ λx: η $t → η (μ $u), ∀ (λy, π (x y))
-with π {psub {$t} $a}
-   ↪ λx: η (μ $t), (π {μ $t} x) ∧ (λy: ε (π {μ $t} x), $a (↓ x y))
-with π {arrd $b}
-   ↪ λx: η (arrd (λx, μ ($b x))), ∀ (λy, π {μ ($b y)} (x y))
-
-rule ε (π (maxcast _)) ↪ ε true // FIXME: to  be justified
-
-// FIXME: is protected needed?
-protected constant symbol max_eq: Set → Set → Bool
-set infix 6 "≃" ≔ max_eq
-
-injective symbol eqcast {fr: Set} {to: Set}: ε (fr ≃ to) → η fr → η to
-
-definition compatible (t u: Set) ≔ μ t ≃ μ u
-set infix 6 "~" ≔ compatible
-
-// The one true cast
-injective symbol cast {fr: Set} {to: Set} (comp: ε (fr ~ to)) (x: η fr):
-// Proof that [x] verifies the constraints of [to]
-  let xtop : η (μ fr) ≔ maxcast x in
-  let x_to_top: η (μ to) ≔ eqcast comp xtop in
-  ε (π x_to_top) → η to
-
-rule cast {$t} {$t} _ $x _ ↪ $x
-
-theorem comp_same_cstr_cast
-        (fr to: Set)
-        (comp: ε (μ fr ≃ μ to))
-        (_: ε (eq {μ fr ~> bool}
-                  (Ï€ {fr})
-                  (λx, π {to} (eqcast comp x))))
-        (x: η fr)
-      : let xtop ≔ maxcast x in
-        let x_to_top ≔ eqcast comp xtop in
-        ε (π x_to_top)
-proof
-  assume fr to comp eq_cstr x
-  refine eq_cstr (λf, f (maxcast x)) _
-  refine λx: ε false, x
-qed
-
-set flag "print_implicits" on
-rule ε ($t ≃ $t) ↪ ε true
-rule ε (($t1 ~> $u1) ≃ ($t2 ~> $u2))
-   ↪ ε ((μ $t1 ≃ μ $t2)
-        ∧ (λh,
-           (eq {μ $t1 ~> bool} (π {$t1}) (λx: η (μ $t1), π {$t2} (eqcast h x)))
-          ∧ (λ_, $u1 ≃ $u2)))
-with ε ((arrd {$t1} $u1) ≃ (arrd {$t2} $u2))
-   ↪ ε ((μ $t1 ≃ μ $t2)
-        ∧ (λh,
-           (eq {μ $t1 ~> bool} π (λx, π (eqcast h x)))
-           ∧ (λ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 6e46ddf9380e87534f73264ae5f63cb42cdaf9d6..c0a20bf49c7d93a0915fa84b816b72c40c5797aa 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -1,6 +1,5 @@
-require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
 
 set declared "â„•"
 set declared "â„š+"
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index c3a159852246285a6d1bc9651f3a4500cf31bd54..ad0342203ea29824ef4f344a57dd225cd275b635 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -4,7 +4,7 @@ require open personoj.encodings.bool_hol
 require open personoj.encodings.prenex
 require open personoj.prelude.logic
 require open personoj.encodings.builtins
-require open personoj.encodings.subtype2
+require open personoj.encodings.subtype
 
 //
 // Theory numbers