diff --git a/multi_actris/channel/channel.v b/multi_actris/channel/channel.v
index 9fa911362d7b958dc579876df615c882db919546..c0a0fbb19e62a9310a021f2f51dc310c35eb4ddc 100644
--- a/multi_actris/channel/channel.v
+++ b/multi_actris/channel/channel.v
@@ -103,7 +103,7 @@ Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
 Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
 Definition iProto_pointsto_eq :
   @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
-Arguments iProto_pointsto {_ _ _} _ _%proto.
+Arguments iProto_pointsto {_ _ _} _ _%_proto.
 Global Instance: Params (@iProto_pointsto) 5 := {}.
 Notation "c ↣ p" := (iProto_pointsto c p)
   (at level 20, format "c  ↣  p").
diff --git a/multi_actris/channel/proofmode.v b/multi_actris/channel/proofmode.v
index 81ca7e6aa3f9e2a12e09d83884b34d8f0766fb81..2c02a5cbfd2973a0372f087e49df5336c0cb4327 100644
--- a/multi_actris/channel/proofmode.v
+++ b/multi_actris/channel/proofmode.v
@@ -39,7 +39,7 @@ Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
     ⊢ iProto_dual_if d p <++>
         foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
 Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
-Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
+Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
 
 Notation ProtoUnfold p1 p2 := (∀ d pas q,
   ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
@@ -49,7 +49,7 @@ Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
   msg_normalize a :
     ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
 Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
-Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
+Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
 
 Section classes.
   Context `{!chanG Σ, !heapGS Σ}.
diff --git a/multi_actris/channel/proto.v b/multi_actris/channel/proto.v
index 75efec70c247bd0b48de12ba23f7551ede3f2706..aaae4751680ac21bf38a47b14c61adc217ed9c78 100644
--- a/multi_actris/channel/proto.v
+++ b/multi_actris/channel/proto.v
@@ -65,7 +65,7 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
 Definition iMsg_base := iMsg_base_aux.(unseal).
 Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
-Arguments iMsg_base {_ _} _%V _%I _%proto.
+Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
 Global Instance: Params (@iMsg_base) 3 := {}.
 
 Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
@@ -74,12 +74,12 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
 Definition iMsg_exist := iMsg_exist_aux.(unseal).
 Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
-Arguments iMsg_exist {_ _ _} _%msg.
+Arguments iMsg_exist {_ _ _} _%_msg.
 Global Instance: Params (@iMsg_exist) 3 := {}.
 
 Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
   tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
-Arguments iMsg_texist {_ _ !_} _%msg /.
+Arguments iMsg_texist {_ _ !_} _%_msg /.
 
 Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
   (at level 200, v at level 20, right associativity,
@@ -114,7 +114,7 @@ Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
 Definition iProto_message := iProto_message_aux.(unseal).
 Definition iProto_message_eq :
   @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
-Arguments iProto_message {_ _} _ _%msg.
+Arguments iProto_message {_ _} _ _%_msg.
 Global Instance: Params (@iProto_message) 3 := {}.
 
 Notation "'END'" := iProto_end : proto_scope.
@@ -166,7 +166,7 @@ Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
 Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
 Definition iProto_app := iProto_app_aux.(unseal).
 Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
-Arguments iProto_app {_ _} _%proto _%proto.
+Arguments iProto_app {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_app) 2 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
@@ -177,13 +177,13 @@ Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
 Definition iProto_dual := iProto_dual_aux.(unseal).
 Definition iProto_dual_eq :
   @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
-Arguments iProto_dual {_ _} _%proto.
+Arguments iProto_dual {_ _} _%_proto.
 Global Instance: Params (@iProto_dual) 2 := {}.
 Notation iMsg_dual := (iMsg_map iProto_dual).
 
 Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
   if d then iProto_dual p else p.
-Arguments iProto_dual_if {_ _} _ _%proto.
+Arguments iProto_dual_if {_ _} _ _%_proto.
 Global Instance: Params (@iProto_dual_if) 3 := {}.
 
 (** * Proofs *)
@@ -487,7 +487,7 @@ Qed.
 Definition iProto_consistent {Σ V} (ps : list (iProto Σ V)) : iProp Σ :=
   fixpoint iProto_consistent_pre' ps.
 
-Arguments iProto_consistent {_ _} _%proto.
+Arguments iProto_consistent {_ _} _%_proto.
 Global Instance: Params (@iProto_consistent) 1 := {}.
 
 Global Instance iProto_consistent_ne {Σ V} : NonExpansive (@iProto_consistent Σ V).
@@ -530,7 +530,7 @@ Proof.
 Qed.
 Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
   fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_ _} _%proto _%proto.
+Arguments iProto_le {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_le) 2 := {}.
 Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
 
@@ -566,7 +566,7 @@ Definition iProto_ctx `{protoG Σ V}
 Definition iProto_own `{!protoG Σ V}
     (γ : gname) (i : nat) (p : iProto Σ V) : iProp Σ :=
   ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ i p'.
-Arguments iProto_own {_ _ _} _ _ _%proto.
+Arguments iProto_own {_ _ _} _ _ _%_proto.
 Global Instance: Params (@iProto_own) 3 := {}.
 
 Global Instance iProto_own_frag_contractive `{protoG Σ V} γ i :
@@ -860,7 +860,7 @@ Section proto.
     { apply (gmap_view_alloc _ (length ps) (DfracOwn 1) (Excl' (Next p))); [|done|done].
       rewrite fmap_map_seq.
       rewrite lookup_map_seq_0.
-      apply lookup_ge_None_2. rewrite fmap_length. done. }
+      apply lookup_ge_None_2. rewrite length_fmap. done. }
     simpl.
     iModIntro. 
     rewrite right_id_L. 
@@ -965,7 +965,7 @@ Section proto.
       iNext.
       iDestruct ("IH" with "Hprot Hle [HSome]") as "HI".
       { rewrite list_lookup_insert; [done|].
-        by rewrite insert_length. }
+        by rewrite length_insert. }
       iClear "IH Hm1 Hm2 Heq".
       rewrite list_insert_insert.
       rewrite (list_insert_commute _ j' i); [|done].
@@ -1266,7 +1266,7 @@ Section proto.
       rewrite list_lookup_insert_ne; [|done].
       rewrite list_lookup_insert; [done|]. lia. }
     { rewrite list_lookup_insert_ne; [|done].
-      rewrite list_lookup_insert; [done|]. rewrite insert_length. lia. }
+      rewrite list_lookup_insert; [done|]. rewrite length_insert. lia. }
     iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
     iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
     iIntros "!>!>". iExists p2. iFrame "Hm2".
