diff --git a/multi_actris/channel/channel.v b/multi_actris/channel/channel.v
index 857323669244e06d85abe817fa84db8eaf092c28..7e68d817c042bd88749916140f5463875a3fbd55 100644
--- a/multi_actris/channel/channel.v
+++ b/multi_actris/channel/channel.v
@@ -373,10 +373,10 @@ Section channel.
     rewrite iMsg_base_eq.
     iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
     wp_pures.
-    iMod (own_update_2 with "H● H◯") as "[H● H◯]";[apply excl_auth_update|].
-    iModIntro. iApply "HΦ".
-    iFrame. iExists _, _, _, _, _, _. iSplit; [done|].
-    iRewrite "Hp". iFrame "#∗". iApply iProto_le_refl.
+    iMod (own_update_2 with "H● H◯") as "[H● H◯]";
+      [apply (excl_auth_update _ _ (Next p'''))|].
+    iModIntro. iApply "HΦ". rewrite /iProto_pointsto_def. iFrame "IH Hls ∗".
+    iSplit; [done|]. iRewrite "Hp". iApply iProto_le_refl.
   Qed.
 
 End channel.
diff --git a/multi_actris/channel/proto.v b/multi_actris/channel/proto.v
index dea40ec8b99f65a2e7d97871efb2a8a92c519876..fdd225fe5370f19e307e9d9e0373e887e9b23d96 100644
--- a/multi_actris/channel/proto.v
+++ b/multi_actris/channel/proto.v
@@ -912,8 +912,7 @@ Section proto.
     iSplitL "Hauth".
     - rewrite /iProto_own_auth.
       rewrite map_seq_snoc. simpl. done.
-    - iSplit; [|done].
-      iExists _. iFrame. by iApply iProto_le_refl.
+    - by iApply iProto_le_refl.
   Qed.
 
   Lemma list_lookup_Some_le (ps : list $ iProto Σ V) (i : nat) (p1 : iProto Σ V) :
@@ -1271,7 +1270,7 @@ Section proto.
   Proof.
     iIntros "Hconsistent".
     iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
-    iExists γ. iFrame. iExists _. by iFrame.
+    iExists γ. by iFrame.
   Qed.
 
   Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
@@ -1416,7 +1415,7 @@ Section proto.
 
 End proto.
 
-Typeclasses Opaque iProto_ctx iProto_own.
+Global Typeclasses Opaque iProto_ctx iProto_own.
 
 Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
   first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.