diff --git a/coq-iris.opam b/coq-iris.opam
index 732d6566cc3b32573cc204061d991a275bcccfd6..ff0e0ab87fe392355b3105602e4efd8c3d172453 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2024-07-19.1.b4310406") | (= "dev") }
+  "coq-stdpp" { (= "dev.2024-08-16.0.6190d85d") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 98b6366c7d027608b365eb23dac7ff70a0073269..b270ba92dd37cc6d85c6a62306cd5648e1683164 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -111,7 +111,7 @@ Section list.
     ([^o list] k ↦ x ∈ l, Φ k x) ≡
     ([^o list] k ↦ x ∈ take n l, Φ k x) `o` ([^o list] k ↦ x ∈ drop n l, Φ (n + k) x).
   Proof.
-    rewrite -{1}(take_drop n l) big_opL_app take_length.
+    rewrite -{1}(take_drop n l) big_opL_app length_take.
     destruct (decide (length l ≤ n)).
     - rewrite drop_ge //=.
     - rewrite Nat.min_l //=; lia.
diff --git a/iris/algebra/vector.v b/iris/algebra/vector.v
index e34d167c3e9b297bbe8edf04bc0580e9368b5e40..a72cb159b02142424e48bf081f663d0f169280a5 100644
--- a/iris/algebra/vector.v
+++ b/iris/algebra/vector.v
@@ -18,7 +18,7 @@ Section ofe.
     apply: (iso_cofe_subtype (λ l : list A, length l = m)
       (λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //.
     - intros v []. by rewrite /= vec_to_list_to_vec.
-    - intros c. by rewrite (conv_compl 0 (chain_map _ c)) /= vec_to_list_length.
+    - intros c. by rewrite (conv_compl 0 (chain_map _ c)) /= length_vec_to_list.
   Qed.
 
   Global Instance vnil_discrete : Discrete (@vnil A).
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index ed494942484509192fac2489c82c73165675c4f4..dfb75cdafbd7b7772a928910f70468cfb5a374d8 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -189,12 +189,12 @@ Section sep_list.
   Proof.
     intros Hli. assert (i ≤ length l) by eauto using lookup_lt_Some, Nat.lt_le_incl.
     rewrite -(take_drop_middle l i x) // big_sepL_app /=.
-    rewrite Nat.add_0_r take_length_le //.
+    rewrite Nat.add_0_r length_take_le //.
     rewrite assoc -!(comm _ (Φ _ _)) -assoc. apply sep_mono_r, forall_intro=> y.
-    rewrite insert_app_r_alt ?take_length_le //.
+    rewrite insert_app_r_alt ?length_take_le //.
     rewrite Nat.sub_diag /=. apply wand_intro_l.
     rewrite assoc !(comm _ (Φ _ _)) -assoc big_sepL_app /=.
-    by rewrite Nat.add_0_r take_length_le.
+    by rewrite Nat.add_0_r length_take_le.
   Qed.
 
   Lemma big_sepL_lookup_acc Φ l i x :
@@ -207,7 +207,7 @@ Section sep_list.
     l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
   Proof.
     intros Hi. destruct select (TCOr _ _).
-    - rewrite -(take_drop_middle l i x) // big_sepL_app /= take_length.
+    - rewrite -(take_drop_middle l i x) // big_sepL_app /= length_take.
       apply lookup_lt_Some in Hi. rewrite (_ : _ + 0 = i); last lia.
       rewrite sep_elim_r sep_elim_l //.
     - rewrite big_sepL_lookup_acc // sep_elim_l //.
@@ -343,11 +343,11 @@ Section sep_list.
     Φ i x ∗ [∗ list] k↦y ∈ l, if decide (k = i) then emp else Φ k y.
   Proof.
     intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r.
-    rewrite take_length_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
+    rewrite length_take_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
     rewrite decide_True // left_id.
     rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv.
     - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk.
-      rewrite take_length in Hk. by rewrite decide_False; last lia.
+      rewrite length_take in Hk. by rewrite decide_False; last lia.
     - apply big_sepL_proper=> k y _. by rewrite decide_False; last lia.
   Qed.
   Lemma big_sepL_delete' `{!BiAffine PROP} Φ l i x :
@@ -490,7 +490,7 @@ Section sep_list2.
     ([∗ list] k↦y1;y2 ∈ l.*1; l.*2, Φ k y1 y2) ⊣⊢
     [∗ list] k ↦ xy ∈ l, Φ k (xy.1) (xy.2).
   Proof.
-    rewrite big_sepL2_alt !fmap_length.
+    rewrite big_sepL2_alt !length_fmap.
     by rewrite pure_True // True_and zip_fst_snd.
   Qed.
 
@@ -537,9 +537,9 @@ Section sep_list2.
   Proof.
     revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] /= Hlen.
     - by rewrite left_id.
-    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length Hlen /= app_length.
+    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length Hlen /= length_app.
       apply pure_elim'; lia.
-    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length -Hlen /= app_length.
+    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length -Hlen /= length_app.
       apply pure_elim'; lia.
     - by rewrite -assoc IH; last lia.
   Qed.
@@ -677,7 +677,7 @@ Section sep_list2.
     intros Hl1 Hl2. rewrite big_sepL2_alt. apply pure_elim_l=> Hl.
     rewrite {1}big_sepL_insert_acc; last by rewrite lookup_zip_with; simplify_option_eq.
     apply sep_mono_r. apply forall_intro => y1. apply forall_intro => y2.
-    rewrite big_sepL2_alt !insert_length pure_True // left_id -insert_zip_with.
+    rewrite big_sepL2_alt !length_insert pure_True // left_id -insert_zip_with.
     by rewrite (forall_elim (y1, y2)).
   Qed.
 
@@ -698,7 +698,7 @@ Section sep_list2.
     intros Hx1 Hx2. destruct select (TCOr _ _).
     - rewrite -(take_drop_middle l1 i x1) // -(take_drop_middle l2 i x2) //.
       apply lookup_lt_Some in Hx1. apply lookup_lt_Some in Hx2.
-      rewrite big_sepL2_app_same_length /= 2?take_length; last lia.
+      rewrite big_sepL2_app_same_length /= 2?length_take; last lia.
       rewrite (_ : _ + 0 = i); last lia.
       rewrite sep_elim_r sep_elim_l //.
     - rewrite big_sepL2_lookup_acc // sep_elim_l //.
@@ -708,14 +708,14 @@ Section sep_list2.
     ([∗ list] k↦y1;y2 ∈ f <$> l1; l2, Φ k y1 y2)
     ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k (f y1) y2).
   Proof.
-    rewrite !big_sepL2_alt fmap_length zip_with_fmap_l zip_with_zip big_sepL_fmap.
+    rewrite !big_sepL2_alt length_fmap zip_with_fmap_l zip_with_zip big_sepL_fmap.
     by f_equiv; f_equiv=> k [??].
   Qed.
   Lemma big_sepL2_fmap_r {B'} (g : B → B') (Φ : nat → A → B' → PROP) l1 l2 :
     ([∗ list] k↦y1;y2 ∈ l1; g <$> l2, Φ k y1 y2)
     ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 (g y2)).
   Proof.
-    rewrite !big_sepL2_alt fmap_length zip_with_fmap_r zip_with_zip big_sepL_fmap.
+    rewrite !big_sepL2_alt length_fmap zip_with_fmap_r zip_with_zip big_sepL_fmap.
     by f_equiv; f_equiv=> k [??].
   Qed.
 
@@ -865,12 +865,12 @@ Section sep_list2.
   Proof.
     intros. rewrite -(take_drop_middle l1 i x1) // -(take_drop_middle l2 i x2) //.
     assert (i < length l1 ∧ i < length l2) as [??] by eauto using lookup_lt_Some.
-    rewrite !big_sepL2_app_same_length /=; [|rewrite ?take_length; lia..].
-    rewrite Nat.add_0_r take_length_le; [|lia].
+    rewrite !big_sepL2_app_same_length /=; [|rewrite ?length_take; lia..].
+    rewrite Nat.add_0_r length_take_le; [|lia].
     rewrite decide_True // left_id.
     rewrite assoc -!(comm _ (Φ _ _ _)) -assoc. do 2 f_equiv.
     - apply big_sepL2_proper=> k y1 y2 Hk. apply lookup_lt_Some in Hk.
-      rewrite take_length in Hk. by rewrite decide_False; last lia.
+      rewrite length_take in Hk. by rewrite decide_False; last lia.
     - apply big_sepL2_proper=> k y1 y2 _. by rewrite decide_False; last lia.
   Qed.
   Lemma big_sepL2_delete' `{!BiAffine PROP} Φ l1 l2 i x1 x2 :
@@ -1104,7 +1104,7 @@ Section and_list.
     l !! i = Some x → ([∧ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
   Proof.
     intros. rewrite -(take_drop_middle l i x) // big_andL_app /=.
-    rewrite Nat.add_0_r take_length_le;
+    rewrite Nat.add_0_r length_take_le;
       eauto using lookup_lt_Some, Nat.lt_le_incl, and_elim_l', and_elim_r'.
   Qed.
 
@@ -1264,7 +1264,7 @@ Section or_list.
     l !! i = Some x → Φ i x ⊢ ([∨ list] k↦y ∈ l, Φ k y).
   Proof.
     intros. rewrite -(take_drop_middle l i x) // big_orL_app /=.
-    rewrite Nat.add_0_r take_length_le;
+    rewrite Nat.add_0_r length_take_le;
       eauto using lookup_lt_Some, Nat.lt_le_incl, or_intro_l', or_intro_r'.
   Qed.
 
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index ea568c1929c2321920522406a14da3b1b70b3d34..45aa4d14893ffdb15dfbb4c12109fc310c3bd65e 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -249,7 +249,7 @@ Proof.
   iMod 1 as (nt') "(Hσ & Hval) /=".
   iDestruct (big_sepL2_app_inv_r with "Hval") as (es' t2' ->) "[Hes' Ht2']".
   iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
-  rewrite replicate_length in Hlen2; subst.
+  rewrite length_replicate in Hlen2; subst.
   iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
   rewrite -plus_n_O.
   iApply ("Hφ" with "[//] [%] [ ] Hσ Hes'");
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 55875d9ee2905baad1d2a5e5bd8481aa9fe9b5de..a57ce3d1c7a0c834be5d79eba9850b07df639bd0 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -81,13 +81,13 @@ Proof.
   iDestruct (array_app with "Hl") as "[Hl1 Hl]".
   iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
   assert (off < length vs) as H by (apply lookup_lt_is_Some; by eexists).
-  rewrite take_length min_l; last by lia. iFrame "Hl2".
+  rewrite length_take min_l; last by lia. iFrame "Hl2".
   iIntros (w) "Hl2".
   clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
   { apply list_lookup_insert. lia. }
   rewrite -[in (l ↦∗{_} <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
   iApply array_app. rewrite take_insert; last by lia. iFrame.
-  iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
+  iApply array_cons. rewrite length_take min_l; last by lia. iFrame.
   rewrite drop_insert_gt; last by lia. done.
 Qed.
 
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 776239141ac581c1360ac859f8b926a18dd424e5..8ed608ab856fa0ae33032411ca7a268471dd74c1 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -107,7 +107,7 @@ Section proof.
     wp_lam.
     wp_alloc dst as "Hdst"; first by auto.
     wp_smart_apply (twp_array_copy_to with "[$Hdst $Hvl]") as "[Hdst Hl]".
-    - rewrite replicate_length Z2Nat.id; lia.
+    - rewrite length_replicate Z2Nat.id; lia.
     - auto.
     - wp_pures.
       iApply "HΦ"; by iFrame.
@@ -253,7 +253,7 @@ Section proof.
       iIntros (Hn Φ) "Hf HΦ". iApply (wp_array_init with "Hf"); first done.
       iIntros "!>" (l vs). iDestruct 1 as (<-) "[Hl Hvs]".
       iDestruct (big_sepL_exists_eq with "Hvs") as (xs ->) "Hxs".
-      iApply "HΦ". iFrame "Hl Hxs". by rewrite fmap_length.
+      iApply "HΦ". iFrame "Hl Hxs". by rewrite length_fmap.
     Qed.
     Lemma twp_array_init_fmap stk E n f :
       (0 < n)%Z →
@@ -269,7 +269,7 @@ Section proof.
       iIntros (Hn Φ) "Hf HΦ". iApply (twp_array_init with "Hf"); first done.
       iIntros (l vs). iDestruct 1 as (<-) "[Hl Hvs]".
       iDestruct (big_sepL_exists_eq with "Hvs") as (xs ->) "Hxs".
-      iApply "HΦ". iFrame "Hl Hxs". by rewrite fmap_length.
+      iApply "HΦ". iFrame "Hl Hxs". by rewrite length_fmap.
     Qed.
   End array_init_fmap.
 End proof.
diff --git a/iris_heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
index 559391987ff11fa359435318d82e8b85df48b146..b342878455198f85a816acfc6026e52968afa8b0 100644
--- a/iris_heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -156,7 +156,7 @@ Proof.
     apply map_Forall_insert_2; auto.
     apply lookup_union_Some in Hix; last first.
     { eapply heap_array_map_disjoint;
-        rewrite replicate_length Z2Nat.id; auto with lia. }
+        rewrite length_replicate Z2Nat.id; auto with lia. }
     destruct Hix as [(?&?&?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
                      [j Hj]%elem_of_map_to_list%elem_of_list_lookup_1].
     + simplify_eq/=. rewrite !Z2Nat.id in Hlt; eauto with lia.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 6e7800ded36f11a8c9ce155709d4909f6cc9e401..522bc118c5b271a4cdc2ddbc09d1b0e88fada573 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -401,12 +401,12 @@ Proof.
   iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
   { apply heap_array_map_disjoint.
-    rewrite replicate_length Z2Nat.id; auto with lia. }
+    rewrite length_replicate Z2Nat.id; auto with lia. }
   iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
   iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs Hsteps". iApply "HΦ".
   iApply big_sepL_sep. iSplitL "Hl".
   - by iApply heap_array_to_seq_pointsto.
-  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
+  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite length_replicate.
 Qed.
 Lemma wp_allocN_seq s E v n :
   (0 < n)%Z →
diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 191dcaa0a641f86d9e58bde95f54578948622430..cbca270a3a7acccf93c5e1c4c82df0b2dd4ac36f 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -580,7 +580,7 @@ Proof.
       * (** e1 is of the form ([Resolve] e10 e11 v0) and e11 takes a base_step. *)
         inversion Hhstp'; simplify_eq.
         edestruct (IH K) as (?&?&?&?&?&Hpstp&?&?&?&?);
-          [rewrite !app_length /=; lia|done|by eapply base_step_not_stuck|];
+          [rewrite !length_app /=; lia|done|by eapply base_step_not_stuck|];
             simplify_eq/=.
         apply base_reducible_prim_step in Hpstp; simpl in *;
           last by rewrite /base_reducible /=; eauto 10.
@@ -597,7 +597,7 @@ Proof.
            (non-head) prim_step. *)
         rewrite fill_app in Hrs; simplify_eq/=.
         edestruct (IH K) as (?&?&?&?&?&Hpstp&Hprstps&?&?&?);
-          [rewrite !app_length; lia|done| |].
+          [rewrite !length_app; lia|done| |].
         { change (fill_item Ki) with (fill [Ki]).
           by rewrite -fill_app; eapply prim_step_not_stuck, Ectx_step. }
         simplify_eq/=.
@@ -622,11 +622,11 @@ Proof.
             end
         end.
       apply (prim_step_matched_by_erased_steps_ectx [ResolveMCtx _ _]).
-      apply IH; [rewrite !app_length /=; lia|done|
+      apply IH; [rewrite !length_app /=; lia|done|
                  by eapply (not_stuck_fill_inv (fill [ResolveMCtx _ _])); simpl].
   - (** e1 is of the form ([Resolve] e1_ e1_2 e13) and e1_3 takes a prim_step. *)
     apply (prim_step_matched_by_erased_steps_ectx [ResolveRCtx _ _]).
-    apply IH; [rewrite !app_length /=; lia|done|
+    apply IH; [rewrite !length_app /=; lia|done|
                  by eapply (not_stuck_fill_inv (fill [ResolveRCtx _ _])); simpl].
 Qed.
 
@@ -644,7 +644,7 @@ Proof.
   { apply erased_base_step_base_step in Hhstp as (?&?&?&?&?&<-&?&<-).
     eexists _, _, _, _, _; repeat split;
       first (by apply base_prim_step); auto using rtc_refl. }
-  rewrite app_length in IHm; simpl in *.
+  rewrite length_app in IHm; simpl in *.
   rewrite fill_app /=; rewrite fill_app /= in He1.
   eapply prim_step_matched_by_erased_steps_ectx_item; eauto; [].
   { intros K' **; simpl in *. apply (IHm (length K')); auto with lia. }
@@ -845,11 +845,11 @@ Proof.
   rewrite list_fmap_insert/=.
   apply Forall2_app; last done.
   apply Forall2_same_length_lookup; split.
-  { apply Forall2_length in Hprstps; rewrite fmap_length in Hprstps.
-    by rewrite !insert_length fmap_length. }
+  { apply Forall2_length in Hprstps; rewrite length_fmap in Hprstps.
+    by rewrite !length_insert length_fmap. }
   intros j x y.
   destruct (decide (i = j)); simplify_eq.
-  { rewrite !list_lookup_insert ?fmap_length; eauto using lookup_lt_Some; [].
+  { rewrite !list_lookup_insert ?length_fmap; eauto using lookup_lt_Some; [].
     by intros ? ?; simplify_eq. }
   rewrite !list_lookup_insert_ne // list_lookup_fmap.
   intros ? ?.
diff --git a/iris_unstable/algebra/list.v b/iris_unstable/algebra/list.v
index 47300ee4947f58690dff003cf3aed018d042d3e0..2db1c192e930522a7938cdc11447cb5fe4b1eb0d 100644
--- a/iris_unstable/algebra/list.v
+++ b/iris_unstable/algebra/list.v
@@ -232,7 +232,7 @@ Section properties.
   Qed.
   Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
   Proof.
-    rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
+    rewrite /singletonM /list_singletonM length_app length_replicate /=; lia.
   Qed.
 
   Lemma list_singletonM_core i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
@@ -344,7 +344,7 @@ Section properties.
       + by rewrite !list_lookup_opM !lookup_app_l.
       + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM; apply (Hxy n).
       + rewrite !(cons_middle _ l1 l2) !assoc.
-        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
+        rewrite !list_lookup_opM !lookup_app_r !length_app //=; lia.
     - intros n mk; rewrite !list_lookup_validN !list_dist_lookup => Hl Hl' i.
       move: (Hl i) (Hl' i).
       destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
@@ -352,11 +352,11 @@ Section properties.
       + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM !inj_iff.
         apply (Hxy' n).
       + rewrite !(cons_middle _ l1 l2) !assoc.
-        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
+        rewrite !list_lookup_opM !lookup_app_r !length_app //=; lia.
   Qed.
   Lemma list_singleton_local_update i x y ml :
     x ~l~> y @ ml ≫= (.!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
-  Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
+  Proof. intros; apply list_middle_local_update. by rewrite length_replicate. Qed.
 *)
 
   Lemma list_alloc_singletonM_local_update x l :
@@ -413,7 +413,7 @@ Section properties.
     rewrite Hk'eq.
     apply list_dist_lookup. intros i. rewrite !list_lookup_op.
     destruct (decide (i < length l)%nat) as [HLt|HGe].
-    - rewrite !lookup_app_l //; last by rewrite replicate_length.
+    - rewrite !lookup_app_l //; last by rewrite length_replicate.
       rewrite lookup_take; last done.
       rewrite lookup_replicate_2; last done.
       rewrite comm assoc -list_lookup_op.
@@ -422,8 +422,8 @@ Section properties.
       apply lookup_lt_is_Some in HLt as [? HEl].
       by rewrite HEl -Some_op ucmra_unit_right_id.
     - assert (length l ≤ i)%nat as HLe by lia.
-      rewrite !lookup_app_r //; last by rewrite replicate_length.
-      rewrite replicate_length.
+      rewrite !lookup_app_r //; last by rewrite length_replicate.
+      rewrite length_replicate.
       rewrite lookup_take_ge; last done.
       replace (mm !! _) with (drop (length l) mm !! (i - length l)%nat);
         last by rewrite lookup_drop; congr (mm !! _); lia.
@@ -469,7 +469,7 @@ Section properties.
     move: HLen. rewrite Hl'eq. clear. move=> HLen.
     assert (length m' ≤ length l)%nat as HLen'.
     { by rewrite list_length_op in HLen; lia. }
-    rewrite list_op_app list_length_op replicate_length max_l;
+    rewrite list_op_app list_length_op length_replicate max_l;
       last lia.
     rewrite list_drop_op -assoc. rewrite HLen. move: HLen'.
     remember (length l) as o. clear.
@@ -480,7 +480,7 @@ Section properties.
     subst. remember (m' â‹… take _ _) as m''.
     remember (length m' `max` length (take o mm))%nat as o''.
     assert (o'' ≤ length m'')%nat as HLen.
-    { by subst; rewrite list_length_op !take_length; lia. }
+    { by subst; rewrite list_length_op !length_take; lia. }
     move: HLen. clear.
     intros HLen. move: n. apply equiv_dist, list_equiv_lookup.
     intros i. rewrite list_lookup_op.
@@ -493,7 +493,7 @@ Section properties.
       by rewrite -Some_op ucmra_unit_left_id.
     - rewrite lookup_ge_None_2.
       { rewrite lookup_ge_None_2 //.
-        by rewrite replicate_length; lia. }
+        by rewrite length_replicate; lia. }
       rewrite -HeqL. lia.
   Qed.