@@ -1274,7 +1274,7 @@ Section proto.
     iSplitL "Hconsistent Hauth".
     { iExists (<[i:=p1]> (<[j:=p2]> ps)).
       iSplit.
-      { iPureIntro. rewrite !insert_length. done. } 
+      { iPureIntro. rewrite !length_insert. done. }
       iFrame. rewrite list_insert_insert.
       rewrite list_insert_commute; [|done]. rewrite list_insert_insert.
       by rewrite list_insert_commute; [|done]. }
diff --git a/multi_actris/channel/proto_alt.v b/multi_actris/channel/proto_alt.v
index 8e27dbf061d0f1612e55ca9c01fa5fd45deaae76..1b4f380819b5418e92d365ff34c4e3f099375f37 100644
--- a/multi_actris/channel/proto_alt.v
+++ b/multi_actris/channel/proto_alt.v
@@ -109,7 +109,7 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
 Definition iMsg_base := iMsg_base_aux.(unseal).
 Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
-Arguments iMsg_base {_ _} _%V _%I _%proto.
+Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
 Global Instance: Params (@iMsg_base) 3 := {}.
 
 Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
@@ -118,12 +118,12 @@ Next Obligation. solve_proper. Qed.
 Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
 Definition iMsg_exist := iMsg_exist_aux.(unseal).
 Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
-Arguments iMsg_exist {_ _ _} _%msg.
+Arguments iMsg_exist {_ _ _} _%_msg.
 Global Instance: Params (@iMsg_exist) 3 := {}.
 
 Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
   tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
