diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 2670d8bf7788fc229a4e8913b1d4d045dacd41b2..3db6d0e36d8e8bdb5285b1a8d758b6cbd6f31e23 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -466,6 +466,14 @@ Section proto.
     - iDestruct 1 as (x ->) "[Hpc Hps]". auto 10.
   Qed.
 
+  Lemma iProto_app_message_tele {TT} a (pc : TT -t> V * iProp Σ * iProto Σ V) p2 :
+    (iProto_message a (tele_app pc) <++> p2)%proto
+    ≡ iProto_message a (tele_app (tele_map (prod_map id (flip iProto_app p2)) pc)).
+  Proof.
+    rewrite iProto_app_message.
+    apply iProto_message_proper; apply tforall_forall=> x; by rewrite /=?tele_map_app.
+  Qed.
+
   Global Instance iProto_app_end_l : LeftId (≡) END%proto (@iProto_app Σ V).
   Proof. intros p. by rewrite iProto_end_eq /iProto_end_def iProto_app_end'. Qed.
   Global Instance iProto_app_end_r : RightId (≡) END%proto (@iProto_app Σ V).
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 4e33d931118b7f6e646fd7aa1cec55fcb3c1e994..74ebb05336d961805482df3d1112ca97d79f3229 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -298,6 +298,77 @@ Section subtype.
     ⊢ (S1 <++> S2) <++> S3 <s:> S1 <++> (S2 <++> S3).
   Proof. rewrite assoc. iApply lsty_bi_le_refl. Qed.
 
