diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6433831ba97e9441de74708281330999a977b947..4579eb471c8c0c0b3f7239e84199ccbd83ae4d48 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,11 @@ lemma.
 
 ## Iris master
 
+**Changes in `algebra`:**
+
+* Rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,invL}`, and add
+  `to_agree_op_invN`.
+
 **Changes in `proofmode`:**
 
 * The proofmode now preserves user-supplied names for existentials when using
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 349deb199ebb5dd04879fc9bc5c3037af2b60d82..58e1953b216906899198471ed0b87dd955d770bf 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -81,7 +81,7 @@ Proof.
     iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
     { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
     wp_load. Show.
-    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
+    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_invL; subst.
     iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
     wp_apply wp_assert. wp_pures. by case_bool_decide.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index b7cfef5df12188ce4d23761514ad5de5c6155a07..f93480ae3c26d4e650a3eb8e3ae315c3833a3434 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -99,7 +99,7 @@ Proof.
     + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
       { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
       wp_load. Show.
-      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
+      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_invL; subst.
       iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
       wp_pures. iApply wp_assert. wp_op. by case_bool_decide.
 Qed.
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index d2783d6eca4722c168f1359e10a21f4cde26af25..e3d0baf4f718b0ade3510d90cdcacd38272e01fa 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -237,10 +237,12 @@ Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y.
 Proof.
   intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
 Qed.
-Lemma agree_op_inv' a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.
+Lemma to_agree_op_invN a b n : ✓{n} (to_agree a ⋅ to_agree b) → a ≡{n}≡ b.
+Proof. by intros ?%agree_op_invN%(inj to_agree). Qed.
+Lemma to_agree_op_inv a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.
 Proof. by intros ?%agree_op_inv%(inj to_agree). Qed.
-Lemma agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
-Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.
+Lemma to_agree_op_invL `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
+Proof. by intros ?%to_agree_op_inv%leibniz_equiv. Qed.
 
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b).
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 3d57ed0509f4d992f3bd5b1da19f961cc0a8ffe7..7a4b7e544847d6b983e2667ace143dbcc3a192c9 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -202,7 +202,7 @@ Section gen_heap.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
     f_equiv. rewrite auth_frag_valid singleton_op singleton_valid -pair_op.
-    by intros [_ ?%agree_op_invL'].
+    by intros [_ ?%to_agree_op_invL].
   Qed.
 
   Lemma mapsto_combine l q1 q2 v1 v2 :
@@ -264,7 +264,7 @@ Section gen_heap.
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
       move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
-      rewrite singleton_valid. apply: agree_op_invL'. }
+      rewrite singleton_valid. apply: to_agree_op_invL. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op.
     iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1".
   Qed.
@@ -290,10 +290,10 @@ Section gen_heap.
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
       move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
-      rewrite singleton_valid. apply: agree_op_invL'. }
+      rewrite singleton_valid. apply: to_agree_op_invL. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
-    move=> /agree_op_invL'. naive_solver.
+    move=> /to_agree_op_invL. naive_solver.
   Qed.
   Lemma meta_set `{Countable A} E l (x : A) N :
     ↑ N ⊆ E → meta_token l E ==∗ meta l N x.