From b44f769238e4158c683d634e8674cc80636fd69f Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 13:09:14 +0200
Subject: [PATCH] Added coercion lemmas for lsty
---
theories/logrel/session_types.v | 4 ++++
theories/logrel/subtyping.v | 5 +++++
2 files changed, 9 insertions(+)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 5ea8484..2e187d9 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -164,4 +164,8 @@ Section session_types.
do 4 f_equiv. by rewrite iMsg_app_base.
Qed.
+ Lemma lsty_car_app (S T : lsty Σ) :
+ (lsty_car S <++> lsty_car T)%proto ≡ lsty_car (S <++> T).
+ Proof. eauto. Qed.
+
End session_types.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 6a7c3c9..dc6c235 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -45,4 +45,9 @@ Section subtyping.
Proof. rewrite /lty_copyable /=. apply _. Qed.
Global Instance lty_copyable_ne : NonExpansive (@lty_copyable Σ).
Proof. rewrite /lty_copyable /=. solve_proper. Qed.
+
+ Lemma lsty_car_mono (S T : lsty Σ) :
+ (S <: T) -∗ lsty_car S ⊑ lsty_car T.
+ Proof. eauto. Qed.
+
End subtyping.
--
GitLab