From 236cc6132c293bd6a2e1891ba1bff7640c84b794 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 13 Apr 2020 17:07:47 +0200
Subject: [PATCH] Added missing transitivity rule for session type subtyping

---
 theories/logrel/subtyping.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 7bbceb0..a436212 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -197,6 +197,9 @@ Section subtype.
   Lemma lsty_le_refl P : ⊢ P <p: P.
   Proof. iApply iProto_le_refl. Qed.
 
+  Lemma lsty_le_trans P1 P2 P3 : P1 <p: P2 -∗ P2 <p: P3 -∗ P1 <p: P3.
+  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_trans. Qed.
+
   Lemma lsty_send_le A1 A2 P1 P2 :
     ▷ (A2 <: A1) -∗ ▷ (P1 <p: P2) -∗
     (<!!> A1 ; P1) <p: (<!!> A2 ; P2).
-- 
GitLab