+  Lemma lsty_le_app_send A S1 S2 : ⊢ (<!!> A; S1) <++> S2 <s:> (<!!> A; S1 <++> S2).
+  Proof.
+    rewrite /lsty_app iProto_app_message_tele.
+    iSplit; iIntros "!>"; iApply iProto_le_refl.
+  Qed.
+
+  Lemma lsty_le_app_recv A S1 S2 : ⊢ (<??> A; S1) <++> S2 <s:> (<??> A; S1 <++> S2).
+  Proof.
+    rewrite /lsty_app iProto_app_message_tele.
+    iSplit; iIntros "!>"; iApply iProto_le_refl.
+  Qed.
+
+  Lemma lsty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
+    ⊢ lsty_choice a Ss <++> S2 <s:>
+      lsty_choice a ((λ S1, S1 <++> S2)%lsty <$> Ss).
+  Proof.
+    destruct a.
+    - rewrite /lsty_app iProto_app_message_tele.
+      iSplit; iIntros "!>".
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_send.
+        iIntros "!>" (x) "%". iExists _ => /=.
+        iSplit; first done.
+        iSplit.
+        * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
+        * destruct a as [S HSs]=> /=.
+          rewrite lookup_total_alt lookup_total_alt HSs /=.
+          rewrite lookup_fmap in HSs.
+          apply fmap_Some_1 in HSs as [S' [-> ->]].
+          iApply iProto_le_refl.
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_send.
+        iIntros "!>" (x) "%".
+        iExists _.
+        iSplit; first done. iSplit.
+        * by rewrite lookup_fmap fmap_is_Some.
+        * destruct a as [S HSs]=> /=.
+          rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
+          iApply iProto_le_refl.
+    - rewrite /lsty_app iProto_app_message_tele.
+      iSplit; iIntros "!>".
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_recv.
+        iIntros "!>" (x) "%". iExists _ => /=.
+        iSplit; first done.
+        iSplit.
+        * by rewrite lookup_fmap fmap_is_Some.
+        * destruct a as [S HSs]=> /=.
+          rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
+          iApply iProto_le_refl.
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_recv.
+        iIntros "!>" (x) "%".
+        iExists _.
+        iSplit; first done. iSplit.
+        * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
+        * destruct a as [S HSs]=> /=.
+          rewrite lookup_total_alt lookup_total_alt HSs /=.
+          rewrite lookup_fmap in HSs.
+          apply fmap_Some_1 in HSs as [S' [-> ->]].
+          iApply iProto_le_refl.
+  Qed.
+
+  Lemma lsty_le_app_select A Ss S2 :
+    ⊢ (lsty_select Ss) <++> S2 <s:> (lsty_select ((λ S1, S1 <++> S2)%lsty <$> Ss)).
+  Proof. apply lsty_le_app_choice. Qed.
+
+  Lemma lsty_le_app_branch A Ss S2 :
+    ⊢ (lsty_branch Ss) <++> S2 <s:> (lsty_branch ((λ S1, S1 <++> S2)%lsty <$> Ss)).
+  Proof. apply lsty_le_app_choice. Qed.
+
   Lemma lsty_le_app_id_l S : ⊢ (END <++> S) <s:> S.
   Proof. rewrite left_id. iApply lsty_bi_le_refl. Qed.
   Lemma lsty_le_app_id_r S : ⊢ (S <++> END) <s:> S.
@@ -323,21 +394,23 @@ Section subtype.
   Proof. apply lsty_le_dual_message. Qed.
 
   Lemma lsty_le_dual_choice a (Ss : gmap Z (lsty Σ)) :
-    ⊢ lsty_dual (lsty_choice a Ss) <s:> lsty_choice (action_dual a) (lsty_dual <$> Ss).
+    ⊢ lsty_dual (lsty_choice a Ss) <s:>
+      lsty_choice (action_dual a) (lsty_dual <$> Ss).
   Proof.
-    iSplit.
-    - iIntros "!>".
-      rewrite /lsty_dual iProto_dual_message_tele /lsty_choice /=.
-      destruct a.
-      + iApply iProto_le_recv.
-        iIntros "!>" (x) "%".
-        iExists _.
-        iSplit; first done. iSplit.
+    destruct a.
+    - rewrite /lsty_dual iProto_dual_message_tele.
+      iSplit; iIntros "!>".
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_recv.
+        iIntros "!>" (x) "%". iExists _ => /=.
+        iSplit; first done.
+        iSplit.
         * by rewrite lookup_fmap fmap_is_Some.
         * destruct a as [S HSs]=> /=.
           rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
           iApply iProto_le_refl.
-      + iApply iProto_le_send.
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_recv.
         iIntros "!>" (x) "%".
         iExists _.
         iSplit; first done. iSplit.
@@ -347,25 +420,28 @@ Section subtype.
           rewrite lookup_fmap in HSs.
           apply fmap_Some_1 in HSs as [S' [-> ->]].
           iApply iProto_le_refl.
-        - iIntros "!>".
-          rewrite /lsty_dual iProto_dual_message_tele /lsty_choice /=.
-          destruct a.
-          + iApply iProto_le_recv.
-            iIntros "!>" (x) "%". iExists _.
-            iSplit; first done. iSplit.
-            * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
-            * destruct a as [S HSs]=> /=.
-              rewrite lookup_total_alt lookup_total_alt HSs /=.
-              rewrite lookup_fmap in HSs.
-              apply fmap_Some_1 in HSs as [S' [-> ->]].
-              iApply iProto_le_refl.
-          + iApply iProto_le_send.
-            iIntros "!>" (x) "%". iExists _.
-            iSplit; first done. iSplit.
-            * by rewrite lookup_fmap fmap_is_Some.
-            * destruct a as [S HSs]=> /=.
-              rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
-              iApply iProto_le_refl.
+    - rewrite /lsty_dual iProto_dual_message_tele.
+      iSplit; iIntros "!>".
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_send.
+        iIntros "!>" (x) "%". iExists _ => /=.
+        iSplit; first done.
+        iSplit.
+      * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
+      * destruct a as [S HSs]=> /=.
+        rewrite lookup_total_alt lookup_total_alt HSs /=.
+        rewrite lookup_fmap in HSs.
+        apply fmap_Some_1 in HSs as [S' [-> ->]].
+        iApply iProto_le_refl.
+      + rewrite /lsty_select /lsty_choice.
+        iApply iProto_le_send.
+        iIntros "!>" (x) "%".
+        iExists _.
+        iSplit; first done. iSplit.
+        * by rewrite lookup_fmap fmap_is_Some.
+        * destruct a as [S HSs]=> /=.
+          rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
+          iApply iProto_le_refl.
   Qed.
 
   Lemma lsty_le_dual_select (Ss : gmap Z (lsty Σ)) :