diff --git a/adlib/cert_f/subtype.lp b/adlib/cert_f/subtype.lp
index 88432e9a1ddffff8d7a718968f1490bdf9d1aebc..2c66d9cd48c087f9d59b2f3e4725a4b0e34c9242 100644
--- a/adlib/cert_f/subtype.lp
+++ b/adlib/cert_f/subtype.lp
@@ -8,7 +8,8 @@ rule ePsub &A _ ⊑ &A    → true
    asb ∧
    (@forall &A
      (λx, imp (&P x)
-              (&Q (cast &B _ x))))
+              (&Q (↑ &B _ x))))
+// FIXME the rewriting generates a new TCC in the cast
 
 symbol refl eA: Term (eA ⊑ eA)
 symbol carrier eA P: Term (ePsub eA P ⊑ eA)
@@ -16,12 +17,8 @@ symbol carrier eA P: Term (ePsub eA P ⊑ eA)
 symbol transitive (eA eB eC: Term uType):
   Term (eA ⊑ eB) ⇒ Term (eB ⊑ eC) ⇒ Term (eA ⊑ eC)
 
-symbol restriction (c d: Term uType)
-  (p: Term c ⇒ Term bool) (q: Term d ⇒ Term bool):
-  ∀ x: Term c, Term (p x) ⇒ Term (q (↑ d _ x))
-
-symbol destruct (c1 c2: Term uType) p1 p2
-  (ps1: Term (ePsub c1 p1)) (ps2: Term (ePsub c2 p2)):
-    Term (c1 ⊑ c2) ⇒ ∀x: Term c1, Term (p1 x) ⇒
-    Term (p2 (↑ c2 _ x)) ⇒
-    Term (ps1 <| ps2)
+symbol destruct {eT eS: Term uType}
+  (P: Term eT ⇒ Term bool) (Q: Term eS ⇒ Term bool)
+  (psubt: Term (eT ⊑ eS)): // Proof of eT ⊑ eS
+  ∀ x, Term (P x) ⇒ Term (Q (↑ eS psubt x)) ⇒
+  Term (ePsub eT P ⊑ ePsub eS Q)