diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 33246ebb45fc17a4b0a8ae5ad6867a7a07b48ddb..5ea8484fd1300e204f85ba715d324c0c19f5f501 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -124,6 +124,8 @@ Section session_types.
   Proof. solve_proper. Qed.
   Global Instance lty_dual_proper : Proper ((≡) ==> (≡)) (@lty_dual Σ).
   Proof. apply ne_proper, _. Qed.
+  Global Instance lty_dual_involutive : Involutive (≡) (@lty_dual Σ).
+  Proof. intros S. rewrite /lty_dual. apply iProto_dual_involutive. Qed.
 
   Global Instance lty_app_ne : NonExpansive2 (@lty_app Σ).
   Proof. solve_proper. Qed.
@@ -138,4 +140,28 @@ Section session_types.
     (∀ x, LtyMsgTele (kt:=kt x) (M x) (A x) (S x)) →
     LtyMsgTele (kt:=KTeleS kt) (∃ x, M x) A S.
   Proof. intros HM. rewrite /LtyMsgTele /=. f_equiv=> x. apply HM. Qed.
+
+  Global Instance lty_app_end_l : LeftId (≡) END%lty (@lty_app Σ).
+  Proof. intros S1. rewrite /lty_app. apply iProto_app_end_l. Qed.
+
+  Global Instance lty_app_end_r : RightId (≡) END%lty (@lty_app Σ).
+  Proof. intros S1. rewrite /lty_app. apply iProto_app_end_r. Qed.
+
+  Global Instance lty_app_assoc : Assoc (≡) (@lty_app Σ).
+  Proof. intros S1 S2 S3. rewrite /lty_app. apply iProto_app_assoc. Qed.
+
+  Lemma lty_app_send (A : ltty Σ) S1 S2 :
+    ((<!!> TY A; S1) <++> S2)%lty ≡ ((<!!> TY A; S1 <++> S2))%lty.
+  Proof.
+    rewrite /lty_message /lty_msg_base !/lty_app iProto_app_message iMsg_app_exist.
+    do 4 f_equiv. by rewrite iMsg_app_base.
+  Qed.
+
+  Lemma lty_app_recv (A : ltty Σ) S1 S2 :
+    ((<??> TY A; S1) <++> S2)%lty ≡ ((<??> TY A; S1 <++> S2))%lty.
+  Proof.
+    rewrite /lty_message /lty_msg_base !/lty_app iProto_app_message iMsg_app_exist.
+    do 4 f_equiv. by rewrite iMsg_app_base.
+  Qed.
+
 End session_types.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index de8bcee048080e3e4c19f9c213b33f1d2f3c049b..6f3c9396a179b0294eb1a13192f2b32688b28dd3 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -412,6 +412,46 @@ Section subtyping_rules.
     iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
   Qed.
 
+  (** The instances below make it possible to use the tactics [iIntros],
+  [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [lty_le] goals.
+  These instances have higher precedence than the ones in [proto.v] to avoid
+  needless unfolding of the subtyping relation. *)
+  Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) name :
+    AsIdentName M name →
+    FromForall (lty_message Recv (lty_msg_exist M) <: S) (λ X, (<??> M X) <: S)%I name | 0.
+  Proof. intros _. apply lty_le_exist_elim_l. Qed.
+  Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) name :
+    AsIdentName M name →
+    FromForall (S <: lty_message Send (lty_msg_exist M)) (λ X, S <: (<!!> M X))%I name | 1.
+  Proof. intros _. apply lty_le_exist_elim_r. Qed.
+
+  Global Instance lty_le_from_exist_l k (M : lty Σ k → lmsg Σ) S :
+    FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 0.
+  Proof.
+    rewrite /FromExist. iDestruct 1 as (x) "H".
+    iApply (lty_le_trans with "[] H"). iApply lty_le_exist_intro_l.
+  Qed.
+  Global Instance lty_le_from_exist_r k (M : lty Σ k → lmsg Σ) S :
+    FromExist (S <: <?? X> M X) (λ X, S <: (<??> M X))%I | 1.
+  Proof.
+    rewrite /FromExist. iDestruct 1 as (x) "H".
+    iApply (lty_le_trans with "H"). iApply lty_le_exist_intro_r.
+  Qed.
+
+  Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
+    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+              ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2) | 0.
+  Proof.
+    rewrite /FromModal. iIntros "H". iApply lty_le_send. iApply lty_le_refl. done.
+  Qed.
+
+  Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
+    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+              ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2) | 0.
+  Proof.
+    rewrite /FromModal. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. done.
+  Qed.
+
   (** Algebraic laws *)
   Lemma lty_le_app S11 S12 S21 S22 :
     (S11 <: S21) -∗ (S12 <: S22) -∗
@@ -419,25 +459,52 @@ Section subtyping_rules.
   Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
   Lemma lty_le_app_id_l S : ⊢ (END <++> S) <:> S.
-  Proof. rewrite /lty_app left_id. iSplit; by iModIntro. Qed.
+  Proof. rewrite left_id. iSplit; by iModIntro. Qed.
   Lemma lty_le_app_id_r S : ⊢ (S <++> END) <:> S.
