diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 6a69f5ecd646203501019e976be72dd61126daef..dabfc95f73f8efc9362da351276385b8b7d0aa03 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -157,6 +157,44 @@ Section channel.
     Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_choice Σ a).
   Proof. solve_proper. Qed.
 
+  Lemma iProto_choice_equiv a1 a2 (P11 P12 P21 P22 : iProp Σ)
+        (p11 p12 p21 p22 : iProto Σ) :
+    ⌜a1 = a2⌝ -∗ ((P11 ≡ P12):iProp Σ) -∗ (P21 ≡ P22) -∗
+    ▷ (p11 ≡ p12) -∗ ▷ (p21 ≡ p22) -∗
+    (iProto_choice a1 P11 P21 p11 p21 ≡ iProto_choice a2 P12 P22 p12 p22).
+  Proof.
+    iIntros (->) "#HP1 #HP2 #Hp1 #Hp2".
+    rewrite iProto_message_equivI.
+    iSplit; [ done | ].
+    iIntros (v lp).
+    rewrite iMsg_exist_eq iMsg_base_eq /=.
+    iApply prop_ext; iIntros "!>"; iSplit.
+    - iDestruct 1 as (b Hbeq) "[Hp HP]".
+      iExists b. rewrite Hbeq.
+      destruct lp as [lp]. destruct b.
+      + iRewrite -"HP1".
+        iSplit; [ done | ]. iFrame "HP".
+        iIntros "!>".
+        by iRewrite -"Hp1".
+      + iRewrite -"HP2".
+        iSplit; [ done | ]. iFrame "HP".
+        iIntros "!>".
+        by iRewrite -"Hp2".
+    - iDestruct 1 as (b Hbeq) "[Hp HP]".
+      iExists b. rewrite Hbeq.
+      destruct lp as [lp].
+      destruct b.
+      + iRewrite "HP1".
+        iSplit; [ done | ]. iFrame "HP".
+        iIntros "!>".
+        by iRewrite "Hp1".
+      + iRewrite "HP2".
+        iSplit; [ done | ]. iFrame "HP".
+        iIntros "!>".
+        by iRewrite "Hp2".
+  Qed.
+
+
   Lemma iProto_dual_choice a P1 P2 p1 p2 :
     iProto_dual (iProto_choice a P1 P2 p1 p2)
     ≡ iProto_choice (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).