diff --git a/CHANGELOG.md b/CHANGELOG.md
index 88c6ce1e6cb83bb357b445a1120d1939c8f8bebd..a52d15289e599c547f29eba0f37e8a8fc7641da4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -106,6 +106,15 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   will fail. We provide one implementation using Ltac2 which works with Coq 8.11
   and can be installed with opam; see
   [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
+* Make names of `f_op`/`f_core` rewrite lemmas more consistent:
+  `op_singleton` -> `singleton_op`, `core_singleton` -> `singleton_core`,
+  `discrete_fun_op_singleton` -> `discrete_fun_singleton_op`,
+  `discrete_fun_core_singleton` -> `discrete_fun_singleton_core`,
+  `list_core_singletonM` -> `list_singletonM_core`,
+  `list_op_singletonM` -> `list_singletonM_op`,
+  `sts_op_auth_frag` -> `sts_auth_frag_op`,
+  `sts_op_auth_frag_up` -> `sts_auth_frag_up_op`,
+  `sts_op_frag` -> `sts_frag_op`.
 
 **Changes in heap_lang:**
 
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 80e65d794a6c49f6b076e39f3e3e1e8bf3c28c13..893c56e0b2915fa738db34af7c6d417062fbdbb6 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -84,7 +84,7 @@ Section cmra.
     by apply ucmra_unit_validN.
   Qed.
 
-  Lemma discrete_fun_core_singleton x (y : B x) :
+  Lemma discrete_fun_singleton_core x (y : B x) :
     core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).
   Proof.
     move=>x'; destruct (decide (x = x')) as [->|];
@@ -94,9 +94,9 @@ Section cmra.
 
   Global Instance discrete_fun_singleton_core_id x (y : B x) :
     CoreId y → CoreId (discrete_fun_singleton x y).
-  Proof. by rewrite !core_id_total discrete_fun_core_singleton=> ->. Qed.
+  Proof. by rewrite !core_id_total discrete_fun_singleton_core=> ->. Qed.
 
-  Lemma discrete_fun_op_singleton (x : A) (y1 y2 : B x) :
+  Lemma discrete_fun_singleton_op (x : A) (y1 y2 : B x) :
     discrete_fun_singleton x y1 ⋅ discrete_fun_singleton x y2 ≡ discrete_fun_singleton x (y1 ⋅ y2).
   Proof.
     intros x'; destruct (decide (x' = x)) as [->|].
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 098a55ebba94d87896278b3f11c2c3d690785372..3cdc9c7bf8c154d973f32adf78d194f8f8cc6c0f 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -284,23 +284,23 @@ Proof.
   - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id_L.
 Qed.
 
-Lemma core_singleton (i : K) (x : A) cx :
+Lemma singleton_core (i : K) (x : A) cx :
   pcore x = Some cx → core {[ i := x ]} =@{gmap K A} {[ i := cx ]}.
 Proof. apply omap_singleton. Qed.
-Lemma core_singleton' (i : K) (x : A) cx :
+Lemma singleton_core' (i : K) (x : A) cx :
   pcore x ≡ Some cx → core {[ i := x ]} ≡@{gmap K A} {[ i := cx ]}.
 Proof.
