diff --git a/multi_actris/channel/channel.v b/multi_actris/channel/channel.v
index 11c498bcd9e20d10594e75f0d081d2e0c8376ae0..09d12c001de42b3288f79be61da3470ffa00d6c1 100644
--- a/multi_actris/channel/channel.v
+++ b/multi_actris/channel/channel.v
@@ -353,16 +353,8 @@ Section channel.
     iInv "IH" as "Hctx".
     iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
     iRewrite "Heq" in "Hown".
-    iAssert (▷ (⌜i < n⌝ ∗ iProto_own γ i (<(Send, j)> m') ∗
-                iProto_ctx γ n))%I with "[Hctx Hown]"
-      as "[Hi [Hown Hctx]]".
-    { iNext. iDestruct (iProto_ctx_agree with "Hctx Hown") as %Hi.
-      iFrame. done. }
-    iAssert (▷ (▷ ⌜j < n⌝ ∗ iProto_own γ i (<(Send, j)> m') ∗
-                iProto_ctx γ n))%I with "[Hctx Hown]"
-      as "[Hj [Hown Hctx]]".
-    { iNext. iDestruct (iProto_target with "Hctx Hown") as "[Hin [$ $]]".
-      iFrame. }
+    iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
+    iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
     iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
     wp_smart_apply (vpos_spec); [done|]; iIntros "_".
     iDestruct "Hi" as %Hi.
@@ -444,15 +436,8 @@ Section channel.
     iInv "IH" as "Hctx".
     iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
     iRewrite "Heq" in "Hown".
-    iAssert (▷ (⌜i < n⌝ ∗ iProto_own γ i (<(Recv, j)> m') ∗
-                iProto_ctx γ n))%I with "[Hctx Hown]"
-      as "[Hi [Hown Hctx]]".
-    { iNext. iDestruct (iProto_ctx_agree with "Hctx Hown") as %Hi.
-      iFrame. done. }
-    iAssert (▷ (▷ ⌜j < n⌝ ∗ iProto_own γ i (<(Recv, j)> m') ∗
-                iProto_ctx γ n))%I with "[Hctx Hown]" as "[Hj [Hown Hctx]]".
-    { iNext. iDestruct (iProto_target with "Hctx Hown") as "[Hin [$$]]".
-      iFrame. }
+    iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
+    iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
     iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
     wp_smart_apply (vpos_spec); [done|]; iIntros "_".
     iDestruct "Hi" as %Hi.
diff --git a/multi_actris/channel/proto.v b/multi_actris/channel/proto.v
index aa0826a901447c221041396c7a8b895ac871a5e1..dea40ec8b99f65a2e7d97871efb2a8a92c519876 100644
--- a/multi_actris/channel/proto.v
+++ b/multi_actris/channel/proto.v
@@ -1329,7 +1329,7 @@ Section proto.
   Lemma iProto_target γ ps_dom i a j m :
     iProto_ctx γ ps_dom -∗
     iProto_own γ i (<(a, j)> m) -∗
-    ▷ (⌜j < ps_dom⌝) ∗ iProto_ctx γ ps_dom ∗ iProto_own γ i (<(a, j)> m).
+    ▷ (⌜j < ps_dom⌝).
   Proof.
     iIntros "Hctx Hown".
     rewrite /iProto_ctx /iProto_own.
@@ -1337,14 +1337,10 @@ Section proto.
     iDestruct "Hown" as (p') "[Hle Hown]".
     iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#Hi".
     iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
-    iAssert (▷ (⌜is_Some (ps !! j)⌝ ∗ iProto_consistent ps))%I
-      with "[Hps]" as "[HSome Hps]".
-    { iNext. iRewrite "Heq" in "Hi".
-      iDestruct (iProto_consistent_target with "Hps Hi") as "#$". by iFrame. }
-    iSplitL "HSome".
-    { iNext. iDestruct "HSome" as %Heq.
-      iPureIntro. simplify_eq. by apply lookup_lt_is_Some_1. }
-    iSplitL "Hauth Hps"; iExists _; by iFrame.
+    iDestruct (iProto_consistent_target with "Hps []") as "#H".
+    { iNext. iRewrite "Heq" in "Hi". done. }
+    iNext. iDestruct "H" as %HSome.
+    iPureIntro. subst. by apply lookup_lt_is_Some_1.
   Qed.
 
   (* (** The instances below make it possible to use the tactics [iIntros], *)