diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 93341be68ce528dab3cf2f9828b777f51cfafd5e..3fc2018f09507a72b228f08f543da35d03c5a7b9 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -348,6 +348,36 @@ Section proto.
     (<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧
       (∀ v lp, iMsg_car m1 v lp ≡ iMsg_car m2 v lp).
   Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
+
+  Lemma iProto_message_equiv {TT1 TT2 : tele} a1 a2
+        (v1 : TT1 → V) (v2 : TT2 → V)
+        (P1 : TT1 → iProp Σ) (P2 : TT2 → iProp Σ)
+        (prot1 : TT1 → iProto Σ V) (prot2 : TT2 → iProto Σ V) :
+    ⌜ a1 = a2 ⌝ -∗
+    (■ ∀ (xs1 : TT1), P1 xs1 -∗
+       ∃ (xs2 : TT2), ⌜v1 xs1 = v2 xs2⌝ ∗ ▷ (prot1 xs1 ≡ prot2 xs2) ∗ P2 xs2) -∗
+    (■ ∀ (xs2 : TT2), P2 xs2 -∗
+       ∃ (xs1 : TT1), ⌜v1 xs1 = v2 xs2⌝ ∗ ▷ (prot1 xs1 ≡ prot2 xs2) ∗ P1 xs1) -∗
+      (<a1 @ xs1> MSG (v1 xs1) {{ P1 xs1 }} ; prot1 xs1) ≡
+      (<a2 @ xs2> MSG (v2 xs2) {{ P2 xs2 }} ; prot2 xs2).
+  Proof.
+    iIntros (Heq) "#Heq1 #Heq2".
+    rewrite iProto_message_eq proto_message_equivI iMsg_exist_eq iMsg_base_eq /=.
+    iSplit; [ done | ].
+    iIntros (v p'). iApply prop_ext.
+    iIntros "!>". iSplit.
+    - iDestruct 1 as (xs1 Hveq1) "[Hrec1 HP1]".
+      iDestruct ("Heq1" with "HP1") as (xs2 Hveq2) "[Hrec2 HP2]".
+      iExists xs2. rewrite -Hveq1 Hveq2.
+      iSplitR; [ done | ]. iSplitR "HP2"; [ | done ].
+      iRewrite -"Hrec1". iApply later_equivI. iIntros "!>". by iRewrite "Hrec2".
+    - iDestruct 1 as (xs2 Hveq2) "[Hrec2 HP2]".
+      iDestruct ("Heq2" with "HP2") as (xs1 Hveq1) "[Hrec1 HP1]".
+      iExists xs1. rewrite -Hveq2 Hveq1.
+      iSplitR; [ done | ]. iSplitR "HP1"; [ | done ].
+      iRewrite -"Hrec2". iApply later_equivI. iIntros "!>". by iRewrite "Hrec1".
+  Qed.
+
   Lemma iProto_message_end_equivI `{!BiInternalEq SPROP} a m :
     (<a> m) ≡ END ⊢@{SPROP} False.
   Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.