From 9fc2519f414b10d82830a11b4d61829117c5ae55 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 1 May 2020 20:00:17 +0200
Subject: [PATCH] WIP: Stated the subtyping rules for texist

---
 theories/logrel/subtyping_rules.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 2ca2ea5..db00e0b 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -267,6 +267,25 @@ Section subtyping_rules.
     ⊢ (<??> M A) <: (<?? X> M X).
   Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
 
+  (* Elimination rules need inhabited variant of telescopes in the model *)
+  Lemma lty_le_texist_elim_l {kt : ktele Σ} (M : ltys kt → lmsg Σ) S :
+    (∀ Xs, (<??> M Xs) <: S) -∗
+    (<??.. Xs> M Xs) <: S.
+  Proof. Admitted.
+
+  Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys kt → lmsg Σ) S :
+    (∀ Xs, S <: (<!!> M Xs)) -∗
+    S <: (<!!.. Xs> M Xs).
+  Proof. Admitted.
+
+  Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys kt → lmsg Σ) Ks :
+    ⊢ (<!!.. Xs> M Xs) <: (<!!> M Ks).
+  Proof. Admitted.
+
+  Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys kt → lmsg Σ) Ks :
+    ⊢ (<??> M Ks) <: (<??.. Xs> M Xs).
+  Proof. Admitted.
+
   Lemma lty_le_swap_recv_send A1 A2 S :
     ⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
   Proof.
-- 
GitLab