diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4579eb471c8c0c0b3f7239e84199ccbd83ae4d48..3f5aebcf21599021f19dd3089759fbb71ad409c2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,8 +7,12 @@ lemma.
 
 **Changes in `algebra`:**
 
-* Rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,invL}`, and add
+* Rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,inv_L}`, and add
   `to_agree_op_invN`.
+* Rename `auth_auth_frac_op_invL` to `auth_auth_frac_op_inv_L`,
+  `excl_auth_agreeL` to `excl_auth_agree_L`,
+  `frac_auth_agreeL` to `frac_auth_agree_L`, and
+  `ufrac_auth_agreeL` to `ufrac_auth_agree_L`.
 
 **Changes in `proofmode`:**
 
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 58e1953b216906899198471ed0b87dd955d770bf..13b4e05aaef3fa9b9749cff8191b50fec1d2ca44 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 %?%to_agree_op_invL; subst.
+    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; 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 f93480ae3c26d4e650a3eb8e3ae315c3833a3434..40efb5efc3e972c6887bce976b8de1d1d4da568f 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 %?%to_agree_op_invL; subst.
+      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; 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 e3d0baf4f718b0ade3510d90cdcacd38272e01fa..7ace47ceae2edce9d53e37d77a1511afdefc821f 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -241,7 +241,7 @@ Lemma to_agree_op_invN a b n : ✓{n} (to_agree a ⋅ to_agree b) → a ≡{n}
 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 to_agree_op_invL `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
+Lemma to_agree_op_inv_L `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
 Proof. by intros ?%to_agree_op_inv%leibniz_equiv. Qed.
 
 (** Internalized properties *)
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 6df092d8c8ce059d7a245014a69d346dc53edc83..d8f9fbbe81f088544fb6d7379398f1dd04b9ac34 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -329,7 +329,7 @@ Proof.
   intros ?. apply equiv_dist. intros n.
   by eapply auth_auth_frac_op_invN, cmra_valid_validN.
 Qed.
-Lemma auth_auth_frac_op_invL `{!LeibnizEquiv A} q a p b :
+Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
   ✓ (●{p} a ⋅ ●{q} b) → a = b.
 Proof. by intros ?%auth_auth_frac_op_inv%leibniz_equiv. Qed.
 
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index 9a086658334337a40602df2d94ea0f42488bb38d..c66266846023b8d075fef2a3abb6049ed8b14146 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -57,7 +57,7 @@ Section excl_auth.
   Proof.
     intros. apply equiv_dist=> n. by apply excl_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma excl_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
+  Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
   Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
 
   Lemma excl_auth_agreeI {M} a b : ✓ (●E a ⋅ ◯E b) ⊢@{uPredI M} (a ≡ b).
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 14cc4b58b031413a927ee81fb3dad58ebeda51a1..9fbdca93f5ce3d975264da8ceae47e28c312b477 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -60,7 +60,7 @@ Section frac_auth.
   Proof.
     intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●F a ⋅ ◯F b) → a = b.
+  Lemma frac_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●F a ⋅ ◯F b) → a = b.
   Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
 
   Lemma frac_auth_includedN n q a b : ✓{n} (●F a ⋅ ◯F{q} b) → Some b ≼{n} Some a.
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index 9020deebf2840e5f4e806da179310de71289eae1..c8423c36c6119f46b95cc5cbe3711b59e49affdf 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -80,7 +80,7 @@ Section ufrac_auth.
   Proof.
     intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma ufrac_auth_agreeL `{!LeibnizEquiv A} p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a = b.
+  Lemma ufrac_auth_agree_L `{!LeibnizEquiv A} p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a = b.
   Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed.
 
   Lemma ufrac_auth_includedN n p q a b : ✓{n} (●U{p} a ⋅ ◯U{q} b) → Some b ≼{n} Some a.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index a02be5297f8151f7e2c7ff47ed4eac299b4ce21b..3af37d7be503f1ad48291233a2de74ae2f6cdd0a 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -78,7 +78,7 @@ Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2) ⊢ ⌜b1 = b2⌝.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  by iDestruct 1 as %?%excl_auth_agreeL.
+  by iDestruct 1 as %?%excl_auth_agree_L.
 Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 7a4b7e544847d6b983e2667ace143dbcc3a192c9..8504c92965be7222fce1e7162a199f067c86912c 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 [_ ?%to_agree_op_invL].
+    by intros [_ ?%to_agree_op_inv_L].
   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: to_agree_op_invL. }
+      rewrite singleton_valid. apply: to_agree_op_inv_L. }
     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: to_agree_op_invL. }
+      rewrite singleton_valid. apply: to_agree_op_inv_L. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
-    move=> /to_agree_op_invL. naive_solver.
+    move=> /to_agree_op_inv_L. naive_solver.
   Qed.
   Lemma meta_set `{Countable A} E l (x : A) N :
     ↑ N ⊆ E → meta_token l E ==∗ meta l N x.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 0cc86cfab7a83652c4f13494edb531a0014a8559..f79e35315903c705ce73691019333ca628b62b9a 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -159,7 +159,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
+    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agree_L.
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
   Qed.