diff --git a/CHANGELOG.md b/CHANGELOG.md
index 88c6ce1e6cb83bb357b445a1120d1939c8f8bebd..4447be5670957c911ad7df39d37a7b6d73c1fa1c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -106,6 +106,48 @@ 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 by always making
+  `_core`/`_op` the suffix:
+  `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_singleton_core`,
+  `list_op_singletonM` -> `list_singleton_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`,
+  `list_op_length` -> `list_length_op`.
+* Make list singleton lemmas consistent with gmap by dropping the `M` suffix of
+  `singleton`:
+  `elem_of_list_singletonM` -> `elem_of_list_singleton`,
+  `list_lookup_singletonM` -> `list_lookup_singleton`,
+  `list_lookup_singletonM_lt` -> `list_lookup_singleton_lt`,
+  `list_lookup_singletonM_gt` -> `list_lookup_singleton_gt`,
+  `list_lookup_singletonM_ne` -> `list_lookup_singleton_ne`,
+  `list_singletonM_validN` -> `list_singleton_validN`,
+  `list_singletonM_length` -> `list_singleton_length`,
+  `list_alter_singletonM` -> `list_alter_singleton`,
+  `list_singletonM_included` -> `list_singleton_included`.
+
+The following `sed` script should perform most of the renaming (FIXME: incomplete)
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
+```
+sed -i -E '
+# f_op/f_core renames
+s/\b(op|core)_singleton\b/singleton_\1/g
+s/\bdiscrete_fun_(op|core)_singleton\b/discrete_fun_singleton_\1/g
+s/\blist_(op|core)_singletonM\b/list_singleton_\1/g
+s/\bsts_op_(auth_frag|auth_frag_up|frag)\b/sts_\1_op/g
+s/\blist_op_length\b/list_length_op/g
+# list singleton renames
+s/\belem_of_list_singletonM\b/elem_of_list_singleton/g
+s/\blist_lookup_singletonM(|_lt|_gt|_ne)\b/list_lookup_singleton\1/g
+s/\blist_singletonM_(validN|length)\b/list_singleton_\1/g
+s/\blist_alter_singletonM\b/list_alter_singleton/g
+s/\blist_singletonM_included\b/list_singleton_included/g
+' $(find theories -name "*.v")
+```
+
 
 **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..e826a54960525ebae106b69bd2fa87078be438fa 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -354,7 +354,7 @@ Section properties.
   Lemma list_lookup_valid_Some l i x : ✓ l → l !! i ≡ Some x → ✓ x.
   Proof. move=> /list_lookup_valid /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.
 
-  Lemma list_op_length l1 l2 : length (l1 â‹… l2) = max (length l1) (length l2).
+  Lemma list_length_op l1 l2 : length (l1 â‹… l2) = max (length l1) (length l2).
   Proof. revert l2. induction l1; intros [|??]; f_equal/=; auto. Qed.
 
   Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
@@ -365,75 +365,75 @@ Section properties.
   Global Instance list_singletonM_proper i :
     Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
 
-  Lemma elem_of_list_singletonM i z x : z ∈ ({[i := x]} : list A) → z = ε ∨ z = x.
+  Lemma elem_of_list_singleton i z x : z ∈ ({[i := x]} : list A) → z = ε ∨ z = x.
   Proof.
     rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
   Qed.
-  Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
+  Lemma list_lookup_singleton i x : ({[ i := x ]} : list A) !! i = Some x.
   Proof. induction i; by f_equal/=. Qed.
-  Lemma list_lookup_singletonM_lt i i' x:
+  Lemma list_lookup_singleton_lt i i' x:
     (i' < i)%nat → ({[ i := x ]} : list A) !! i' = Some ε.
   Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
-  Lemma list_lookup_singletonM_gt i i' x:
+  Lemma list_lookup_singleton_gt i i' x:
     (i < i')%nat → ({[ i := x ]} : list A) !! i' = None.
   Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
-  Lemma list_lookup_singletonM_ne i j x :
+  Lemma list_lookup_singleton_ne i j x :
     i ≠ j →
     ({[ i := x ]} : list A) !! j = None ∨ ({[ i := x ]} : list A) !! j = Some ε.
   Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
-  Lemma list_singletonM_validN n i x : ✓{n} ({[ i := x ]} : list A) ↔ ✓{n} x.
+  Lemma list_singleton_validN n i x : ✓{n} ({[ i := x ]} : list A) ↔ ✓{n} x.
   Proof.
     rewrite list_lookup_validN. split.
-    { move=> /(_ i). by rewrite list_lookup_singletonM. }
+    { move=> /(_ i). by rewrite list_lookup_singleton. }
     intros Hx j; destruct (decide (i = j)); subst.
-    - by rewrite list_lookup_singletonM.
-    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
+    - by rewrite list_lookup_singleton.
+    - destruct (list_lookup_singleton_ne i j x) as [Hi|Hi]; first done;
         rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
   Qed.
   Lemma list_singleton_valid  i x : ✓ ({[ i := x ]} : list A) ↔ ✓ x.
   Proof.
-    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
+    rewrite !cmra_valid_validN. by setoid_rewrite list_singleton_validN.
   Qed.
-  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
+  Lemma list_singleton_length i x : length {[ i := x ]} = S i.
   Proof.
     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_singleton_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 /=.
     induction i; constructor; rewrite ?left_id; auto.
   Qed.
-  Lemma list_alter_singletonM f i x :
+  Lemma list_alter_singleton f i x :
     alter f i ({[i := x]} : list A) = {[i := f x]}.
   Proof.
     rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
   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_singleton_core=> ->. Qed.
   Lemma list_singleton_snoc l x:
     {[length l := x]} ⋅ l ≡ l ++ [x].
   Proof. elim: l => //= ?? <-. by rewrite left_id. Qed.
-  Lemma list_singletonM_included i x l:
+  Lemma list_singleton_included i x l:
     {[i := x]} ≼ l ↔ (∃ x', l !! i = Some x' ∧ x ≼ x').
   Proof.
     rewrite list_lookup_included. split.
-    { move /(_ i). rewrite list_lookup_singletonM option_included_total.
+    { move /(_ i). rewrite list_lookup_singleton option_included_total.
       naive_solver. }
     intros (y&Hi&?) j. destruct (Nat.lt_total j i) as [?|[->|?]].
-    - rewrite list_lookup_singletonM_lt //.
+    - rewrite list_lookup_singleton_lt //.
       destruct (lookup_lt_is_Some_2 l j) as [z Hz].
       { trans i; eauto using lookup_lt_Some. }
       rewrite Hz. by apply Some_included_2, ucmra_unit_least.
-    - rewrite list_lookup_singletonM Hi. by apply Some_included_2.
-    - rewrite list_lookup_singletonM_gt //. apply: ucmra_unit_least.
+    - rewrite list_lookup_singleton Hi. by apply Some_included_2.
+    - rewrite list_lookup_singleton_gt //. apply: ucmra_unit_least.
   Qed.
 
   (* Update *)
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.