-  Proof. rewrite /lty_app right_id. iSplit; by iModIntro. Qed.
+  Proof. rewrite right_id. iSplit; by iModIntro. Qed.
   Lemma lty_le_app_assoc S1 S2 S3 :
     ⊢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
-  Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
+  Proof. rewrite assoc. iSplit; by iModIntro. Qed.
+
+  Lemma lty_le_app_send_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) S2 :
+    LtyMsgTele M A S →
+    ⊢ (<!!> M) <++> S2 <:>
+        <!!.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
+  Proof.
+    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /lty_app /lty_message iProto_app_message /=.
+    induction kt as [|k kt IH]; rewrite iMsg_app_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
+  Qed.
 
   Lemma lty_le_app_send A S1 S2 :
     ⊢ (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
+  Proof. rewrite lty_app_send. iSplit; iApply lty_le_refl. Qed.
+
+  Lemma lty_le_app_recv_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) S2 :
+    LtyMsgTele M A S →
+    ⊢ (<??> M) <++> S2 <:>
+        <??.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
   Proof.
-    rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
-    iSplit; by iIntros "!> /=".
+    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /lty_app /lty_message iProto_app_message /=.
+    induction kt as [|k kt IH]; rewrite iMsg_app_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
   Qed.
+
   Lemma lty_le_app_recv A S1 S2 :
     ⊢ (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
-  Proof.
-    rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
-    iSplit; by iIntros "!> /=".
-  Qed.
+  Proof. rewrite lty_app_recv. iSplit; iApply lty_le_refl. Qed.
 
   Lemma lty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
     ⊢ lty_choice a Ss <++> S2 <:> lty_choice a ((.<++> S2) <$> Ss)%lty.
@@ -466,11 +533,45 @@ Section subtyping_rules.
   Proof. rewrite /lty_dual iProto_dual_end=> /=. apply lty_bi_le_refl. Qed.
 
   Lemma lty_le_dual_message a A S :
-    ⊢ lty_dual (lty_message a (TY A; S)) <:> lty_message (action_dual a) (TY A; (lty_dual S)).
+    ⊢ lty_dual (lty_message a (TY A; S)) <:>
+      lty_message (action_dual a) (TY A; (lty_dual S)).
   Proof.
     rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
     setoid_rewrite iMsg_dual_base. iSplit; by iIntros "!> /=".
   Qed.
+
+  Lemma lty_le_dual_send_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :
+    LtyMsgTele M A S →
+    ⊢ lty_dual (<!!> M) <:>
+        <??.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
+  Proof.
+    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /lty_dual /lty_message iProto_dual_message /=.
+    induction kt as [|k kt IH]; rewrite iMsg_dual_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
+  Qed.
+
+  Lemma lty_le_dual_recv_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :
+    LtyMsgTele M A S →
+    ⊢ lty_dual (<??> M) <:>
+      <!!.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
+  Proof.
+    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /lty_dual /lty_message iProto_dual_message /=.
+    induction kt as [|k kt IH]; rewrite iMsg_dual_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
+  Qed.
+
   Lemma lty_le_dual_send A S : ⊢ lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
   Proof. apply lty_le_dual_message. Qed.
   Lemma lty_le_dual_recv A S : ⊢ lty_dual (<??> TY A; S) <:> (<!!> TY A; lty_dual S).
@@ -493,45 +594,6 @@ Section subtyping_rules.
     ⊢ lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
   Proof. iApply lty_le_dual_choice. Qed.
 
-  (** The instances below make it possible to use the tactics [iIntros],
-  [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [lty_le] goals.
-  These instances have higher precedence than the ones in [proto.v] to avoid
-  needless unfolding of the subtyping relation. *)
-  Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) name :
-    AsIdentName M name →
-    FromForall (lty_message Recv (lty_msg_exist M) <: S) (λ X, (<??> M X) <: S)%I name | 0.
-  Proof. intros _. apply lty_le_exist_elim_l. Qed.
-  Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) name :
-    AsIdentName M name →
-    FromForall (S <: lty_message Send (lty_msg_exist M)) (λ X, S <: (<!!> M X))%I name | 1.
-  Proof. intros _. apply lty_le_exist_elim_r. Qed.
-
-  Global Instance lty_le_from_exist_l k (M : lty Σ k → lmsg Σ) S :
-    FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 0.
-  Proof.
-    rewrite /FromExist. iDestruct 1 as (x) "H".
-    iApply (lty_le_trans with "[] H"). iApply lty_le_exist_intro_l.
-  Qed.
-  Global Instance lty_le_from_exist_r k (M : lty Σ k → lmsg Σ) S :
-    FromExist (S <: <?? X> M X) (λ X, S <: (<??> M X))%I | 1.
-  Proof.
-    rewrite /FromExist. iDestruct 1 as (x) "H".
-    iApply (lty_le_trans with "H"). iApply lty_le_exist_intro_r.
-  Qed.
-
-  Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
-    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
-              ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2) | 0.
-  Proof.
-    rewrite /FromModal. iIntros "H". iApply lty_le_send. iApply lty_le_refl. done.
-  Qed.
-
-  Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
-    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
-              ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2) | 0.
-  Proof.
-    rewrite /FromModal. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. done.
-  Qed.
 End subtyping_rules.
 
 Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>