diff --git a/adlib/cert_f/subtype.lp b/adlib/cert_f/subtype.lp
index 8eb80591bacb07f229ab23aa365bead278d0e8ba..9788f253d7431693cbc3e9698d775949c4ac6341 100644
--- a/adlib/cert_f/subtype.lp
+++ b/adlib/cert_f/subtype.lp
@@ -19,3 +19,7 @@ symbol sub {T S: Term uType}
   (psubt: Term (T ⊑ S)): // Proof of eT ⊑ eS
   Term (forall (λx, imp (P x) (Q (↑ S psubt x)))) ⇒
   Term (Psub T P ⊑ Psub S Q)
+
+// Transitivity of the cast
+rule ↑ {&U} &V &pruv (↑ {&T} &U &prtu &x) →
+  ↑ {&T} &V (trans &T &U &V &prtu &pruv) &x