diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index cfac3f33a8122ea8e8ed55e2131ecce0cf7a7c02..067baf5dccb8272f32d38adcced68d77af4db7cf 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -566,13 +566,20 @@ Section proto.
     (<?> m1) ⊑ (<!> m2).
   Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
 
-  Lemma iProto_le_end_inv p : p ⊑ END -∗ ◇ (p ≡ END).
+  Lemma iProto_le_end_inv_l p : p ⊑ END -∗ ◇ (p ≡ END).
   Proof.
     rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
     iDestruct "H" as (a1 a2 m1 m2) "(_ & >Heq & _)".
     by iDestruct (iProto_end_message_equivI with "Heq") as %[].
   Qed.
 
+  Lemma iProto_le_end_inv_r p : END ⊑ p -∗ ◇ (p ≡ END).
+  Proof.
+    rewrite iProto_le_unfold. iIntros "[[_ Hp]|H] //".
+    iDestruct "H" as (a1 a2 m1 m2) "(>Heq & _ & _)".
+    iDestruct (iProto_end_message_equivI with "Heq") as %[].
+  Qed.
+
   Lemma iProto_le_send_inv p1 m2 :
     p1 ⊑ (<!> m2) -∗ ∃ a1 m1,
       ◇ (p1 ≡ <a1> m1) ∗
@@ -658,7 +665,7 @@ Section proto.
   Proof.
     iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
     destruct (iProto_case p3) as [->|([]&m3&->)].
-    - iMod (iProto_le_end_inv with "H2") as "H2". by iRewrite "H2" in "H1".
+    - iMod (iProto_le_end_inv_l with "H2") as "H2". by iRewrite "H2" in "H1".
     - iDestruct (iProto_le_send_inv with "H2") as (a2 m2) "[>Hp2 H2]".
       iRewrite "Hp2" in "H1"; clear p2. destruct a2.
       + iDestruct (iProto_le_send_inv with "H1") as (a1 m1) "[>Hp1 H1]".
@@ -753,6 +760,28 @@ Section proto.
     - iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
       by iApply (iProto_le_recv_recv_inv with "H").
   Qed.
