From 549e25cb6a39b548fa3b7f8518dc88ae7debbdeb Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 4 Mar 2020 16:00:03 +0100
Subject: [PATCH] rule for cast transitivity

---
 adlib/cert_f/subtype.lp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/adlib/cert_f/subtype.lp b/adlib/cert_f/subtype.lp
index 8eb8059..9788f25 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
-- 
GitLab