-  intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
+  intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (singleton_core _ _ cx').
 Qed.
 Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
   core {[ i := x ]} =@{gmap K A} {[ i := core x ]}.
-Proof. apply core_singleton. rewrite cmra_pcore_core //. Qed.
-Lemma op_singleton (i : K) (x y : A) :
+Proof. apply singleton_core. rewrite cmra_pcore_core //. Qed.
+Lemma singleton_op (i : K) (x y : A) :
   {[ i := x ]} â‹… {[ i := y ]} =@{gmap K A} {[ i := x â‹… y ]}.
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
 Global Instance is_op_singleton i a a1 a2 :
   IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
-Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -op_singleton. Qed.
+Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
 
 Global Instance gmap_core_id m : (∀ x : A, CoreId x) → CoreId m.
 Proof.
@@ -309,7 +309,7 @@ Proof.
 Qed.
 Global Instance gmap_singleton_core_id i (x : A) :
   CoreId x → CoreId {[ i := x ]}.
-Proof. intros. by apply core_id_total, core_singleton'. Qed.
+Proof. intros. by apply core_id_total, singleton_core'. Qed.
 
 Lemma singleton_includedN_l n m i x :
   {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ Some x ≼{n} Some y.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index a6d5d0f9289cad342f44f1cbb457c607c7c44835..c49e65582063b51dbe9b4ac2fde0f81587bdb782 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -399,12 +399,12 @@ Section properties.
     rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
   Qed.
 
-  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
+  Lemma list_singletonM_core i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
   Proof.
     rewrite /singletonM /list_singletonM.
     by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ∅).
   Qed.
-  Lemma list_op_singletonM i (x y : A) :
+  Lemma list_singleton_op i (x y : A) :
     {[ i := x ]} ⋅ {[ i := y ]} ≡@{list A} {[ i := x ⋅ y ]}.
   Proof.
     rewrite /singletonM /list_singletonM /=.
@@ -417,7 +417,7 @@ Section properties.
   Qed.
   Global Instance list_singleton_core_id i (x : A) :
     CoreId x → CoreId {[ i := x ]}.
-  Proof. by rewrite !core_id_total list_core_singletonM=> ->. Qed.
+  Proof. by rewrite !core_id_total list_singletonM_core=> ->. Qed.
   Lemma list_singleton_snoc l x:
     {[length l := x]} ⋅ l ≡ l ++ [x].
   Proof. elim: l => //= ?? <-. by rewrite left_id. Qed.
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index db80ca2ac0f0b7d7f5555c5c73ca8aaba15f3524..5681a13992ef986d4cd1f1e3ecbb265c5a084090 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -213,7 +213,7 @@ Proof. rewrite namespace_map_valid_eq /=. split. done. by left. Qed.
 Lemma namespace_map_data_op N a b :
   namespace_map_data N (a â‹… b) = namespace_map_data N a â‹… namespace_map_data N b.
 Proof.
-  by rewrite {2}/op /namespace_map_op /namespace_map_data /= -op_singleton left_id_L.
+  by rewrite {2}/op /namespace_map_op /namespace_map_data /= singleton_op left_id_L.
 Qed.
 Lemma namespace_map_data_mono N a b :
   a ≼ b → namespace_map_data N a ≼ namespace_map_data N b.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index f4c0eb82bfe12839af1d1bc2c4e91149d6577562..e270d09ae98b24f3e4a714256718879aa48b0c72 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -327,14 +327,14 @@ Lemma sts_auth_frag_valid_inv s S T1 T2 :
 Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
 
 (** Op *)
-Lemma sts_op_auth_frag s S T :
+Lemma sts_auth_frag_op s S T :
   s ∈ S → closed S T → sts_auth s ∅ ⋅ sts_frag S T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
   - intros (?&?&?); by apply closed_disjoint with S.
   - intros; split_and?; last constructor; set_solver.
 Qed.
-Lemma sts_op_auth_frag_up s T :
+Lemma sts_auth_frag_up_op s T :
   sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
@@ -346,7 +346,7 @@ Proof.
     + constructor; last set_solver. apply elem_of_up.
 Qed.
 
-Lemma sts_op_frag S1 S2 T1 T2 :
+Lemma sts_frag_op S1 S2 T1 T2 :
   T1 ## T2 → sts.closed S1 T1 → sts.closed S2 T2 →
   sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
 Proof.
@@ -357,7 +357,7 @@ Qed.
 (* Notice that the following does *not* hold -- the composition of the
    two closures is weaker than the closure with the itnersected token
    set.  Also see up_op.
-Lemma sts_op_frag_up s T1 T2 :
+Lemma sts_frag_up_op s T1 T2 :
   T1 ## T2 → sts_frag_up s (T1 ∪ T2) ≡ sts_frag_up s T1 ⋅ sts_frag_up s T2.
 *)
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 1ee1d569d94ecb82507f40f9002b0b1b1bea40bd..091e77d61bd3579e529e8dd943a66855941ecbcc 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -190,7 +190,7 @@ Section gen_heap.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
     intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
-      op_singleton -pair_op agree_idemp.
+      singleton_op -pair_op agree_idemp.
   Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
@@ -200,7 +200,7 @@ Section gen_heap.
   Proof.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
-    f_equiv. rewrite auth_frag_valid op_singleton singleton_valid -pair_op.
+    f_equiv. rewrite auth_frag_valid singleton_op singleton_valid -pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
@@ -255,7 +255,7 @@ Section gen_heap.
     iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
-      move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
+      move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
       rewrite singleton_valid. apply: 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".
@@ -281,7 +281,7 @@ Section gen_heap.
     iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
-      move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
+      move: Hγ. rewrite -auth_frag_op singleton_op=> /auth_frag_valid /=.
       rewrite singleton_valid. apply: agree_op_invL'. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 357f2979e2877143d81fe06fa5dec31ddfba95ce..3b80db9787db36bd8396cf1ff34c92fd2679045d 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -75,7 +75,7 @@ Proof. by intros n a a' Ha; apply discrete_fun_singleton_ne; rewrite Ha. Qed.
 Lemma iRes_singleton_op γ a1 a2 :
   iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
 Proof.
-  by rewrite /iRes_singleton discrete_fun_op_singleton op_singleton cmra_transport_op.
+  rewrite /iRes_singleton discrete_fun_singleton_op singleton_op -cmra_transport_op //.
 Qed.
 
 (** ** Properties of [own] *)
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 6b6b748e4fc9209dc5a876b21e619fccb65ca35d..a283029322e6399e06550ac90744331a88266f9c 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -96,7 +96,7 @@ Section sts.
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
     T1 ## T2 → sts.closed S1 T1 → sts.closed S2 T2 →
     sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2).
-  Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
+  Proof. intros. by rewrite /sts_ownS -own_op sts_frag_op. Qed.
 
   Lemma sts_own_op γ s T1 T2 :
     T1 ## T2 → sts_own γ s (T1 ∪ T2) ==∗ sts_own γ s T1 ∗ sts_own γ s T2.
@@ -104,7 +104,7 @@ Section sts.
   Proof.
     intros. rewrite /sts_own -own_op. iIntros "Hown".
     iDestruct (own_valid with "Hown") as %Hval%sts_frag_up_valid.
-    rewrite -sts_op_frag.
+    rewrite -sts_frag_op.
     - iApply (sts_own_weaken with "Hown"); first done.
       + split; apply sts.elem_of_up.
       + eapply sts.closed_op; apply sts.closed_up; set_solver.
@@ -121,7 +121,7 @@ Section sts.
     iIntros "Hφ". rewrite /sts_ctx /sts_own.
     iMod (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
     { apply sts_auth_valid; set_solver. }
-    iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
+    iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
     iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
     rewrite /sts_inv. iNext. iExists s. by iFrame.
   Qed.
@@ -139,8 +139,8 @@ Section sts.
     iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
     iIntros (s' T') "[% Hφ]".
     iMod (own_update_2 with "Hγ Hγf") as "Hγ".
-    { rewrite sts_op_auth_frag; [|done..]. by apply sts_update_auth. }
-    iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
+    { rewrite sts_auth_frag_op; [|done..]. by apply sts_update_auth. }
+    iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
     iModIntro. iNext. iExists s'; by iFrame.
   Qed.