+
+  Lemma iProto_le_exist_elim_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p :
+    (∀ x, (<?> m x) ⊑ p) -∗
+    (<? x> m x) ⊑ p.
+  Proof.
+    rewrite iMsg_exist_eq. iIntros "H".
+    destruct (iProto_case p) as [Heq | [a [m' Heq]]].
+    - unshelve iSpecialize ("H" $!inhabitant); first by apply _.
+      rewrite Heq.
+      iMod (iProto_le_end_inv_l with "H") as "H".
+      rewrite iProto_end_eq iProto_message_eq.
+      iDestruct (proto_message_end_equivI with "H") as "[]".
+    - iEval (rewrite Heq). destruct a.
+      + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=".
+        iDestruct "Hm1" as (x) "Hm1".
+        iSpecialize ("H" $! x). rewrite Heq.
+        iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
+      + iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
+        iSpecialize ("H" $! x). rewrite Heq.
+        by iApply (iProto_le_recv_recv_inv with "H").
+  Qed.
+
   Lemma iProto_le_exist_elim_r {A} a m1 (m2 : A → iMsg Σ V) :
     (∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗
     (<a> m1) ⊑ (<! x> m2 x).
@@ -764,6 +793,26 @@ Section proto.
       iDestruct 1 as (x) "Hm2".
       iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
   Qed.
+  Lemma iProto_le_exist_elim_r_inhabited `{Hinh : Inhabited A} p (m : A → iMsg Σ V) :
+    (∀ x, p ⊑ (<!> m x)) -∗
+    p ⊑ (<! x> m x).
+  Proof.
+    rewrite iMsg_exist_eq. iIntros "H".
+    destruct (iProto_case p) as [Heq | [a [m' Heq]]].
+    - unshelve iSpecialize ("H" $!inhabitant); first by apply _.
+      rewrite Heq.
+      iMod (iProto_le_end_inv_r with "H") as "H".
+      rewrite iProto_end_eq iProto_message_eq.
+      iDestruct (proto_message_end_equivI with "H") as "[]".
+    - iEval (rewrite Heq). destruct a.
+      + iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
+        iSpecialize ("H" $! x). rewrite Heq.
+        by iApply (iProto_le_send_send_inv with "H").
+      + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1".
+        iDestruct 1 as (x) "Hm2".
+        iSpecialize ("H" $! x). rewrite Heq.
+        iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
+  Qed.
   Lemma iProto_le_exist_intro_l {A} (m : A → iMsg Σ V) a :
     ⊢ (<! x> m x) ⊑ (<!> m a).
   Proof.
@@ -810,7 +859,7 @@ Section proto.
   Proof.
     iIntros "H". iLöb as "IH" forall (p1 p2).
     destruct (iProto_case p1) as [->|([]&m1&->)].
-    - iMod (iProto_le_end_inv with "H") as "H".
+    - iMod (iProto_le_end_inv_l with "H") as "H".
       iRewrite "H". iApply iProto_le_refl.
     - iDestruct (iProto_le_send_inv with "H") as (a2 m2) "[>Hp2 H]".
       iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message).
@@ -853,7 +902,7 @@ Section proto.
   Proof.
     iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4).
     destruct (iProto_case p2) as [->|([]&m2&->)].
-    - iMod (iProto_le_end_inv with "H1") as "H1".
+    - iMod (iProto_le_end_inv_l with "H1") as "H1".
       iRewrite "H1". by rewrite !left_id.
     - iDestruct (iProto_le_send_inv with "H1") as (a1 m1) "[>Hp1 H1]".
       iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. destruct a1; simpl.
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index bf718e6f36e4861e2dc1f821d899a117b90f72ee..28980c4670309ee8d238c9a261588323b368e34b 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -85,14 +85,14 @@ Section double.
   Qed.
 
   Lemma prog_typed :
-    ⊢ ∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ lty_int * lty_int.
+    ⊢ ∅ ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
   Proof.
     iIntros (vs) "!> HΓ /=".
     iApply wp_value.
     iSplitL; last by iApply env_ltyped_empty.
     iIntros (c) "Hc".
     iApply (wp_prog with "[Hc]").
-    { iApply (iProto_mapsto_le _ (lsty_car (<??> lty_int; <??> lty_int; END)) with "Hc").
+    { iApply (iProto_mapsto_le _ (lsty_car (<??> TY lty_int; <??> TY lty_int; END)) with "Hc").
       iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists x1.
       iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists x2. auto. }
     iIntros "!>" (k1 k2 _).
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 78081802e41d7a156316f34cf93bc4f5a4787a5a..77074ab3da3e301548da9ff8b1199d37d6ca6c44 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -7,7 +7,7 @@ Section pair.
   Context `{heapG Σ, chanG Σ}.
 
   Lemma prog_typed :
-    ⊢ ∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ lty_int * lty_int.
+    ⊢ ∅ ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
   Proof.
     rewrite /prog.
     iApply ltyped_lam. iApply ltyped_pair.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 9ba6d36d20812d2df09131ab41c3879c295deb58..8289817c72d32b6d31fffbfd4967886e2e11b04d 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -2,10 +2,20 @@ From iris.algebra Require Export gmap.
 From actris.logrel Require Export model.
 From actris.channel Require Export channel.
 
+Definition lmsg Σ := iMsg Σ.
+Delimit Scope lmsg_scope with lmsg.
+Bind Scope lmsg_scope with lmsg.
+
+Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
+  (∃ v, M v)%msg.
+
+Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
+  (∃ v, MSG v {{ ▷ ltty_car A v}} ; (lsty_car S))%msg.
+
 Definition lty_end {Σ} : lsty Σ := Lsty END.
 
-Definition lty_message {Σ} (a : action) (A : ltty Σ) (S : lsty Σ) : lsty Σ :=
-  Lsty (<a@v> MSG v {{ â–· ltty_car A v }}; lsty_car S).
+Definition lty_message {Σ} (a : action) (M : lmsg Σ) : lsty Σ :=
+  Lsty (<a> M).
 
 Definition lty_choice {Σ} (a : action) (Ss : gmap Z (lsty Σ)) : lsty Σ :=
   Lsty (<a@(x : Z)> MSG #x {{ ⌜is_Some (Ss !! x)⌝ }}; lsty_car (Ss !!! x)).
@@ -20,11 +30,25 @@ Instance: Params (@lty_choice) 2 := {}.
 Instance: Params (@lty_dual) 1 := {}.
 Instance: Params (@lty_app) 1 := {}.
 
+Notation "'TY' A ; S" := (lty_msg_base A S)
+  (at level 200, right associativity,
+   format "'TY'  A  ;  S") : lmsg_scope.
+Notation "∃ x .. y , m" :=
+  (lty_msg_exist (λ x, .. (lty_msg_exist (λ y, m)) ..)%lmsg) : lmsg_scope.
+
 Notation "'END'" := lty_end : lty_scope.
-Notation "<!!> A ; S" :=
-  (lty_message Send A S) (at level 20, A, S at level 200) : lty_scope.
-Notation "<??> A ; S" :=
-  (lty_message Recv A S) (at level 20, A, S at level 200) : lty_scope.
+Notation "<!!> M" :=
+  (lty_message Send M) (at level 200, M at level 200) : lty_scope.
+Notation "<!! x1 .. xn > M" :=
+  (lty_message Send (∃ x1, .. (∃ xn, M) ..))
+    (at level 200, x1 closed binder, xn closed binder, M at level 200,
+     format "<!!  x1  ..  xn >  M") : lty_scope.
+Notation "<??> M" :=
+  (lty_message Recv M) (at level 200, M at level 200) : lty_scope.
+Notation "<?? x1 .. xn > M" :=
+  (lty_message Recv (∃ x1, .. (∃ xn, M) ..))
+    (at level 200, x1 closed binder, xn closed binder, M at level 200,
+     format "<??  x1  ..  xn >  M") : lty_scope.
 Notation lty_select := (lty_choice Send).
 Notation lty_branch := (lty_choice Recv).
 Infix "<++>" := lty_app (at level 60) : lty_scope.
@@ -34,15 +58,27 @@ Notation "(.<++> T )" := (λ S, lty_app S T) (only parsing) : lty_scope.
 Section session_types.
   Context {Σ : gFunctors}.
 
-  Global Instance lty_message_ne a : NonExpansive2 (@lty_message Σ a).
+  Global Instance lty_msg_exist_ne k :
+    Proper (pointwise_relation _ (dist n) ==> (dist n)) (@lty_msg_exist Σ k).
   Proof. solve_proper. Qed.
-  Global Instance lty_message_proper a :
-    Proper ((≡) ==> (≡) ==> (≡)) (@lty_message Σ a).
-  Proof. apply ne_proper_2, _. Qed.
-  Global Instance lty_message_contractive n a :
-    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_message Σ a).
+  Global Instance lty_msg_exist_proper k :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (@lty_msg_exist Σ k).
+  Proof. solve_proper. Qed.
+  Global Instance lty_msg_base_ne : NonExpansive2 (@lty_msg_base Σ).
+  Proof. rewrite /lty_msg_base. solve_proper. Qed.
+  Global Instance lty_msg_base_proper :
+    Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ).
+  Proof. rewrite /lty_msg_base. apply ne_proper_2, _. Qed.
+  Global Instance lty_msg_base_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_msg_base Σ).
   Proof. solve_contractive. Qed.
 
+  Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
+  Proof. solve_proper. Qed.
+  Global Instance lty_message_proper a :
+    Proper ((≡) ==> (≡)) (@lty_message Σ a).
+  Proof. apply ne_proper, _. Qed.
+
   Global Instance lty_choice_ne a : NonExpansive (@lty_choice Σ a).
   Proof. solve_proper. Qed.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 1a7342aa8862f2c60ad7512e21f50438c149047c..ce565880e20606566acbac0de84336670c98a32a 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -248,7 +248,7 @@ Section subtyping_rules.
   (** Session subtyping *)
   Lemma lty_le_send A1 A2 S1 S2 :
     ▷ (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
-    (<!!> A1 ; S1) <: (<!!> A2 ; S2).
+    (<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
   Proof.
     iIntros "#HAle #HSle !>" (v) "H". iExists v. 
     iDestruct ("HAle" with "H") as "$". by iModIntro.
@@ -256,14 +256,32 @@ Section subtyping_rules.
 
   Lemma lty_le_recv A1 A2 S1 S2 :
     ▷ (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
-    (<??> A1 ; S1) <: (<??> A2 ; S2).
+    (<??> TY A1 ; S1) <: (<??> TY A2 ; S2).
   Proof.
     iIntros "#HAle #HSle !>" (v) "H". iExists v.
     iDestruct ("HAle" with "H") as "$". by iModIntro.
   Qed.
 
+  Lemma lty_le_exist_elim_l k (M : lty Σ k → lmsg Σ) S :
+    (∀ (A : lty Σ k), (<??> M A) <: S) -∗
+    ((<?? (A : lty Σ k)> M A) <: S).
+  Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto. Qed.
+
+  Lemma lty_le_exist_elim_r k (M : lty Σ k → lmsg Σ) S :
+    (∀ (A : lty Σ k), S <: (<!!> M A)) -∗
+    (S <: (<!! (A : lty Σ k)> M A)).
+  Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto. Qed.
+
+  Lemma lty_le_exist_intro_l k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
+    ⊢ (<! X> M X) ⊑ (<!> M A).
+  Proof. by iApply (iProto_le_exist_intro_l). Qed.
+
+  Lemma lty_le_exist_intro_r k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
+    ⊢ (<?> M A) ⊑ (<? X> M X).
+  Proof. by iApply (iProto_le_exist_intro_r). Qed.
+
   Lemma lty_le_swap_recv_send A1 A2 S :
-    ⊢ (<??> A1; <!!> A2; S) <: (<!!> A2; <??> A1; S).
+    ⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
   Proof.
     iIntros "!>" (v1 v2).
     iApply iProto_le_trans;
@@ -274,7 +292,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_swap_recv_select A Ss :
-    ⊢ (<??> A; lty_select Ss) <: lty_select ((λ S, <??> A; S) <$> Ss)%lty.
+    ⊢ (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
   Proof.
     iIntros "!>" (v1 x2).
     iApply iProto_le_trans;
@@ -286,7 +304,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_swap_branch_send A Ss :
-    ⊢ lty_branch ((λ S, <!!> A; S) <$> Ss)%lty <: (<!!> A; lty_branch Ss).
+    ⊢ lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
   Proof.
     iIntros "!>" (x1 v2).
     iApply iProto_le_trans;
@@ -353,12 +371,12 @@ Section subtyping_rules.
     ⊢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
   Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
 
-  Lemma lty_le_app_send A S1 S2 : ⊢ (<!!> A; S1) <++> S2 <:> (<!!> A; S1 <++> S2).
+  Lemma lty_le_app_send 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.
-  Lemma lty_le_app_recv A S1 S2 : ⊢ (<??> A; S1) <++> S2 <:> (<??> A; S1 <++> S2).
+  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 "!> /=".
@@ -391,14 +409,14 @@ 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 A S) <:> lty_message (action_dual a) 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 A S : ⊢ lty_dual (<!!> A; S) <:> (<??> A; lty_dual S).
+  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 (<??> A; S) <:> (<!!> A; lty_dual S).
+  Lemma lty_le_dual_recv A S : ⊢ lty_dual (<??> TY A; S) <:> (<!!> TY A; lty_dual S).
   Proof. apply lty_le_dual_message. Qed.
 
   Lemma lty_le_dual_choice a (Ss : gmap Z (lsty Σ)) :
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 1506efea987be3ea636f45f93fc621d98a33f698..fb4b2ce41287d5882c22ebb2ae1f38e097b4f6ed 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -460,7 +460,7 @@ Section properties.
 
     Definition chansend : val := λ: "chan" "val", send "chan" "val";; "chan".
     Lemma ltyped_chansend A S :
-      ⊢ ∅ ⊨ chansend : chan (<!!> A; S) → A ⊸ chan S.
+      ⊢ ∅ ⊨ chansend : chan (<!!> TY A; S) → A ⊸ chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iSplitL; last by iApply env_ltyped_empty.
@@ -470,7 +470,7 @@ Section properties.
     Qed.
 
     Lemma ltyped_send Γ Γ' (x : string) e A S :
-      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> A; S))%lty]> Γ') -∗
+      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> TY A; S))%lty]> Γ') -∗
       Γ ⊨ send x e : () ⫤ <[x:=(chan S)%lty]> Γ'.
     Proof.
       iIntros "#He !>" (vs) "HΓ"=> /=.
@@ -488,7 +488,7 @@ Section properties.
 
     Definition chanrecv : val := λ: "chan", (recv "chan", "chan").
     Lemma ltyped_chanrecv A S :
-      ⊢ ∅ ⊨ chanrecv : chan (<??> A; S) → A * chan S.
+      ⊢ ∅ ⊨ chanrecv : chan (<??> TY A; S) → A * chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iSplitL; last by iApply env_ltyped_empty.
@@ -498,7 +498,7 @@ Section properties.
     Qed.
 
     Lemma ltyped_recv Γ (x : string) A S :
-      ⊢ <[x := (chan (<??> A; S))%lty]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
+      ⊢ <[x := (chan (<??> TY A; S))%lty]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
     Proof.
       iIntros "!>" (vs) "HΓ"=> /=.
       iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".