-Arguments iMsg_texist {_ _ !_} _%msg /.
+Arguments iMsg_texist {_ _ !_} _%_msg /.
 
 Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
   (at level 200, v at level 20, right associativity,
@@ -158,7 +158,7 @@ Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
 Definition iProto_message := iProto_message_aux.(unseal).
 Definition iProto_message_eq :
   @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
-Arguments iProto_message {_ _} _ _%msg.
+Arguments iProto_message {_ _} _ _%_msg.
 Global Instance: Params (@iProto_message) 3 := {}.
 
 Notation "'END'" := iProto_end : proto_scope.
@@ -210,7 +210,7 @@ Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
 Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
 Definition iProto_app := iProto_app_aux.(unseal).
 Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
-Arguments iProto_app {_ _} _%proto _%proto.
+Arguments iProto_app {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_app) 2 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
@@ -221,13 +221,13 @@ Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
 Definition iProto_dual := iProto_dual_aux.(unseal).
 Definition iProto_dual_eq :
   @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
-Arguments iProto_dual {_ _} _%proto.
+Arguments iProto_dual {_ _} _%_proto.
 Global Instance: Params (@iProto_dual) 2 := {}.
 Notation iMsg_dual := (iMsg_map iProto_dual).
 
 Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
   if d then iProto_dual p else p.
-Arguments iProto_dual_if {_ _} _ _%proto.
+Arguments iProto_dual_if {_ _} _ _%_proto.
 Global Instance: Params (@iProto_dual_if) 3 := {}.
 
 (** * Proofs *)
@@ -600,7 +600,7 @@ Qed.
 Definition iProto_consistent {Σ V} (ps : list (iProto Σ V)) : iProp Σ :=
   fixpoint iProto_consistent_pre' ps.
 
-Arguments iProto_consistent {_ _} _%proto.
+Arguments iProto_consistent {_ _} _%_proto.
 Global Instance: Params (@iProto_consistent) 1 := {}.
 
 Global Instance iProto_consistent_ne {Σ V} : NonExpansive (@iProto_consistent Σ V).
@@ -643,7 +643,7 @@ Proof.
 Qed.
 Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
   fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_ _} _%proto _%proto.
+Arguments iProto_le {_ _} _%_proto _%_proto.
 Global Instance: Params (@iProto_le) 2 := {}.
 Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
 
@@ -680,7 +680,7 @@ Definition iProto_ctx `{protoG Σ V}
 Definition iProto_own `{!protoG Σ V}
     (γ : gname) (i : nat) (p : iProto Σ V) : iProp Σ :=
   ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ i p'.
-Arguments iProto_own {_ _ _} _ _ _%proto.
+Arguments iProto_own {_ _ _} _ _ _%_proto.
 Global Instance: Params (@iProto_own) 3 := {}.
 
 Global Instance iProto_own_frag_contractive `{protoG Σ V} γ i :
diff --git a/multi_actris/utils/matrix.v b/multi_actris/utils/matrix.v
index 166b7d260fe28e59da81a8a787d2f7cda984e841..6a643600b5123217ab3561ba789c983692ad161e 100644
--- a/multi_actris/utils/matrix.v
+++ b/multi_actris/utils/matrix.v
@@ -36,7 +36,7 @@ Section with_Σ.
     iDestruct "Hl" as "[Hl Hls]".
     iDestruct ("IHn" with "Hl") as "Hl".
     iFrame=> /=.
-    rewrite Nat.add_0_r !replicate_length.
+    rewrite Nat.add_0_r !length_replicate.
     replace (Z.of_nat (n * m)) with (Z.of_nat n * Z.of_nat m)%Z by lia.
     by iFrame.
   Qed.
@@ -50,7 +50,7 @@ Section with_Σ.
     replace (S n) with (n + 1) by lia.
     rewrite !replicate_add /=. iDestruct "H" as "[H1 H2]".
     iSplitL "H1"; [by iApply "IHn"|]=> /=.
-    by rewrite !replicate_length.
+    by rewrite !length_replicate.
   Qed.
 
   Lemma array_to_matrix l m n v :