diff --git a/_CoqProject b/_CoqProject
index 94f4bdfb3d129f8bd0ce7e901b91327db7811c72..b327506ff794ed37d0ef8a951cd080e373e93cd6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -32,4 +32,5 @@ theories/logrel/lib/mutex.v
 theories/logrel/examples/double.v
 theories/logrel/examples/pair.v
 theories/logrel/examples/rec_subtyping.v
+theories/logrel/examples/choice_subtyping.v
 
diff --git a/theories/logrel/examples/choice_subtyping.v b/theories/logrel/examples/choice_subtyping.v
new file mode 100644
index 0000000000000000000000000000000000000000..0fae3e166c717f8118fd252a0355a93e21803577
--- /dev/null
+++ b/theories/logrel/examples/choice_subtyping.v
@@ -0,0 +1,236 @@
+From actris.channel Require Import proofmode proto channel.
+From actris.logrel Require Import subtyping_rules.
+From iris.proofmode Require Import tactics.
+
+Section choice_example.
+  Context `{heapG Σ, chanG Σ}.
+
+  Variables R M P Q S U : ltty Σ.
+
+  (**
+  ?R. ((!M._) <+> (!P._) <+> (!Q._))
+  <&>
+  ?S. ((!M._) <+> (!P._))
+   *)
+  Definition prot_sub : lsty Σ :=
+    (lty_branch
+       (<[1%Z:= <??> TY R ;
+         lty_select
+           (<[1%Z:= <!!> TY M ; END]>
+            (<[2%Z:= <!!> TY P ; END]>
+             (<[3%Z:= <!!> TY Q ; END]>∅)))]>
+        (<[2%Z:= <??> TY S ;
+          lty_select
+            (<[1%Z := <!!> TY M ; END]>
+             (<[2%Z := <!!> TY P; END]>∅))]>∅)))%lty.
+
+
+  (**
+  !M.((?R._) <&> (?S._) <&> (?U._))
+  <+>
+  !P.((?R._) <&> (?S._))
+   *)
+  Definition prot_sup : lsty Σ :=
+    (lty_select
+       (<[1%Z:= <!!> TY M ; lty_branch
+                              (<[1%Z:= <??> TY R ; END]>
+                               (<[2%Z:= <??> TY S ; END]>
+                               (<[3%Z:= <??> TY U ; END]>∅)))]>
+        (<[2%Z:= <!!> TY P ; lty_branch
+                               (<[1%Z := <??> TY R ; END]>
+                                (<[2%Z := <??> TY S; END]>∅))]>∅)))%lty.
+
+  (**
+  Weaken select
+  ?R.((!M._) <+> (!P._))
+  <&>
+  ?S.((!M._) <+> (!P._))
+  *)
+  Definition prot1 : lsty Σ :=
+    (lty_branch
+       (<[1%Z:= <??> TY R ;
+         lty_select
+           (<[1%Z:= <!!> TY M ; END]>
+            (<[2%Z:= <!!> TY P ; END]>∅))]>
+        (<[2%Z:= <??> TY S ;
+          lty_select
+            (<[1%Z := <!!> TY M ; END]>
+             (<[2%Z := <!!> TY P; END]>∅))]>∅)))%lty.
+
+  (**
+  Swap recv/select
+  ((?R.!M._) <+> (?R.!P._))
+  <&>
+  ((?S.!M._) <+> (?S.!P._))
+  *)
+  Definition prot2 : lsty Σ :=
+    (lty_branch
+       (<[1%Z:= lty_select
+                  (<[1%Z:= <??> TY R ; <!!> TY M ; END]>
+                   (<[2%Z:= <??> TY R ; <!!> TY P ; END]>∅))]>
+        (<[2%Z:= lty_select
+                   (<[1%Z := <??> TY S ; <!!> TY M ; END]>
+                    (<[2%Z := <??> TY S ; <!!> TY P; END]>∅))]>∅)))%lty.
+
+  (**
+  swap branch/select
+  ((?R.!M._) <&> (?S.!M._))
+  <+>
+  ((?R.!P._) <&> (?S.!P._))
+  *)
+  Definition prot3 : lsty Σ :=
+    (lty_select
+       (<[1%Z:= lty_branch
+                  (<[1%Z:= <??> TY R ; <!!> TY M ; END]>
+                   (<[2%Z:= <??> TY S ; <!!> TY M ; END]>∅))]>
+        (<[2%Z:= lty_branch
+                   (<[1%Z := <??> TY R ; <!!> TY P ; END]>
+                    (<[2%Z := <??> TY S ; <!!> TY P; END]>∅))]>∅)))%lty.
+
+  (**
+  swap recv/send
+  ((!M.?R._) <&> (!M.?S._))
+  <+>
+  ((!P.?R._) <&> (!P.?S._))
+  *)
+  Definition prot4 : lsty Σ :=
+    (lty_select
+       (<[1%Z:= lty_branch
+                  (<[1%Z:= <!!> TY M ; <??> TY R ; END]>
+                   (<[2%Z:= <!!> TY M ; <??> TY S ; END]>∅))]>
+        (<[2%Z:= lty_branch
+                   (<[1%Z := <!!> TY P ; <??> TY R ; END]>
+                    (<[2%Z := <!!> TY P; <??> TY S ; END]>∅))]>∅)))%lty.
+
+  (**
+  Swap branch/send
+  !M.((?R._) <&> (?S._))
+  <+>
+  !P.((?R._) <&> (?S._))
+  *)
+  Definition prot5 : lsty Σ :=
+    (lty_select
+       (<[1%Z:= <!!> TY M ;
+         lty_branch (<[1%Z:= <??> TY R ; END]>
+                     (<[2%Z:= <??> TY S ; END]>∅))]>
+        (<[2%Z:= <!!> TY P ;
+          lty_branch
+            (<[1%Z := <??> TY R ; END]>
+             (<[2%Z := <??> TY S ; END]>∅))]>∅)))%lty.
+
+  Lemma subtype_proof :
+    ⊢ prot_sub <: prot_sup.
+  Proof.
+    (** Weakening of select *)
+    iApply (lty_le_trans _ prot1).
+    {
+      iApply lty_le_branch. iIntros "!>".
+      rewrite big_sepM2_insert=> //.
+      iSplit.
+      - iApply lty_le_recv; [iApply lty_le_refl | ].
+        iApply lty_le_select_subseteq.
+        rewrite (insert_commute _ 2%Z 3%Z) //.
+        rewrite (insert_commute _ 1%Z 3%Z) //.
+        by apply insert_subseteq.
+      - rewrite big_sepM2_insert //. eauto.
+    }
+    (** Swap recv/select *)
+    iApply (lty_le_trans _ prot2).
+    {
+      iApply lty_le_branch. iIntros "!>".
+      rewrite big_sepM2_insert=> //.
+      iSplit.
+      - iApply lty_le_swap_recv_select.
+      - rewrite big_sepM2_insert=> //. iSplit=> //.
+        iApply lty_le_swap_recv_select.
+    }
+    (** Swap branch/select *)
+    iApply (lty_le_trans _ prot3).
+    {
+      iApply (lty_le_swap_branch_select
+                (<[1%Z:=
+                     <[1%Z:=(<??> TY R; <!!> TY M; END)%lty]>
+                     (<[2%Z:= (<??> TY R; <!!> TY P; END)%lty]>∅)]>
+                 (<[2%Z:=
+                     <[1%Z:=(<??> TY S; <!!> TY M; END)%lty]>
+                     (<[2%Z:= (<??> TY S; <!!> TY P; END)%lty]>∅)]>∅))
+                (<[1%Z:=
+                     <[1%Z:=(<??> TY R; <!!> TY M; END)%lty]>
+                     (<[2%Z:= (<??> TY S; <!!> TY M; END)%lty]>∅)]>
+                 (<[2%Z:=
+                     <[1%Z:=(<??> TY R; <!!> TY P; END)%lty]>
+                     (<[2%Z:= (<??> TY S; <!!> TY P; END)%lty]>∅)]>∅))
+             ).
+      intros i j Ss1' Ss2' Hin1 Hin2.
+      assert (i = 1%Z ∨ i = 2%Z).
+      {
+        destruct (decide (i = 1)). eauto.
+        destruct (decide (i = 2)). eauto.
+        rewrite lookup_insert_ne in Hin1=> //.
+        rewrite lookup_insert_ne in Hin1=> //.
+      }
+      assert (j = 1%Z ∨ j = 2%Z).
+      {
+        destruct (decide (j = 1)). eauto.
+        destruct (decide (j = 2)). eauto.
+        rewrite lookup_insert_ne in Hin2=> //.
+        rewrite lookup_insert_ne in Hin2=> //.
+      }
+      destruct H2 as [-> | ->] ,H1 as [-> | ->].
+      - rewrite lookup_insert in Hin1.
+        rewrite lookup_insert in Hin2.
+        inversion Hin1; inversion Hin2; eauto.
+      - rewrite (insert_commute _ 1%Z 2%Z) in Hin1=> //.
+        rewrite lookup_insert in Hin1.
+        rewrite lookup_insert in Hin2.
+        inversion Hin1; inversion Hin2; eauto.
+      - rewrite (insert_commute _ 1%Z 2%Z) in Hin2=> //.
+        rewrite lookup_insert in Hin1.
+        rewrite lookup_insert in Hin2.
+        inversion Hin1; inversion Hin2; eauto.
+      - rewrite (insert_commute _ 1%Z 2%Z) in Hin1=> //.
+        rewrite (insert_commute _ 1%Z 2%Z) in Hin2=> //.
+        rewrite lookup_insert in Hin1.
+        rewrite lookup_insert in Hin2.
+        inversion Hin1; inversion Hin2; eauto.
+    }
+    (** Swap recv/send *)
+    iApply (lty_le_trans _ prot4).
+    {
+      iApply lty_le_select. iIntros "!>".
+      rewrite big_sepM2_insert=> //. iSplit.
+      - iApply lty_le_branch. iIntros "!>".
+        rewrite big_sepM2_insert=> //. iSplit.
+        + iApply lty_le_swap_recv_send.
+        + rewrite big_sepM2_insert=> //.
+          iSplit=> //. iApply lty_le_swap_recv_send.
+      - rewrite big_sepM2_insert=> //. iSplit=> //.
+        iApply lty_le_branch. iIntros "!>".
+        rewrite big_sepM2_insert=> //. iSplit.
+        + iApply lty_le_swap_recv_send.
+        + rewrite big_sepM2_insert=> //.
+          iSplit=> //. iApply lty_le_swap_recv_send.
+    }
+    (** Swap branch/send *)
+    iApply (lty_le_trans _ prot5).
+    {
+      iApply lty_le_select. iIntros "!>".
+      rewrite big_sepM2_insert=> //. iSplit.
+      - iApply (lty_le_swap_branch_send _
+          (<[1%Z:=(<??> TY R; END)%lty]> (<[2%Z:=(<??> TY S; END)%lty]> ∅))).
+      - rewrite big_sepM2_insert=> //. iSplit=> //.
+        iApply (lty_le_swap_branch_send _
+          ((<[1%Z:=(<??> TY R; END)%lty]> (<[2%Z:=(<??> TY S; END)%lty]> ∅)))).
+    }
+    (** Weaken branch *)
+    iApply lty_le_select. iIntros "!>".
+    rewrite big_sepM2_insert=> //. iSplit=> //.
+    - iApply lty_le_send; [iApply lty_le_refl|].
+      iApply lty_le_branch_subseteq.
+      rewrite (insert_commute _ 2%Z 3%Z) //.
+      rewrite (insert_commute _ 1%Z 3%Z) //.
+      by apply insert_subseteq.
+    - rewrite big_sepM2_insert=> //. eauto.
+  Qed.
+
+End choice_example.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 5badbfd13cbf04904db67fbd6df14c1760659ed3..eee85cf00ebde5f63c6ec6df73a324b408497086 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -348,6 +348,29 @@ Section subtyping_rules.
     iModIntro. by iExists v2.
   Qed.
 
+  Lemma lty_le_swap_branch_select (Ss1 Ss2 : (gmap Z (gmap Z (lsty Σ)))) :
+    (∀ i j Ss1' Ss2',
+        Ss1 !! i = Some Ss1' → Ss2 !! j = Some Ss2' →
+        (is_Some (Ss1' !! j) ∧ is_Some (Ss2' !! i) ∧
+        Ss1' !! j = Ss2' !! i)) →
+    ⊢ lty_branch ((λ Ss, lty_select Ss) <$> Ss1) <:
+      lty_select ((λ Ss, lty_branch Ss) <$> Ss2).
+  Proof.
+    intros Hin.
+    iIntros "!>" (v1 v2).
+    rewrite !lookup_fmap !fmap_is_Some !lookup_total_alt !lookup_fmap.
+    iIntros ">% >%".
+    destruct H1 as [Ss1' Heq1]. destruct H2 as [Ss2' Heq2].
+    rewrite Heq1 Heq2 /=.
+    destruct (Hin v1 v2 Ss1' Ss2' Heq1 Heq2) as (Hin1 & Hin2 & Heq).
+    iApply iProto_le_trans.
+    { iModIntro. iExists v2. by iApply iProto_le_payload_intro_l. }
+    iApply iProto_le_trans; [ iApply iProto_le_base_swap |].
+    iModIntro. iExists v1.
+    iApply iProto_le_trans; [|by iApply iProto_le_payload_intro_r].
+    iModIntro. rewrite !lookup_total_alt. by rewrite Heq.
+  Qed.
+
   Lemma lty_le_select (Ss1 Ss2 : gmap Z (lsty Σ)) :
     ▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
     lty_select Ss1 <: lty_select Ss2.