diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7e2233fe69fca923848aa6e0faea7b3456efb837..845c46534100e9e5d86aa77c168bd1b6aa390b66 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -105,6 +105,20 @@ API-breaking change is listed.
   `take` lemmas.
 - Add lemmas `lookup_singleton_is_Some`, `list_lookup_insert_is_Some`,
   `list_lookup_insert_None`.
+- Rename lemmas `elem_of_list_X` into `list_elem_of_X` to be consistent with
+  the `list_lookup_X` lemmas. The `sed` script contains all renames, the
+  following renames were special since they fix other inconsistencies:
+  `list_elem_of_fmap_1` → `list_elem_of_fmap_2`,
+  `list_elem_of_fmap_1_alt` → `list_elem_of_fmap_2'`,
+  `list_elem_of_fmap_2` → `list_elem_of_fmap_1`,
+  `list_lookup_fmap_inv` → `list_lookup_fmap_Some_1`,
+  `list_elem_of_fmap_2_inj` → `list_elem_of_fmap_inj_2`.
+- Change the order of the conjunction in `list_lookup_fmap_Some`. The new
+  version is `(f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x`, which
+  makes it consistent with `list_elem_of_fmap` and the corresponding lemmas for
+  sets and maps.
+- Rename `list_alter_fmap` → `list_fmap_alter`.
+- Remove `list_alter_fmap_mono`, use `list_fmap_alter` instead.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -179,6 +193,45 @@ s/\btake_alter\b/take_alter_ge/g
 s/\bdrop_alter\b/drop_alter_lt/g
 s/\bdrop_insert_le\b/drop_insert_gt/g # make inequality consistent with take lemma
 s/\bdrop_insert_gt\b/drop_insert_lt/g # make inequality consistent with take lemma
+
+# list_elem_of
+s/\bdecompose_elem_of_list\b/decompose_list_elem_of/g
+s/\belem_of_list\b/list_elem_of/g
+s/\belem_of_list_here\b/list_elem_of_here/g
+s/\belem_of_list_further\b/list_elem_of_further/g
+s/\belem_of_list_In\b/list_elem_of_In/g
+s/\belem_of_list_singleton\b/list_elem_of_singleton/g
+s/\belem_of_list_lookup_1\b/list_elem_of_lookup_1/g
+s/\belem_of_list_lookup_total_1\b/list_elem_of_lookup_total_1/g
+s/\belem_of_list_lookup_2\b/list_elem_of_lookup_2/g
+s/\belem_of_list_lookup_total_2\b/list_elem_of_lookup_total_2/g
+s/\belem_of_list_lookup\b/list_elem_of_lookup/g
+s/\belem_of_list_lookup_total\b/list_elem_of_lookup_total/g
+s/\belem_of_list_split_length\b/list_elem_of_split_length/g
+s/\belem_of_list_split\b/list_elem_of_split/g
+s/\belem_of_list_split_l\b/list_elem_of_split_l/g
+s/\belem_of_list_split_r\b/list_elem_of_split_r/g
+s/\belem_of_list_intersection_with\b/list_elem_of_intersection_with/g
+s/\belem_of_list_difference\b/list_elem_of_difference/g
+s/\belem_of_list_union\b/list_elem_of_union/g
+s/\belem_of_list_intersection\b/list_elem_of_intersection/g
+s/\belem_of_list_filter\b/list_elem_of_filter/g
+s/\belem_of_list_fmap\b/list_elem_of_fmap/g
+s/\belem_of_list_fmap_1\b/list_elem_of_fmap_2/g
+s/\belem_of_list_fmap_2\b/list_elem_of_fmap_1/g
+s/\belem_of_list_fmap_1_alt\b/list_elem_of_fmap_2'/g
+s/\belem_of_list_fmap_inj\b/list_elem_of_fmap_inj/g
+s/\belem_of_list_fmap_2_inj\b/list_elem_of_fmap_inj_2/g
+s/\belem_of_list_omap\b/list_elem_of_omap/g
+s/\belem_of_list_bind\b/list_elem_of_bind/g
+s/\belem_of_list_ret\b/list_elem_of_ret/g
+s/\belem_of_list_join\b/list_elem_of_join/g
+s/\belem_of_list_dec\b/list_elem_of_dec/g
+
+# list fmap lemmas
+s/\blist_lookup_fmap_inv\b/list_lookup_fmap_Some_1/g
+s/\blist_alter_fmap\b/list_fmap_alter/g
+s/\blist_alter_fmap_mono\b/list_fmap_alter/g
 EOF
 ```
 
diff --git a/stdpp/base.v b/stdpp/base.v
index c604e841dc0743d0611c68e8ab1ff4085a621c32..deca91cd71e933dc7a8a56c7e11773cda2af1b19 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1520,12 +1520,12 @@ Global Hint Mode Elements - ! : typeclass_instances.
 Global Instance: Params (@elements) 3 := {}.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
-Inductive elem_of_list {A} : ElemOf A (list A) :=
-  | elem_of_list_here (x : A) l : x ∈ x :: l
-  | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l.
-Global Existing Instance elem_of_list.
+Inductive list_elem_of {A} : ElemOf A (list A) :=
+  | list_elem_of_here (x : A) l : x ∈ x :: l
+  | list_elem_of_further (x y : A) l : x ∈ l → x ∈ y :: l.
+Global Existing Instance list_elem_of.
 
-Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
+Lemma list_elem_of_In {A} (l : list A) x : x ∈ l ↔ In x l.
 Proof.
   split.
   - induction 1; simpl; auto.
@@ -1539,8 +1539,8 @@ Inductive NoDup {A} : list A → Prop :=
 Lemma NoDup_ListNoDup {A} (l : list A) : NoDup l ↔ List.NoDup l.
 Proof.
   split.
-  - induction 1; constructor; rewrite <-?elem_of_list_In; auto.
-  - induction 1; constructor; rewrite ?elem_of_list_In; auto.
+  - induction 1; constructor; rewrite <-?list_elem_of_In; auto.
+  - induction 1; constructor; rewrite ?list_elem_of_In; auto.
 Qed.
 
 (** Decidability of equality of the carrier set is admissible, but we add it
diff --git a/stdpp/coPset.v b/stdpp/coPset.v
index 31af5b0cf3e4f469a5fc0af078f57e980eda0a9e..9b076821e1cf7766dd38fe3f05b30b99ae858f6e 100644
--- a/stdpp/coPset.v
+++ b/stdpp/coPset.v
@@ -231,13 +231,13 @@ Proof.
       by apply (infinite_is_fresh l), Hl. }
     intros [ll Hll]; rewrite andb_True; split.
     + apply IHl; exists (omap (maybe (~0)) ll); intros i.
-      rewrite elem_of_list_omap; intros; exists (i~0); auto.
+      rewrite list_elem_of_omap; intros; exists (i~0); auto.
     + apply IHr; exists (omap (maybe (~1)) ll); intros i.
-      rewrite elem_of_list_omap; intros; exists (i~1); auto.
+      rewrite list_elem_of_omap; intros; exists (i~1); auto.
   - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
     rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto.
     exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
-      rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver.
+      rewrite elem_of_cons, elem_of_app, !list_elem_of_fmap; naive_solver.
 Qed.
 Global Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
 Proof.
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index ffcf431c6bd94109454df19e98aae599806912d1..c6a404bdc84f63e03fa4fb1a24b03f9cdde2fce7 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1068,7 +1068,7 @@ Lemma elem_of_list_to_map_1 {A} (l : list (K * A)) i x :
   NoDup (l.*1) → (i,x) ∈ l → (list_to_map l : M A) !! i = Some x.
 Proof.
   intros ? Hx; apply elem_of_list_to_map_1'; eauto using NoDup_fmap_fst.
-  intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj'].
+  intros y; revert Hx. rewrite !list_elem_of_lookup; intros [i' Hi'] [j' Hj'].
   cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (l.*1) i;
     by rewrite ?list_lookup_fmap, ?Hi', ?Hj'.
 Qed.
@@ -1090,7 +1090,7 @@ Proof. split; auto using elem_of_list_to_map_1, elem_of_list_to_map_2. Qed.
 Lemma not_elem_of_list_to_map_1 {A} (l : list (K * A)) i :
   i ∉ l.*1 → (list_to_map l : M A) !! i = None.
 Proof.
-  rewrite elem_of_list_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi.
+  rewrite list_elem_of_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi.
   exists (i,x); simpl; auto using elem_of_list_to_map_2.
 Qed.
 Lemma not_elem_of_list_to_map_2 {A} (l : list (K * A)) i :
@@ -1167,7 +1167,7 @@ Proof.
   intros. apply list_to_map_inj; csimpl.
   - apply NoDup_fst_map_to_list.
   - constructor; [|by auto using NoDup_fst_map_to_list].
-    rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
+    rewrite list_elem_of_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
     rewrite elem_of_map_to_list in Hlookup. congruence.
   - by rewrite !list_to_map_to_list.
 Qed.
@@ -1249,13 +1249,13 @@ Proof.
   unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl.
   - destruct (m !! i) as [x|] eqn:?; simplify_eq/=.
     apply elem_of_list_to_map_1'.
-    { intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?).
+    { intros y'; rewrite list_elem_of_omap; intros ([i' x']&Hi'&?).
       by rewrite elem_of_map_to_list in Hi'; simplify_option_eq. }
-    apply elem_of_list_omap; exists (i,x); split;
+    apply list_elem_of_omap; exists (i,x); split;
       [by apply elem_of_map_to_list|by simplify_option_eq].
-  - apply not_elem_of_list_to_map; rewrite elem_of_list_fmap.
+  - apply not_elem_of_list_to_map; rewrite list_elem_of_fmap.
     intros ([i' x]&->&Hi'); simplify_eq/=.
-    rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?).
+    rewrite list_elem_of_omap in Hi'; destruct Hi' as ([j y]&Hj&?).
     rewrite elem_of_map_to_list in Hj; simplify_option_eq.
 Qed.
 
@@ -1426,11 +1426,11 @@ Section set_to_map.
   Proof.
     intros Hinj. assert (∀ x',
       (i, x) ∈ f <$> elements Y → (i, x') ∈ f <$> elements Y → x = x').
-    { intros x'. intros (y&Hx&Hy)%elem_of_list_fmap (y'&Hx'&Hy')%elem_of_list_fmap.
+    { intros x'. intros (y&Hx&Hy)%list_elem_of_fmap (y'&Hx'&Hy')%list_elem_of_fmap.
       rewrite elem_of_elements in Hy, Hy'.
       cut (y = y'); [congruence|]. apply Hinj; auto. by rewrite <-Hx, <-Hx'. }
     unfold set_to_map; rewrite <-elem_of_list_to_map' by done.
-    rewrite elem_of_list_fmap. setoid_rewrite elem_of_elements; naive_solver.
+    rewrite list_elem_of_fmap. setoid_rewrite elem_of_elements; naive_solver.
   Qed.
 End set_to_map.
 
@@ -1449,7 +1449,7 @@ Section map_to_set.
     y ∈ map_to_set (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
   Proof.
     unfold map_to_set; simpl.
-    rewrite elem_of_list_to_set, elem_of_list_fmap. split.
+    rewrite elem_of_list_to_set, list_elem_of_fmap. split.
     - intros ([i x] & ? & ?%elem_of_map_to_list); eauto.
     - intros (i&x&?&?). exists (i,x). by rewrite elem_of_map_to_list.
   Qed.
@@ -1498,13 +1498,13 @@ Proof.
   - intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf.
     + intros ->. eapply Hj, (NoDup_lookup ((i,x) :: map_to_list m).*1).
       * csimpl. apply NoDup_cons_2, NoDup_fst_map_to_list.
-        intros ([??]&?&?%elem_of_map_to_list)%elem_of_list_fmap; naive_solver.
+        intros ([??]&?&?%elem_of_map_to_list)%list_elem_of_fmap; naive_solver.
       * by rewrite list_lookup_fmap, Hj1.
       * by rewrite list_lookup_fmap, Hj2.
     + apply elem_of_map_to_list. rewrite map_to_list_insert by done.
-      by eapply elem_of_list_lookup_2.
+      by eapply list_elem_of_lookup_2.
     + apply elem_of_map_to_list. rewrite map_to_list_insert by done.
-      by eapply elem_of_list_lookup_2.
+      by eapply list_elem_of_lookup_2.
 Qed.
 
 Lemma map_fold_empty {A B} (f : K → A → B → B) (b : B) :
@@ -3923,10 +3923,10 @@ Section kmap.
     assert (∀ x',
       (j, x) ∈ prod_map f id <$> map_to_list m →
       (j, x') ∈ prod_map f id <$> map_to_list m → x = x').
-    { intros x'. rewrite !elem_of_list_fmap.
+    { intros x'. rewrite !list_elem_of_fmap.
       intros [[j' y1] [??]] [[? y2] [??]]; simplify_eq/=.
       by apply (map_to_list_unique m j'). }
-    unfold kmap. rewrite <-elem_of_list_to_map', elem_of_list_fmap by done.
+    unfold kmap. rewrite <-elem_of_list_to_map', list_elem_of_fmap by done.
     setoid_rewrite elem_of_map_to_list'. split.
     - intros [[??] [??]]; naive_solver.
     - intros [? [??]]. eexists (_, _); naive_solver.
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index 01e3bf7a723e287e808fee0e34785e8947ecbdc2..0d004a118fea47069f2b790e957444cc930b1fe9 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -182,7 +182,7 @@ Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, set_size. simpl. rewrite <-!elem_of_elements.
   generalize (elements X). intros [|? l]; intro; simplify_eq/=.
-  rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
+  rewrite (nil_length_inv l), !list_elem_of_singleton by done; congruence.
 Qed.
 Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
 Proof.
@@ -314,8 +314,8 @@ Proof.
   intros ? Hf Hdisj. unfold set_fold; simpl.
   rewrite <-foldr_app. apply (foldr_permutation R f b).
   - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf.
-    + apply elem_of_list_lookup_2 in Hj1. set_solver.
-    + apply elem_of_list_lookup_2 in Hj2. set_solver.
+    + apply list_elem_of_lookup_2 in Hj1. set_solver.
+    + apply list_elem_of_lookup_2 in Hj2. set_solver.
     + intros ->. pose proof (NoDup_elements (X ∪ Y)).
       by eapply Hj, NoDup_lookup.
   - by rewrite elements_disj_union, (comm (++)).
@@ -371,7 +371,7 @@ Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
   x ∈ filter P X ↔ P x ∧ x ∈ X.
 Proof.
   unfold filter, set_filter.
-  by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
+  by rewrite elem_of_list_to_set, list_elem_of_filter, elem_of_elements.
 Qed.
 Global Instance set_unfold_filter (P : A → Prop) `{!∀ x, Decision (P x)} X Q x :
   SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q).
@@ -427,7 +427,7 @@ Section map.
   Lemma elem_of_map (f : A → B) (X : C) y :
     y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
   Proof.
-    unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
+    unfold set_map. rewrite elem_of_list_to_set, list_elem_of_fmap.
     by setoid_rewrite elem_of_elements.
   Qed.
   Global Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) y :
@@ -528,7 +528,7 @@ Section set_omap.
 
   Lemma elem_of_set_omap f X y : y ∈ set_omap f X ↔ ∃ x, x ∈ X ∧ f x = Some y.
   Proof.
-    unfold set_omap. rewrite elem_of_list_to_set, elem_of_list_omap.
+    unfold set_omap. rewrite elem_of_list_to_set, list_elem_of_omap.
     by setoid_rewrite elem_of_elements.
   Qed.
 
diff --git a/stdpp/finite.v b/stdpp/finite.v
index 63f95e1cb5e9ac31199b87f621a759d0ca3a8f90..64b191fec9abac2fbb086d41baa4f3282f724a55 100644
--- a/stdpp/finite.v
+++ b/stdpp/finite.v
@@ -125,7 +125,7 @@ Qed.
 Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
   `{!Inj (=) (=) f} : card A = card B → Surj (=) f.
 Proof.
-  intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
+  intros HAB y. destruct (list_elem_of_fmap_1 f (enum A) y) as (x&?&?); eauto.
   rewrite finite_inj_Permutation; auto using elem_of_enum.
 Qed.
 
@@ -212,8 +212,8 @@ Section enc_finite.
     rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
   Qed.
   Next Obligation.
-    intros x. rewrite elem_of_list_fmap. exists (to_nat x).
-    split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
+    intros x. rewrite list_elem_of_fmap. exists (to_nat x).
+    split; auto. by apply list_elem_of_lookup_2 with (to_nat x), lookup_seq.
   Qed.
   Lemma enc_finite_card : card A = c.
   Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
@@ -232,7 +232,7 @@ Section surjective_finite.
     {| enum := remove_dups (f <$> enum A) |}.
   Next Obligation. apply NoDup_remove_dups. Qed.
   Next Obligation.
-    intros y. rewrite elem_of_remove_dups, elem_of_list_fmap.
+    intros y. rewrite elem_of_remove_dups, list_elem_of_fmap.
     destruct (surj f y). eauto using elem_of_enum.
   Qed.
 End surjective_finite.
@@ -245,7 +245,7 @@ Section bijective_finite.
     {| enum := f <$> enum A |}.
   Next Obligation. apply (NoDup_fmap f), NoDup_enum. Qed.
   Next Obligation.
-    intros b. rewrite elem_of_list_fmap. destruct (surj f b).
+    intros b. rewrite list_elem_of_fmap. destruct (surj f b).
     eauto using elem_of_enum.
   Qed.
 End bijective_finite.
@@ -254,12 +254,12 @@ Global Program Instance option_finite `{Finite A} : Finite (option A) :=
   {| enum := None :: (Some <$> enum A) |}.
 Next Obligation.
   constructor.
-  - rewrite elem_of_list_fmap. by intros (?&?&?).
+  - rewrite list_elem_of_fmap. by intros (?&?&?).
   - apply (NoDup_fmap_2 _); auto using NoDup_enum.
 Qed.
 Next Obligation.
   intros ??? [x|]; [right|left]; auto.
-  apply elem_of_list_fmap. eauto using elem_of_enum.
+  apply list_elem_of_fmap. eauto using elem_of_enum.
 Qed.
 Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
 Proof. unfold card. simpl. by rewrite fmap_length. Qed.
@@ -272,13 +272,13 @@ Proof. done. Qed.
 
 Global Program Instance unit_finite : Finite () := {| enum := [tt] |}.
 Next Obligation. apply NoDup_singleton. Qed.
-Next Obligation. intros []. by apply elem_of_list_singleton. Qed.
+Next Obligation. intros []. by apply list_elem_of_singleton. Qed.
 Lemma unit_card : card unit = 1.
 Proof. done. Qed.
 
 Global Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
 Next Obligation.
-  constructor; [ by rewrite elem_of_list_singleton | apply NoDup_singleton ].
+  constructor; [ by rewrite list_elem_of_singleton | apply NoDup_singleton ].
 Qed.
 Next Obligation. intros [|]; [ left | right; left ]. Qed.
 Lemma bool_card : card bool = 2.
@@ -289,11 +289,11 @@ Global Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :
 Next Obligation.
   intros. apply NoDup_app; split_and?.
   - apply (NoDup_fmap_2 _). by apply NoDup_enum.
-  - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
+  - intro. rewrite !list_elem_of_fmap. intros (?&?&?) (?&?&?); congruence.
   - apply (NoDup_fmap_2 _). by apply NoDup_enum.
 Qed.
 Next Obligation.
-  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
+  intros ?????? [x|y]; rewrite elem_of_app, !list_elem_of_fmap;
     [left|right]; (eexists; split; [done|apply elem_of_enum]).
 Qed.
 Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
@@ -303,14 +303,14 @@ Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type
   {| enum := a ← enum A; (a,.) <$> enum B |}.
 Next Obligation.
   intros A ?????. apply NoDup_bind.
-  - intros a1 a2 [a b] ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
+  - intros a1 a2 [a b] ?? (?&?&_)%list_elem_of_fmap (?&?&_)%list_elem_of_fmap.
     naive_solver.
   - intros a ?. rewrite (NoDup_fmap _). apply NoDup_enum.
   - apply NoDup_enum.
 Qed.
 Next Obligation.
-  intros ?????? [a b]. apply elem_of_list_bind.
-  exists a. eauto using elem_of_enum, elem_of_list_fmap_1.
+  intros ?????? [a b]. apply list_elem_of_bind.
+  exists a. eauto using elem_of_enum, list_elem_of_fmap_2.
 Qed.
 Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
 Proof.
@@ -329,14 +329,14 @@ Global Program Instance vec_finite `{Finite A} n : Finite (vec A n) :=
 Next Obligation.
   intros A ?? n. induction n as [|n IH]; csimpl; [apply NoDup_singleton|].
   apply NoDup_bind.
-  - intros x1 x2 y ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
+  - intros x1 x2 y ?? (?&?&_)%list_elem_of_fmap (?&?&_)%list_elem_of_fmap.
     congruence.
   - intros x ?. rewrite NoDup_fmap by (intros ?; apply vcons_inj_2). done.
   - apply NoDup_enum.
 Qed.
 Next Obligation.
-  intros A ?? n v. induction v as [|x n v IH]; csimpl; [apply elem_of_list_here|].
-  apply elem_of_list_bind. eauto using elem_of_enum, elem_of_list_fmap_1.
+  intros A ?? n v. induction v as [|x n v IH]; csimpl; [apply list_elem_of_here|].
+  apply list_elem_of_bind. eauto using elem_of_enum, list_elem_of_fmap_2.
 Qed.
 Lemma vec_card `{Finite A} n : card (vec A n) = card A ^ n.
 Proof.
@@ -361,12 +361,12 @@ Fixpoint fin_enum (n : nat) : list (fin n) :=
 Global Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
 Next Obligation.
   intros n. induction n; simpl; constructor.
-  - rewrite elem_of_list_fmap. by intros (?&?&?).
+  - rewrite list_elem_of_fmap. by intros (?&?&?).
   - by apply (NoDup_fmap _).
 Qed.
 Next Obligation.
   intros n i. induction i as [|n i IH]; simpl;
-    rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
+    rewrite elem_of_cons, ?list_elem_of_fmap; eauto.
 Qed.
 Lemma fin_card n : card (fin n) = n.
 Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
@@ -377,8 +377,8 @@ Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
 Proof.
   assert {xs : list A | ∀ x, P x ↔ x ∈ xs} as [xs ?].
   { clear x. exists (proj1_sig <$> enum _). intros x. split; intros Hx.
-    - apply elem_of_list_fmap_1_alt with (x ↾ Hx); [apply elem_of_enum|]; done.
-    - apply elem_of_list_fmap in Hx as [[x' Hx'] [-> _]]; done. }
+    - apply list_elem_of_fmap_2' with (x ↾ Hx); [apply elem_of_enum|]; done.
+    - apply list_elem_of_fmap in Hx as [[x' Hx'] [-> _]]; done. }
   destruct (decide (x ∈ xs)); [left | right]; naive_solver.
 Qed. (* <- could be Defined but this lemma will probably not be used for computing *)
 
@@ -410,8 +410,8 @@ Section sig_finite.
     apply NoDup_filter, NoDup_enum.
   Qed.
   Next Obligation.
-    intros p. apply (elem_of_list_fmap_2_inj proj1_sig).
-    rewrite list_filter_sig_filter, elem_of_list_filter.
+    intros p. apply (list_elem_of_fmap_inj proj1_sig).
+    rewrite list_filter_sig_filter, list_elem_of_filter.
     split; [by destruct p | apply elem_of_enum].
   Qed.
   Lemma sig_card : card (sig P) = length (filter P (enum A)).
@@ -450,8 +450,8 @@ Proof.
     l2 !! (fin_to_nat j) = Some x) as [f Hf]%fin_choice.
   { intros i. destruct (lookup_lt_is_Some_2 l1 i)
       as [x Hix]; [apply fin_to_nat_lt|].
-    assert (x ∈ l2) as [j Hjx]%elem_of_list_lookup_1
-      by (by eapply Hl, elem_of_list_lookup_2).
+    assert (x ∈ l2) as [j Hjx]%list_elem_of_lookup_1
+      by (by eapply Hl, list_elem_of_lookup_2).
     exists (nat_to_fin (lookup_lt_Some _ _ _ Hjx)), x.
     by rewrite fin_to_nat_to_fin. }
   destruct (finite_pigeonhole f) as (i1&i2&Hi&Hf'); [by rewrite !fin_card|].
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index bb1a94e772093de93d86ed57f1e7d40b006ffb04..8e03c24b70c76bd97a45b81bcff3abbf2051d2e6 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -539,7 +539,7 @@ Section more_lemmas.
     destruct X as [X]. unfold elements, gmultiset_elements.
     set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl.
     unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
-    rewrite elem_of_list_bind. split.
+    rewrite list_elem_of_bind. split.
     - intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia.
     - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
       exists (x,n); split; [|by apply elem_of_map_to_list].
@@ -567,7 +567,7 @@ Section more_lemmas.
   Proof.
     intros ? Hf. unfold set_fold; simpl.
     rewrite <-foldr_app. apply (foldr_permutation R f b).
-    - intros j1 a1 j2 a2 c ? Ha1%elem_of_list_lookup_2 Ha2%elem_of_list_lookup_2.
+    - intros j1 a1 j2 a2 c ? Ha1%list_elem_of_lookup_2 Ha2%list_elem_of_lookup_2.
       rewrite gmultiset_elem_of_elements in Ha1, Ha2. eauto.
     - rewrite (comm (++)). apply gmultiset_elements_disj_union.
   Qed.
diff --git a/stdpp/hashset.v b/stdpp/hashset.v
index 71fb610486f9dd0069c080a0e65baa6ee720fe5d..4c5566cccbe0a35189d8ea71bba033a4c7869951 100644
--- a/stdpp/hashset.v
+++ b/stdpp/hashset.v
@@ -65,39 +65,39 @@ Proof.
   - intros ? (?&?&?); simplify_map_eq/=.
   - unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
     intros x y. setoid_rewrite lookup_singleton_Some. split.
-    { by intros (?&[? <-]&?); decompose_elem_of_list. }
-    intros ->; eexists [y]. by rewrite elem_of_list_singleton.
+    { by intros (?&[? <-]&?); decompose_list_elem_of. }
+    intros ->; eexists [y]. by rewrite list_elem_of_singleton.
   - unfold elem_of, hashset_elem_of, union, hashset_union.
     intros [m1 Hm1] [m2 Hm2] x; simpl; setoid_rewrite lookup_union_with_Some.
     split.
     { intros (?&[[]|[[]|(l&k&?&?&?)]]&Hx); simplify_eq/=; eauto.
-      rewrite elem_of_list_union in Hx; destruct Hx; eauto. }
+      rewrite list_elem_of_union in Hx; destruct Hx; eauto. }
     intros [(l&?&?)|(k&?&?)].
     + destruct (m2 !! hash x) as [k|]; eauto.
-      exists (list_union l k). rewrite elem_of_list_union. naive_solver.
+      exists (list_union l k). rewrite list_elem_of_union. naive_solver.
     + destruct (m1 !! hash x) as [l|]; eauto 6.
-      exists (list_union l k). rewrite elem_of_list_union. naive_solver.
+      exists (list_union l k). rewrite list_elem_of_union. naive_solver.
   - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
     intros [m1 ?] [m2 ?] x; simpl.
     setoid_rewrite lookup_intersection_with_Some. split.
     { intros (?&(l&k&?&?&?)&Hx); simplify_option_eq.
-      rewrite elem_of_list_intersection in Hx; naive_solver. }
+      rewrite list_elem_of_intersection in Hx; naive_solver. }
     intros [(l&?&?) (k&?&?)]. assert (x ∈ list_intersection l k)
-      by (by rewrite elem_of_list_intersection).
+      by (by rewrite list_elem_of_intersection).
     exists (list_intersection l k); split; [exists l, k|]; split_and?; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
     intros [m1 ?] [m2 ?] x; simpl.
     setoid_rewrite lookup_difference_with_Some. split.
     { intros (l'&[[??]|(l&k&?&?&?)]&Hx); simplify_option_eq;
-        rewrite ?elem_of_list_difference in Hx; naive_solver. }
+        rewrite ?list_elem_of_difference in Hx; naive_solver. }
     intros [(l&?&?) Hm2]; destruct (m2 !! hash x) as [k|] eqn:?; eauto.
     destruct (decide (x ∈ k)); [destruct Hm2; eauto|].
-    assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference).
+    assert (x ∈ list_difference l k) by (by rewrite list_elem_of_difference).
     exists (list_difference l k); split; [right; exists l,k|]; split_and?; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   - unfold elem_of at 2, hashset_elem_of, elements, hashset_elements.
-    intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.
+    intros [m Hm] x; simpl. setoid_rewrite list_elem_of_bind. split.
     { intros ([n l]&Hx&Hn); simpl in *; rewrite elem_of_map_to_list in Hn.
       cut (hash x = n); [intros <-; eauto|].
       eapply (Forall_forall (λ x, hash x = n) l); eauto. eapply Hm; eauto. }
@@ -107,12 +107,12 @@ Proof.
     induction Hm as [|[n l] m' [??] Hm];
       csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
     apply NoDup_app; split_and?; eauto.
-    setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
+    setoid_rewrite list_elem_of_bind; intros x ? ([n' l']&?&?); simpl in *.
     assert (hash x = n ∧ hash x = n') as [??]; subst.
     { split; [eapply (Forall_forall (λ x, hash x = n) l); eauto|].
       eapply (Forall_forall (λ x, hash x = n') l'); eauto.
       rewrite Forall_forall in Hm. eapply (Hm (_,_)); eauto. }
-    destruct Hn; rewrite elem_of_list_fmap; exists (hash x, l'); eauto.
+    destruct Hn; rewrite list_elem_of_fmap; exists (hash x, l'); eauto.
 Qed.
 End hashset.
 
diff --git a/stdpp/infinite.v b/stdpp/infinite.v
index f57dc97070c1508948c8aadc29dae0364dccd2a3..72c9297fdd8d1fb68775d19368998d5a196f4de5 100644
--- a/stdpp/infinite.v
+++ b/stdpp/infinite.v
@@ -14,7 +14,7 @@ Program Definition inj_infinite `{Infinite A} {B}
   Infinite B := {| infinite_fresh := f ∘ fresh ∘ omap g |}.
 Next Obligation.
   intros A ? B f g Hfg xs Hxs; simpl in *.
-  apply (infinite_is_fresh (omap g xs)), elem_of_list_omap; eauto.
+  apply (infinite_is_fresh (omap g xs)), list_elem_of_omap; eauto.
 Qed.
 Next Obligation. solve_proper. Qed.
 
@@ -42,7 +42,7 @@ Section search_infinite.
     revert xs. assert (help : ∀ xs n n',
       Acc (R (filter (.≠ f n') xs)) n → n' < n → Acc (R xs) n).
     { induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia].
-      split; [done|]. apply elem_of_list_filter; naive_solver lia. }
+      split; [done|]. apply list_elem_of_filter; naive_solver lia. }
     intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
     intros n1; constructor; intros n2 [Hn Hs].
     apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto.
@@ -142,7 +142,7 @@ Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
 |}.
 Next Obligation.
   intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
-  apply elem_of_list_fmap. eexists; split; [|done].
+  apply list_elem_of_fmap. eexists; split; [|done].
   unfold fresh. by rewrite replicate_length.
 Qed.
 Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
diff --git a/stdpp/list.v b/stdpp/list.v
index a39ddc8ae4e41bb50872c5bd0b3c6959459f6105..078a96c51d02f0cdc7b1d566175e06f2031afb4e 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -352,7 +352,7 @@ Global Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈
 
 Section list_set.
   Context `{dec : EqDecision A}.
-  Global Instance elem_of_list_dec : RelDecision (∈@{list A}).
+  Global Instance list_elem_of_dec : RelDecision (∈@{list A}).
   Proof using Type*.
    refine (
     fix go x l :=
@@ -1005,12 +1005,12 @@ Proof.
 Qed.
 Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
 Proof. rewrite elem_of_app. tauto. Qed.
-Lemma elem_of_list_singleton x y : x ∈ [y] ↔ x = y.
+Lemma list_elem_of_singleton x y : x ∈ [y] ↔ x = y.
 Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
 Lemma elem_of_reverse_2 x l : x ∈ l → x ∈ reverse l.
 Proof.
   induction 1; rewrite reverse_cons, elem_of_app,
-    ?elem_of_list_singleton; intuition.
+    ?list_elem_of_singleton; intuition.
 Qed.
 Lemma elem_of_reverse x l : x ∈ reverse l ↔ x ∈ l.
 Proof.
@@ -1018,32 +1018,32 @@ Proof.
   intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
 Qed.
 
-Lemma elem_of_list_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x.
+Lemma list_elem_of_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x.
 Proof.
   induction 1 as [|???? IH]; [by exists 0 |].
   destruct IH as [i ?]; auto. by exists (S i).
 Qed.
-Lemma elem_of_list_lookup_total_1 `{!Inhabited A} l x :
+Lemma list_elem_of_lookup_total_1 `{!Inhabited A} l x :
   x ∈ l → ∃ i, i < length l ∧ l !!! i = x.
 Proof.
-  intros [i Hi]%elem_of_list_lookup_1.
+  intros [i Hi]%list_elem_of_lookup_1.
   eauto using lookup_lt_Some, list_lookup_total_correct.
 Qed.
-Lemma elem_of_list_lookup_2 l i x : l !! i = Some x → x ∈ l.
+Lemma list_elem_of_lookup_2 l i x : l !! i = Some x → x ∈ l.
 Proof.
   revert i. induction l; intros [|i] ?; simplify_eq/=; constructor; eauto.
 Qed.
-Lemma elem_of_list_lookup_total_2 `{!Inhabited A} l i :
+Lemma list_elem_of_lookup_total_2 `{!Inhabited A} l i :
   i < length l → l !!! i ∈ l.
-Proof. intros. by eapply elem_of_list_lookup_2, list_lookup_lookup_total_lt. Qed.
-Lemma elem_of_list_lookup l x : x ∈ l ↔ ∃ i, l !! i = Some x.
-Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed.
-Lemma elem_of_list_lookup_total `{!Inhabited A} l x :
+Proof. intros. by eapply list_elem_of_lookup_2, list_lookup_lookup_total_lt. Qed.
+Lemma list_elem_of_lookup l x : x ∈ l ↔ ∃ i, l !! i = Some x.
+Proof. firstorder eauto using list_elem_of_lookup_1, list_elem_of_lookup_2. Qed.
+Lemma list_elem_of_lookup_total `{!Inhabited A} l x :
   x ∈ l ↔ ∃ i, i < length l ∧ l !!! i = x.
 Proof.
-  naive_solver eauto using elem_of_list_lookup_total_1, elem_of_list_lookup_total_2.
+  naive_solver eauto using list_elem_of_lookup_total_1, list_elem_of_lookup_total_2.
 Qed.
-Lemma elem_of_list_split_length l i x :
+Lemma list_elem_of_split_length l i x :
   l !! i = Some x → ∃ l1 l2, l = l1 ++ x :: l2 ∧ i = length l1.
 Proof.
   revert i; induction l as [|y l IH]; intros [|i] Hl; simplify_eq/=.
@@ -1051,11 +1051,11 @@ Proof.
   - destruct (IH _ Hl) as (?&?&?&?); simplify_eq/=.
     eexists (y :: _); eauto.
 Qed.
-Lemma elem_of_list_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
+Lemma list_elem_of_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
 Proof.
-  intros [? (?&?&?&_)%elem_of_list_split_length]%elem_of_list_lookup_1; eauto.
+  intros [? (?&?&?&_)%list_elem_of_split_length]%list_elem_of_lookup_1; eauto.
 Qed.
-Lemma elem_of_list_split_l `{EqDecision A} l x :
+Lemma list_elem_of_split_l `{EqDecision A} l x :
   x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l1.
 Proof.
   induction 1 as [x l|x y l ? IH].
@@ -1065,23 +1065,23 @@ Proof.
   - destruct IH as (l1 & l2 & -> & ?).
     exists (y :: l1), l2. rewrite elem_of_cons. naive_solver.
 Qed.
-Lemma elem_of_list_split_r `{EqDecision A} l x :
+Lemma list_elem_of_split_r `{EqDecision A} l x :
   x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l2.
 Proof.
   induction l as [|y l IH] using rev_ind.
   { by rewrite elem_of_nil. }
   destruct (decide (x = y)) as [->|].
   - exists l, []. rewrite elem_of_nil. naive_solver.
-  - rewrite elem_of_app, elem_of_list_singleton. intros [?| ->]; try done.
+  - rewrite elem_of_app, list_elem_of_singleton. intros [?| ->]; try done.
     destruct IH as (l1 & l2 & -> & ?); auto.
     exists l1, (l2 ++ [y]).
-    rewrite elem_of_app, elem_of_list_singleton, <-(assoc_L (++)). naive_solver.
+    rewrite elem_of_app, list_elem_of_singleton, <-(assoc_L (++)). naive_solver.
 Qed.
 Lemma list_elem_of_insert l i x : i < length l → x ∈ <[i:=x]>l.
-Proof. intros. by eapply elem_of_list_lookup_2, list_lookup_insert_eq. Qed.
+Proof. intros. by eapply list_elem_of_lookup_2, list_lookup_insert_eq. Qed.
 Lemma nth_elem_of l i d : i < length l → nth i l d ∈ l.
 Proof.
-  intros; eapply elem_of_list_lookup_2.
+  intros; eapply list_elem_of_lookup_2.
   destruct (nth_lookup_or_length l i d); [done | by lia].
 Qed.
 
@@ -1130,14 +1130,14 @@ Proof.
   intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH].
   { intros; simplify_eq. }
   intros [|i] [|j] ??; simplify_eq/=; eauto with f_equal;
-    exfalso; eauto using elem_of_list_lookup_2.
+    exfalso; eauto using list_elem_of_lookup_2.
 Qed.
 Lemma NoDup_alt l :
   NoDup l ↔ ∀ i j x, l !! i = Some x → l !! j = Some x → i = j.
 Proof.
   split; eauto using NoDup_lookup.
   induction l as [|x l IH]; intros Hl; constructor.
-  - rewrite elem_of_list_lookup. intros [i ?].
+  - rewrite list_elem_of_lookup. intros [i ?].
     opose proof* (Hl (S i) 0); by auto.
   - apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x').
 Qed.
@@ -1172,7 +1172,7 @@ End no_dup_dec.
 
 (** ** Set operations on lists *)
 Section list_set.
-  Lemma elem_of_list_intersection_with f l k x :
+  Lemma list_elem_of_intersection_with f l k x :
     x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
         x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
   Proof.
@@ -1195,7 +1195,7 @@ Section list_set.
   Qed.
 
   Context `{!EqDecision A}.
-  Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
+  Lemma list_elem_of_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
   Proof.
     split; induction l; simpl; try case_decide;
       rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
@@ -1205,21 +1205,21 @@ Section list_set.
     induction 1; simpl; try case_decide.
     - constructor.
     - done.
-    - constructor; [|done]. rewrite elem_of_list_difference; intuition.
+    - constructor; [|done]. rewrite list_elem_of_difference; intuition.
   Qed.
-  Lemma elem_of_list_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
+  Lemma list_elem_of_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
   Proof.
-    unfold list_union. rewrite elem_of_app, elem_of_list_difference.
+    unfold list_union. rewrite elem_of_app, list_elem_of_difference.
     intuition. case (decide (x ∈ k)); intuition.
   Qed.
   Lemma NoDup_list_union l k : NoDup l → NoDup k → NoDup (list_union l k).
   Proof.
     intros. apply NoDup_app. repeat split.
     - by apply NoDup_list_difference.
-    - intro. rewrite elem_of_list_difference. intuition.
+    - intro. rewrite list_elem_of_difference. intuition.
     - done.
   Qed.
-  Lemma elem_of_list_intersection l k x :
+  Lemma list_elem_of_intersection l k x :
     x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
   Proof.
     split; induction l; simpl; repeat case_decide;
@@ -1229,7 +1229,7 @@ Section list_set.
   Proof.
     induction 1; simpl; try case_decide.
     - constructor.
-    - constructor; [|done]. rewrite elem_of_list_intersection; intuition.
+    - constructor; [|done]. rewrite list_elem_of_intersection; intuition.
     - done.
   Qed.
 End list_set.
@@ -1281,7 +1281,7 @@ Lemma last_Some_elem_of l x :
   last l = Some x → x ∈ l.
 Proof.
   rewrite last_Some. intros [l' ->]. apply elem_of_app. right.
-  by apply elem_of_list_singleton.
+  by apply list_elem_of_singleton.
 Qed.
 
 (** ** Properties of the [head] function *)
@@ -1401,7 +1401,7 @@ Proof. rewrite lookup_take. case_decide; naive_solver lia. Qed.
 
 Lemma elem_of_take x n l : x ∈ take n l ↔ ∃ i, l !! i = Some x ∧ i < n.
 Proof.
-  rewrite elem_of_list_lookup. setoid_rewrite lookup_take_Some. naive_solver.
+  rewrite list_elem_of_lookup. setoid_rewrite lookup_take_Some. naive_solver.
 Qed.
 
 Lemma take_alter_ge f l n i : n ≤ i → take n (alter f i l) = take n l.
@@ -1576,7 +1576,7 @@ Proof.
 Qed.
 Lemma elem_of_replicate n x y : y ∈ replicate n x ↔ y = x ∧ n ≠ 0.
 Proof.
-  rewrite elem_of_list_lookup, Nat.neq_0_lt_0.
+  rewrite list_elem_of_lookup, Nat.neq_0_lt_0.
   setoid_rewrite lookup_replicate; naive_solver eauto with lia.
 Qed.
 Lemma lookup_replicate_1 n x y i :
@@ -2082,7 +2082,7 @@ Qed.
 Lemma elem_of_Permutation l x : x ∈ l ↔ ∃ k, l ≡ₚ x :: k.
 Proof.
   split.
-  - intros [i ?]%elem_of_list_lookup. eexists. by apply delete_Permutation.
+  - intros [i ?]%list_elem_of_lookup. eexists. by apply delete_Permutation.
   - intros [k ->]. by left.
 Qed.
 
@@ -2090,7 +2090,7 @@ Lemma Permutation_cons_inv_r l k x :
   k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
 Proof.
   intros Hk. assert (∃ i, k !! i = Some x) as [i Hi].
-  { apply elem_of_list_lookup. rewrite Hk, elem_of_cons; auto. }
+  { apply list_elem_of_lookup. rewrite Hk, elem_of_cons; auto. }
   exists (take i k), (drop (S i) k). split.
   - by rewrite take_drop_middle.
   - rewrite <-delete_take_drop. apply (inj (x ::.)).
@@ -2174,7 +2174,7 @@ Section filter.
     by rewrite IH.
   Qed.
 
-  Lemma elem_of_list_filter l x : x ∈ filter P l ↔ P x ∧ x ∈ l.
+  Lemma list_elem_of_filter l x : x ∈ filter P l ↔ P x ∧ x ∈ l.
   Proof.
     induction l; simpl; repeat case_decide;
       rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
@@ -2182,7 +2182,7 @@ Section filter.
   Lemma NoDup_filter l : NoDup l → NoDup (filter P l).
   Proof.
     induction 1; simpl; repeat case_decide;
-      rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
+      rewrite ?NoDup_nil, ?NoDup_cons, ?list_elem_of_filter; tauto.
   Qed.
 
   Global Instance filter_Permutation : Proper ((≡ₚ) ==> (≡ₚ)) (filter P).
@@ -2801,8 +2801,8 @@ Lemma lookup_submseteq l k i x :
   ∃ j, k !! j = Some x.
 Proof.
   intros Hsub Hlook.
-  eapply elem_of_list_lookup_1, elem_of_submseteq;
-    eauto using elem_of_list_lookup_2.
+  eapply list_elem_of_lookup_1, elem_of_submseteq;
+    eauto using list_elem_of_lookup_2.
 Qed.
 
 Lemma submseteq_take l i : take i l ⊆+ l.
@@ -2902,7 +2902,7 @@ Lemma NoDup_submseteq l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l ⊆+
 Proof.
   intros Hl. revert k. induction Hl as [|x l Hx ? IH].
   { intros k Hk. by apply submseteq_nil_l. }
-  intros k Hlk. destruct (elem_of_list_split k x) as (l1&l2&?); subst.
+  intros k Hlk. destruct (list_elem_of_split k x) as (l1&l2&?); subst.
   { apply Hlk. by constructor. }
   rewrite <-Permutation_middle. apply submseteq_skip, IH.
   intros y Hy. rewrite elem_of_app.
@@ -2933,13 +2933,13 @@ Lemma singleton_submseteq_l l x :
 Proof.
   split.
   - intros Hsub. eapply elem_of_submseteq; [|done].
-    apply elem_of_list_singleton. done.
-  - intros (l1&l2&->)%elem_of_list_split.
+    apply list_elem_of_singleton. done.
+  - intros (l1&l2&->)%list_elem_of_split.
     apply submseteq_cons_middle, submseteq_nil_l.
 Qed.
 Lemma singleton_submseteq x y :
   [x] ⊆+ [y] ↔ x = y.
-Proof. rewrite singleton_submseteq_l. apply elem_of_list_singleton. Qed.
+Proof. rewrite singleton_submseteq_l. apply list_elem_of_singleton. Qed.
 
 Section submseteq_dec.
   Context `{!EqDecision A}.
@@ -3072,7 +3072,7 @@ Section Forall_Exists.
 
   Lemma Forall_lookup l : Forall P l ↔ ∀ i x, l !! i = Some x → P x.
   Proof.
-    rewrite Forall_forall. setoid_rewrite elem_of_list_lookup. naive_solver.
+    rewrite Forall_forall. setoid_rewrite list_elem_of_lookup. naive_solver.
   Qed.
   Lemma Forall_lookup_total `{!Inhabited A} l :
     Forall P l ↔ ∀ i, i < length l → P (l !!! i).
@@ -3198,7 +3198,7 @@ Section Forall_Exists.
     Forall P l → Forall P (list_difference l k).
   Proof.
     rewrite !Forall_forall.
-    intros ? x; rewrite elem_of_list_difference; naive_solver.
+    intros ? x; rewrite list_elem_of_difference; naive_solver.
   Qed.
   Lemma Forall_list_union `{!EqDecision A} l k :
     Forall P l → Forall P k → Forall P (list_union l k).
@@ -3207,7 +3207,7 @@ Section Forall_Exists.
     Forall P l → Forall P (list_intersection l k).
   Proof.
     rewrite !Forall_forall.
-    intros ? x; rewrite elem_of_list_intersection; naive_solver.
+    intros ? x; rewrite list_elem_of_intersection; naive_solver.
   Qed.
 
   Context {dec : ∀ x, Decision (P x)}.
@@ -4002,7 +4002,7 @@ Section find.
   Proof.
     rewrite eq_None_not_Some, Forall_forall. split.
     - intros Hl x Hx HP. destruct Hl. eauto using list_find_elem_of.
-    - intros HP [[i x] (?%elem_of_list_lookup_2&?&?)%list_find_Some]; naive_solver.
+    - intros HP [[i x] (?%list_elem_of_lookup_2&?&?)%list_find_Some]; naive_solver.
   Qed.
 
   Lemma list_find_app_None l1 l2 :
@@ -4173,26 +4173,29 @@ Section fmap.
   Lemma const_fmap (l : list A) (y : B) :
     (∀ x, f x = y) → f <$> l = replicate (length l) y.
   Proof. intros; induction l; f_equal/=; auto. Qed.
+
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
   Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
-  Lemma list_lookup_fmap_Some l i x :
-    (f <$> l) !! i =  Some x ↔ ∃ y, l !! i = Some y ∧ x = f y.
-  Proof. by rewrite list_lookup_fmap, fmap_Some. Qed.
   Lemma list_lookup_total_fmap `{!Inhabited A, !Inhabited B} l i :
     i < length l → (f <$> l) !!! i = f (l !!! i).
   Proof.
     intros [x Hx]%lookup_lt_is_Some_2.
     by rewrite !list_lookup_total_alt, list_lookup_fmap, Hx.
   Qed.
-  Lemma list_lookup_fmap_inv l i x :
-    (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
-  Proof.
-    intros Hi. rewrite list_lookup_fmap in Hi.
-    destruct (l !! i) eqn:?; simplify_eq/=; eauto.
-  Qed.
+
+  Lemma list_lookup_fmap_Some l i y :
+    (f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x.
+  Proof. rewrite list_lookup_fmap, fmap_Some. naive_solver. Qed.
+  Lemma list_lookup_fmap_Some_1 l i y :
+    (f <$> l) !! i = Some y → ∃ x, y = f x ∧ l !! i = Some x.
+  Proof. by rewrite list_lookup_fmap_Some. Qed.
+  Lemma list_lookup_fmap_Some_2 l i x :
+    l !! i = Some x → (f <$> l) !! i = Some (f x).
+  Proof. rewrite list_lookup_fmap_Some. naive_solver. Qed.
+
   Lemma list_fmap_insert l i x: f <$> <[i:=x]>l = <[i:=f x]>(f <$> l).
   Proof. revert i. by induction l; intros [|i]; f_equal/=. Qed.
-  Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
+  Lemma list_fmap_alter (g : A → A) (h : B → B) l i :
     Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l).
   Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal/=. Qed.
   Lemma list_fmap_delete l i : f <$> (delete i l) = delete i (f <$> l).
@@ -4201,28 +4204,22 @@ Section fmap.
     naive_solver congruence.
   Qed.
 
-  Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
-  Proof. induction 1; csimpl; rewrite elem_of_cons; intuition. Qed.
-  Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
-  Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
-  Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
-  Proof.
-    induction l as [|y l IH]; simpl; inversion_clear 1.
-    - exists y. split; [done | by left].
-    - destruct IH as [z [??]]; [done|]. exists z. split; [done | by right].
-  Qed.
-  Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l.
-  Proof.
-    naive_solver eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
-  Qed.
-  Lemma elem_of_list_fmap_2_inj `{!Inj (=) (=) f} l x : f x ∈ f <$> l → x ∈ l.
+  Lemma list_elem_of_fmap l y : y ∈ f <$> l ↔ ∃ x, y = f x ∧ x ∈ l.
   Proof.
-    intros (y, (E, I))%elem_of_list_fmap_2. by rewrite (inj f) in I.
-  Qed.
-  Lemma elem_of_list_fmap_inj `{!Inj (=) (=) f} l x : f x ∈ f <$> l ↔ x ∈ l.
-  Proof.
-    naive_solver eauto using elem_of_list_fmap_1, elem_of_list_fmap_2_inj.
+    setoid_rewrite list_elem_of_lookup. setoid_rewrite list_lookup_fmap_Some.
+    naive_solver.
   Qed.
+  Lemma list_elem_of_fmap_1 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
+  Proof. by rewrite list_elem_of_fmap. Qed.
+  Lemma list_elem_of_fmap_2 l x : x ∈ l → f x ∈ f <$> l.
+  Proof. rewrite list_elem_of_fmap. naive_solver. Qed.
+  Lemma list_elem_of_fmap_2' l x y : x ∈ l → y = f x → y ∈ f <$> l.
+  Proof. intros ? ->. by apply list_elem_of_fmap_2. Qed.
+
+  Lemma list_elem_of_fmap_inj `{!Inj (=) (=) f} l x : f x ∈ f <$> l ↔ x ∈ l.
+  Proof. rewrite list_elem_of_fmap. naive_solver. Qed.
+  Lemma list_elem_of_fmap_inj_2 `{!Inj (=) (=) f} l x : f x ∈ f <$> l → x ∈ l.
+  Proof. by rewrite list_elem_of_fmap_inj. Qed.
 
   Lemma list_fmap_inj R1 R2 :
     Inj R1 R2 f → Inj (Forall2 R1) (Forall2 R2) (fmap f).
@@ -4248,7 +4245,7 @@ Section fmap.
     NoDup (f <$> l).
   Proof.
     intros Hinj. induction 1 as [|x l ?? IH]; simpl; constructor.
-    - intros [y [Hxy ?]]%elem_of_list_fmap.
+    - intros [y [Hxy ?]]%list_elem_of_fmap.
       apply Hinj in Hxy; [by subst|by constructor..].
     - apply IH. clear- Hinj.
       intros x' y Hx' Hy. apply Hinj; by constructor.
@@ -4257,7 +4254,7 @@ Section fmap.
   Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
   Proof.
     induction l; simpl; inversion_clear 1; constructor; auto.
-    rewrite elem_of_list_fmap in *. naive_solver.
+    rewrite list_elem_of_fmap in *. naive_solver.
   Qed.
   Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
   Proof. apply NoDup_fmap_2_strong. intros ?? _ _. apply (inj f). Qed.
@@ -4327,14 +4324,11 @@ Section ext.
   Qed.
 End ext.
 
-Lemma list_alter_fmap_mono {A} (f : A → A) (g : A → A) l i :
-  Forall (λ x, f (g x) = g (f x)) l → f <$> alter g i l = alter g i (f <$> l).
-Proof. auto using list_alter_fmap. Qed.
 Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
   (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) → NoDup l → NoDup (l.*1).
 Proof.
   intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; constructor.
-  - rewrite elem_of_list_fmap.
+  - rewrite list_elem_of_fmap.
     intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
     rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
   - apply IH. intros. eapply Hunique; rewrite ?elem_of_cons; eauto.
@@ -4364,7 +4358,7 @@ Section omap.
     induction 1 as [|x y l l' Hfg ? IH]; [done|].
     csimpl. rewrite Hfg. destruct (g y); [|done]. by f_equal.
   Qed.
-  Lemma elem_of_list_omap l y : y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y.
+  Lemma list_elem_of_omap l y : y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y.
   Proof.
     split.
     - induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
@@ -4422,7 +4416,7 @@ Section bind.
   Proof. csimpl. by rewrite (right_id_L _ (++)). Qed.
   Lemma bind_app l1 l2 : (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
   Proof. by induction l1; csimpl; rewrite <-?(assoc_L (++)); f_equal. Qed.
-  Lemma elem_of_list_bind (x : B) (l : list A) :
+  Lemma list_elem_of_bind (x : B) (l : list A) :
     x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
   Proof.
     split.
@@ -4449,10 +4443,10 @@ Section bind.
   Proof.
     intros Hinj Hf. induction 1 as [|x l ?? IH]; csimpl; [constructor|].
     apply NoDup_app. split_and!.
-    - eauto 10 using elem_of_list_here.
-    - intros y ? (x'&?&?)%elem_of_list_bind.
-      destruct (Hinj x x' y); auto using elem_of_list_here, elem_of_list_further.
-    - eauto 10 using elem_of_list_further.
+    - eauto 10 using list_elem_of_here.
+    - intros y ? (x'&?&?)%list_elem_of_bind.
+      destruct (Hinj x x' y); auto using list_elem_of_here, list_elem_of_further.
+    - eauto 10 using list_elem_of_further.
   Qed.
 End bind.
 
@@ -4467,11 +4461,11 @@ Section ret_join.
   Proof. by induction ls; f_equal/=. Qed.
   Global Instance join_Permutation : Proper ((≡ₚ@{list A}) ==> (≡ₚ)) mjoin.
   Proof. intros ?? E. by rewrite !list_join_bind, E. Qed.
-  Lemma elem_of_list_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y.
-  Proof. apply elem_of_list_singleton. Qed.
-  Lemma elem_of_list_join (x : A) (ls : list (list A)) :
+  Lemma list_elem_of_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y.
+  Proof. apply list_elem_of_singleton. Qed.
+  Lemma list_elem_of_join (x : A) (ls : list (list A)) :
     x ∈ mjoin ls ↔ ∃ l : list A, x ∈ l ∧ l ∈ ls.
-  Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
+  Proof. by rewrite list_join_bind, list_elem_of_bind. Qed.
   Lemma join_nil (ls : list (list A)) : mjoin ls = [] ↔ Forall (.= []) ls.
   Proof.
     split; [|by induction 1 as [|[|??] ?]].
@@ -4620,12 +4614,12 @@ Section imap.
   Lemma elem_of_lookup_imap_1 l x :
     x ∈ imap f l → ∃ i y, x = f i y ∧ l !! i = Some y.
   Proof.
-    intros [i Hin]%elem_of_list_lookup. rewrite list_lookup_imap in Hin.
+    intros [i Hin]%list_elem_of_lookup. rewrite list_lookup_imap in Hin.
     simplify_option_eq; naive_solver.
   Qed.
   Lemma elem_of_lookup_imap_2 l x i : l !! i = Some x → f i x ∈ imap f l.
   Proof.
-    intros Hl. rewrite elem_of_list_lookup.
+    intros Hl. rewrite list_elem_of_lookup.
     exists i. by rewrite list_lookup_imap, Hl.
   Qed.
   Lemma elem_of_lookup_imap l x :
@@ -4644,63 +4638,63 @@ Section permutations.
   Lemma interleave_Permutation x l l' : l' ∈ interleave x l → l' ≡ₚ x :: l.
   Proof.
     revert l'. induction l as [|y l IH]; intros l'; simpl.
-    - rewrite elem_of_list_singleton. by intros ->.
-    - rewrite elem_of_cons, elem_of_list_fmap. intros [->|[? [-> H]]]; [done|].
+    - rewrite list_elem_of_singleton. by intros ->.
+    - rewrite elem_of_cons, list_elem_of_fmap. intros [->|[? [-> H]]]; [done|].
       rewrite (IH _ H). constructor.
   Qed.
   Lemma permutations_refl l : l ∈ permutations l.
   Proof.
-    induction l; simpl; [by apply elem_of_list_singleton|].
-    apply elem_of_list_bind. eauto using interleave_cons.
+    induction l; simpl; [by apply list_elem_of_singleton|].
+    apply list_elem_of_bind. eauto using interleave_cons.
   Qed.
   Lemma permutations_skip x l l' :
     l ∈ permutations l' → x :: l ∈ permutations (x :: l').
-  Proof. intro. apply elem_of_list_bind; eauto using interleave_cons. Qed.
+  Proof. intro. apply list_elem_of_bind; eauto using interleave_cons. Qed.
   Lemma permutations_swap x y l : y :: x :: l ∈ permutations (x :: y :: l).
   Proof.
-    simpl. apply elem_of_list_bind. exists (y :: l). split; simpl.
+    simpl. apply list_elem_of_bind. exists (y :: l). split; simpl.
     - destruct l; csimpl; rewrite !elem_of_cons; auto.
-    - apply elem_of_list_bind. simpl.
+    - apply list_elem_of_bind. simpl.
       eauto using interleave_cons, permutations_refl.
   Qed.
   Lemma permutations_nil l : l ∈ permutations [] ↔ l = [].
-  Proof. simpl. by rewrite elem_of_list_singleton. Qed.
+  Proof. simpl. by rewrite list_elem_of_singleton. Qed.
   Lemma interleave_interleave_toggle x1 x2 l1 l2 l3 :
     l1 ∈ interleave x1 l2 → l2 ∈ interleave x2 l3 → ∃ l4,
       l1 ∈ interleave x2 l4 ∧ l4 ∈ interleave x1 l3.
   Proof.
     revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
-    { rewrite !elem_of_list_singleton. intros ? ->. exists [x1].
+    { rewrite !list_elem_of_singleton. intros ? ->. exists [x1].
       change (interleave x2 [x1]) with ([[x2; x1]] ++ [[x1; x2]]).
-      by rewrite (comm (++)), elem_of_list_singleton. }
-    rewrite elem_of_cons, elem_of_list_fmap.
+      by rewrite (comm (++)), list_elem_of_singleton. }
+    rewrite elem_of_cons, list_elem_of_fmap.
     intros Hl1 [? | [l2' [??]]]; simplify_eq/=.
-    - rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
+    - rewrite !elem_of_cons, list_elem_of_fmap in Hl1.
       destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
       + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
       + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
       + exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
-    - rewrite elem_of_cons, elem_of_list_fmap in Hl1.
+    - rewrite elem_of_cons, list_elem_of_fmap in Hl1.
       destruct Hl1 as [? | [l1' [??]]]; subst.
       + exists (x1 :: y :: l3). csimpl.
-        rewrite !elem_of_cons, !elem_of_list_fmap.
+        rewrite !elem_of_cons, !list_elem_of_fmap.
         split; [| by auto]. right. right. exists (y :: l2').
-        rewrite elem_of_list_fmap. naive_solver.
+        rewrite list_elem_of_fmap. naive_solver.
       + destruct (IH l1' l2') as [l4 [??]]; auto. exists (y :: l4). simpl.
-        rewrite !elem_of_cons, !elem_of_list_fmap. naive_solver.
+        rewrite !elem_of_cons, !list_elem_of_fmap. naive_solver.
   Qed.
   Lemma permutations_interleave_toggle x l1 l2 l3 :
     l1 ∈ permutations l2 → l2 ∈ interleave x l3 → ∃ l4,
       l1 ∈ interleave x l4 ∧ l4 ∈ permutations l3.
   Proof.
     revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
-    { rewrite elem_of_list_singleton. intros Hl1 ->. eexists [].
-      by rewrite elem_of_list_singleton. }
-    rewrite elem_of_cons, elem_of_list_fmap.
+    { rewrite list_elem_of_singleton. intros Hl1 ->. eexists [].
+      by rewrite list_elem_of_singleton. }
+    rewrite elem_of_cons, list_elem_of_fmap.
     intros Hl1 [? | [l2' [? Hl2']]]; simplify_eq/=.
-    - rewrite elem_of_list_bind in Hl1.
+    - rewrite list_elem_of_bind in Hl1.
       destruct Hl1 as [l1' [??]]. by exists l1'.
-    - rewrite elem_of_list_bind in Hl1. setoid_rewrite elem_of_list_bind.
+    - rewrite list_elem_of_bind in Hl1. setoid_rewrite list_elem_of_bind.
       destruct Hl1 as [l1' [??]]. destruct (IH l1' l2') as (l1''&?&?); auto.
       destruct (interleave_interleave_toggle y x l1 l1' l1'') as (?&?&?); eauto.
   Qed.
@@ -4708,17 +4702,17 @@ Section permutations.
     l1 ∈ permutations l2 → l2 ∈ permutations l3 → l1 ∈ permutations l3.
   Proof.
     revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
-    - rewrite !elem_of_list_singleton. intros Hl1 ->; simpl in *.
-      by rewrite elem_of_list_singleton in Hl1.
-    - rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
+    - rewrite !list_elem_of_singleton. intros Hl1 ->; simpl in *.
+      by rewrite list_elem_of_singleton in Hl1.
+    - rewrite !list_elem_of_bind. intros Hl1 [l2' [Hl2 Hl2']].
       destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
   Qed.
   Lemma permutations_Permutation l l' : l' ∈ permutations l ↔ l ≡ₚ l'.
   Proof.
     split.
     - revert l'. induction l; simpl; intros l''.
-      + rewrite elem_of_list_singleton. by intros ->.
-      + rewrite elem_of_list_bind. intros [l' [Hl'' ?]].
+      + rewrite list_elem_of_singleton. by intros ->.
+      + rewrite list_elem_of_bind. intros [l' [Hl'' ?]].
         rewrite (interleave_Permutation _ _ _ Hl''). constructor; auto.
     - induction 1; eauto using permutations_refl,
         permutations_skip, permutations_swap, permutations_trans.
@@ -4796,8 +4790,8 @@ Lemma foldr_comm_acc_strong {A B} (R : relation B) `{!PreOrder R}
   R (foldr f (g b) l) (g (foldr f b l)).
 Proof.
   intros ? Hcomm. induction l as [|x l IH]; simpl; [done|].
-  rewrite <-Hcomm by eauto using elem_of_list_here.
-  by rewrite IH by eauto using elem_of_list_further.
+  rewrite <-Hcomm by eauto using list_elem_of_here.
+  by rewrite IH by eauto using list_elem_of_further.
 Qed.
 Lemma foldr_comm_acc {A} (f : A → A → A) (g : A → A) (a : A) l :
   (∀ x y, f x (g y) = g (f x y)) →
@@ -4994,14 +4988,14 @@ Section zip_with.
   Lemma elem_of_lookup_zip_with_1 l k (z : C) :
     z ∈ zip_with f l k → ∃ i x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
   Proof.
-    intros [i Hin]%elem_of_list_lookup. rewrite lookup_zip_with in Hin.
+    intros [i Hin]%list_elem_of_lookup. rewrite lookup_zip_with in Hin.
     simplify_option_eq; naive_solver.
   Qed.
 
   Lemma elem_of_lookup_zip_with_2 l k x y (z : C) i :
     l !! i = Some x → k !! i = Some y → f x y ∈ zip_with f l k.
   Proof.
-    intros Hl Hk. rewrite elem_of_list_lookup.
+    intros Hl Hk. rewrite list_elem_of_lookup.
     exists i. by rewrite lookup_zip_with, Hl, Hk.
   Qed.
 
@@ -5016,7 +5010,7 @@ Section zip_with.
     z ∈ zip_with f l k → ∃ x y, z = f x y ∧ x ∈ l ∧ y ∈ k.
   Proof.
     intros ?%elem_of_lookup_zip_with.
-    naive_solver eauto using elem_of_list_lookup_2.
+    naive_solver eauto using list_elem_of_lookup_2.
   Qed.
 
 End zip_with.
@@ -5326,7 +5320,7 @@ Ltac solve_submseteq :=
   quote_submseteq; apply rlist.eval_submseteq;
   compute_done.
 
-Ltac decompose_elem_of_list := repeat
+Ltac decompose_list_elem_of := repeat
   match goal with
   | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
   | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 50e46d7a0192e303a8e1e961beae5d68edd1ef77..79827e253a804d7a5792d594e936f4c8a52bfd22 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -90,7 +90,7 @@ Section seq.
 
   Lemma elem_of_seq j n k :
     k ∈ seq j n ↔ j ≤ k < j + n.
-  Proof. rewrite elem_of_list_In, in_seq. done. Qed.
+  Proof. rewrite list_elem_of_In, in_seq. done. Qed.
 
   Lemma Forall_seq (P : nat → Prop) i n :
     Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
@@ -188,7 +188,7 @@ Section seqZ.
   Lemma elem_of_seqZ m n k :
     k ∈ seqZ m n ↔ m ≤ k < m + n.
   Proof.
-    rewrite elem_of_list_lookup.
+    rewrite list_elem_of_lookup.
     setoid_rewrite lookup_seqZ. split; [naive_solver lia|].
     exists (Z.to_nat (k - m)). rewrite Z2Nat.id by lia. lia.
   Qed.
@@ -296,8 +296,8 @@ Section max_list.
     destruct (Nat.max_spec n (max_list ns)) as [[? ->]|[? ->]].
     - destruct ns.
       + simpl in *. lia.
-      + by apply elem_of_list_further, IHns.
-    - apply elem_of_list_here.
+      + by apply list_elem_of_further, IHns.
+    - apply list_elem_of_here.
   Qed.
 End max_list.
 
diff --git a/stdpp/listset.v b/stdpp/listset.v
index 8961894dfe731c1c5ce99e0cf5194a61e7cb50e1..3a284e55b99ed05a85e0a137e99c88a44f20c373 100644
--- a/stdpp/listset.v
+++ b/stdpp/listset.v
@@ -21,7 +21,7 @@ Global Instance listset_simple_set : SemiSet A (listset A).
 Proof.
   split.
   - by apply not_elem_of_nil.
-  - by apply elem_of_list_singleton.
+  - by apply list_elem_of_singleton.
   - intros [?] [?]. apply elem_of_app.
 Qed.
 Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
@@ -52,8 +52,8 @@ Local Instance listset_set: Set_ A (listset A).
 Proof.
   split.
   - apply _.
-  - intros [?] [?]. apply elem_of_list_intersection.
-  - intros [?] [?]. apply elem_of_list_difference.
+  - intros [?] [?]. apply list_elem_of_intersection.
+  - intros [?] [?]. apply list_elem_of_difference.
 Qed.
 Global Instance listset_elements: Elements A (listset A) :=
   remove_dups ∘ listset_car.
@@ -77,9 +77,9 @@ Global Instance listset_set_monad : MonadSet listset.
 Proof.
   split.
   - intros. apply _.
-  - intros ??? [?] ?. apply elem_of_list_bind.
-  - intros. apply elem_of_list_ret.
-  - intros ??? [?]. apply elem_of_list_fmap.
+  - intros ??? [?] ?. apply list_elem_of_bind.
+  - intros. apply list_elem_of_ret.
+  - intros ??? [?]. apply list_elem_of_fmap.
   - intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
-    simpl. by rewrite elem_of_list_bind.
+    simpl. by rewrite list_elem_of_bind.
 Qed.
diff --git a/stdpp/listset_nodup.v b/stdpp/listset_nodup.v
index 84f5b476cb8b00c5df4c901dbdf6554c30e0dd48..9ee47fe96f42f34d754fccf8520e3f42890196b7 100644
--- a/stdpp/listset_nodup.v
+++ b/stdpp/listset_nodup.v
@@ -33,10 +33,10 @@ Local Instance listset_nodup_set: Set_ A C.
 Proof.
   split; [split | | ].
   - by apply not_elem_of_nil.
-  - by apply elem_of_list_singleton.
-  - intros [??] [??] ?. apply elem_of_list_union.
-  - intros [??] [??] ?. apply elem_of_list_intersection.
-  - intros [??] [??] ?. apply elem_of_list_difference.
+  - by apply list_elem_of_singleton.
+  - intros [??] [??] ?. apply list_elem_of_union.
+  - intros [??] [??] ?. apply list_elem_of_intersection.
+  - intros [??] [??] ?. apply list_elem_of_difference.
 Qed.
 
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
diff --git a/stdpp/mapset.v b/stdpp/mapset.v
index 689f556dd11be6047720637738cbf8c385fe634b..f7ada6aa8f4aad6ddea6c6a3aa091497f7e60042 100644
--- a/stdpp/mapset.v
+++ b/stdpp/mapset.v
@@ -69,7 +69,7 @@ Proof.
   split.
   - apply _.
   - unfold elements, elem_of at 2, mapset_elements, mapset_elem_of.
-    intros [m] x. simpl. rewrite elem_of_list_fmap. split.
+    intros [m] x. simpl. rewrite list_elem_of_fmap. split.
     + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list.
     + intros. exists (x, ()). by rewrite elem_of_map_to_list.
   - unfold elements, mapset_elements. intros [m]. simpl.
diff --git a/stdpp/relations.v b/stdpp/relations.v
index b8918438138a96ff7d89ec8fd80c256aec1bd285..1b75b206bdd62201f62a5de8ff6711c3de15df85 100644
--- a/stdpp/relations.v
+++ b/stdpp/relations.v
@@ -422,7 +422,7 @@ Section properties.
     revert x xs Hn Hfin.
     induction (lt_wf n) as [n _ IH]; intros x xs -> Hfin.
     constructor; simpl; intros x' Hxx'.
-    assert (x' ∈ xs) as (xs1&xs2&->)%elem_of_list_split by eauto using tc_once.
+    assert (x' ∈ xs) as (xs1&xs2&->)%list_elem_of_split by eauto using tc_once.
     refine (IH (length xs1 + length xs2) _ _ (xs1 ++ xs2) _ _);
       [rewrite app_length; simpl; lia..|].
     intros x'' Hx'x''. opose proof* (Hfin x'') as Hx''; [by econstructor|].
diff --git a/stdpp/sets.v b/stdpp/sets.v
index 7f0fa2d7211dfcd2fb4119ea8b623e14ed56a729..3851988ad719cf68f6fcb3d3480c6e6f51c0b57a 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -303,7 +303,7 @@ Section set_unfold_list.
     (∀ x, SetUnfoldElemOf x l (P x)) →
     SetUnfoldElemOf y (f <$> l) (∃ x, y = f x ∧ P x).
   Proof.
-    constructor. rewrite elem_of_list_fmap. f_equiv; intros x.
+    constructor. rewrite list_elem_of_fmap. f_equiv; intros x.
     by rewrite (set_unfold_elem_of x l (P x)).
   Qed.
   Global Instance set_unfold_rotate x l P n:
@@ -313,7 +313,7 @@ Section set_unfold_list.
   Global Instance set_unfold_list_bind {B} (f : A → list B) l P Q y :
     (∀ x, SetUnfoldElemOf x l (P x)) → (∀ x, SetUnfoldElemOf y (f x) (Q x)) →
     SetUnfoldElemOf y (l ≫= f) (∃ x, Q x ∧ P x).
-  Proof. constructor. rewrite elem_of_list_bind. naive_solver. Qed.
+  Proof. constructor. rewrite list_elem_of_bind. naive_solver. Qed.
 End set_unfold_list.
 
 Tactic Notation "set_unfold" :=
@@ -1128,7 +1128,7 @@ Section pred_finite_infinite.
     intros Hf HP xs. destruct (HP (f <$> xs)) as [x [HPx Hx]].
     destruct (Hf _ HPx) as [y Hf']. exists y. split.
     - simpl. rewrite Hf'. done.
-    - intros Hy. apply Hx. apply elem_of_list_fmap. eauto.
+    - intros Hy. apply Hx. apply list_elem_of_fmap. eauto.
   Qed.
 
   Lemma pred_not_infinite_finite {A} (P : A → Prop) :
@@ -1142,7 +1142,7 @@ Section pred_finite_infinite.
 
   Lemma pred_finite_lt n : pred_finite (flip lt n).
   Proof.
-    exists (seq 0 n); intros i Hi. apply (elem_of_list_lookup_2 _ i).
+    exists (seq 0 n); intros i Hi. apply (list_elem_of_lookup_2 _ i).
     by rewrite lookup_seq.
   Qed.
   Lemma pred_infinite_lt n : pred_infinite (lt n).
@@ -1231,7 +1231,7 @@ Lemma dec_pred_finite_alt {A} (P : A → Prop) `{!∀ x, Decision (P x)} :
   pred_finite P ↔ ∃ xs : list A, ∀ x, P x ↔ x ∈ xs.
 Proof.
   split; intros [xs ?].
-  - exists (filter P xs). intros x. rewrite elem_of_list_filter. naive_solver.
+  - exists (filter P xs). intros x. rewrite list_elem_of_filter. naive_solver.
   - exists xs. naive_solver.
 Qed.
 
@@ -1239,21 +1239,21 @@ Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} :
   pred_finite P.
 Proof.
   exists (proj1_sig <$> enum _). intros x px.
-  apply elem_of_list_fmap_1_alt with (x ↾ px); [apply elem_of_enum|]; done.
+  apply list_elem_of_fmap_2' with (x ↾ px); [apply elem_of_enum|]; done.
 Qed.
 
 Lemma pred_finite_arg2 {A B} (P : A → B → Prop) x :
   pred_finite (uncurry P) → pred_finite (P x).
 Proof.
   intros [xys ?]. exists (xys.*2). intros y ?.
-  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+  apply list_elem_of_fmap_2' with (x, y); by auto.
 Qed.
 
 Lemma pred_finite_arg1 {A B} (P : A → B → Prop) y :
   pred_finite (uncurry P) → pred_finite (flip P y).
 Proof.
   intros [xys ?]. exists (xys.*1). intros x ?.
-  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+  apply list_elem_of_fmap_2' with (x, y); by auto.
 Qed.
 
 (** Sets of sequences of natural numbers *)
diff --git a/stdpp/vector.v b/stdpp/vector.v
index b237a90cebc63f0e370705a154c09220f4fb16ad..1b2efce4373a02bd5a0e843433c4f781796f527d 100644
--- a/stdpp/vector.v
+++ b/stdpp/vector.v
@@ -192,7 +192,7 @@ Qed.
 Lemma elem_of_vlookup {A n} (v : vec A n) x :
   x ∈ vec_to_list v ↔ ∃ i, v !!! i = x.
 Proof.
-  rewrite elem_of_list_lookup. setoid_rewrite <-vlookup_lookup'.
+  rewrite list_elem_of_lookup. setoid_rewrite <-vlookup_lookup'.
   split; [by intros (?&?&?); eauto|]. intros [i Hx].
   exists i, (fin_to_nat_lt _). by rewrite nat_to_fin_to_nat.
 Qed.
diff --git a/stdpp_unstable/bitblast.v b/stdpp_unstable/bitblast.v
index 12313f9dfc53979b025b9fa50fb804b33d268881..68989c1a0f06be6330056a5730fdbe6c03f43095 100644
--- a/stdpp_unstable/bitblast.v
+++ b/stdpp_unstable/bitblast.v
@@ -107,34 +107,34 @@ Proof.
   elim: p => //; csimpl.
   - move => p IH n. rewrite Nat_eqb_eq. case_match; subst.
     + split; [|done] => _. case_match.
-      all: eexists _; split; [by apply elem_of_list_here|] => /=; lia.
+      all: eexists _; split; [by apply list_elem_of_here|] => /=; lia.
     + rewrite {}IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
       * (* r = (pos_to_bit_ranges_aux p).1 *)
         case_bool_decide as Heq; simplify_eq/=.
-        -- eexists _. split; [by apply elem_of_list_here|] => /=. lia.
-        -- eexists _. split. { apply elem_of_list_further. apply elem_of_list_here. }
+        -- eexists _. split; [by apply list_elem_of_here|] => /=. lia.
+        -- eexists _. split. { apply list_elem_of_further. apply list_elem_of_here. }
           simplify_eq/=. lia.
       * (* r ∈ (pos_to_bit_ranges_aux p).2 *)
         case_bool_decide as Heq; simplify_eq/=.
-        -- eexists _. split. { apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+        -- eexists _. split. { apply list_elem_of_further. apply list_elem_of_fmap. by eexists _. }
            simplify_eq/=. lia.
-        -- eexists _. split. { do 2 apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+        -- eexists _. split. { do 2 apply list_elem_of_further. apply list_elem_of_fmap. by eexists _. }
            simplify_eq/=. lia.
-      * eexists _. split; [by apply elem_of_list_here|]. case_bool_decide as Heq; simplify_eq/=; lia.
+      * eexists _. split; [by apply list_elem_of_here|]. case_bool_decide as Heq; simplify_eq/=; lia.
       * case_bool_decide as Heq; simplify_eq/=.
-        -- move: Hin => /= /elem_of_list_fmap[?[??]]; subst. eexists _. split; [by apply elem_of_list_further |].
+        -- move: Hin => /= /list_elem_of_fmap[?[??]]; subst. eexists _. split; [by apply list_elem_of_further |].
            simplify_eq/=. lia.
-        -- rewrite -fmap_cons in Hin. move: Hin => /elem_of_list_fmap[?[??]]; subst. naive_solver lia.
+        -- rewrite -fmap_cons in Hin. move: Hin => /list_elem_of_fmap[?[??]]; subst. naive_solver lia.
   - move => p IH n. case_match; subst.
-    + split; [done|] => -[[l h][/elem_of_cons[?|/(elem_of_list_fmap_2 _ _ _)[[??][??]]]?]]; simplify_eq/=; lia.
+    + split; [done|] => -[[l h][/elem_of_cons[?|/(list_elem_of_fmap _ _ _)[[??][??]]]?]]; simplify_eq/=; lia.
     + rewrite IH. split; move => [r[/elem_of_cons[Heq|Hin] ?]]; simplify_eq/=.
-      * eexists _. split; [by apply elem_of_list_here|] => /=; lia.
-      * eexists _. split. { apply elem_of_list_further. apply elem_of_list_fmap. by eexists _. }
+      * eexists _. split; [by apply list_elem_of_here|] => /=; lia.
+      * eexists _. split. { apply list_elem_of_further. apply list_elem_of_fmap. by eexists _. }
         destruct r; simplify_eq/=. lia.
-      * eexists _. split; [by apply elem_of_list_here|] => /=; lia.
-      * move: Hin => /elem_of_list_fmap[r'[??]]; subst. eexists _. split; [by apply elem_of_list_further|].
+      * eexists _. split; [by apply list_elem_of_here|] => /=; lia.
+      * move: Hin => /list_elem_of_fmap[r'[??]]; subst. eexists _. split; [by apply list_elem_of_further|].
          destruct r'; simplify_eq/=. lia.
-  - move => n. setoid_rewrite elem_of_list_singleton. case_match; split => //; subst; naive_solver lia.
+  - move => n. setoid_rewrite list_elem_of_singleton. case_match; split => //; subst; naive_solver lia.
 Qed.
 
 Definition Z_to_bit_ranges (z : Z) : list (nat * nat) :=
diff --git a/stdpp_unstable/bitvector.v b/stdpp_unstable/bitvector.v
index 175ccf72f2baede9c42b586f9e3583e107b7f494..0c9de52684ee26f18d0bdebb86a627a9e37db9a3 100644
--- a/stdpp_unstable/bitvector.v
+++ b/stdpp_unstable/bitvector.v
@@ -447,7 +447,7 @@ Next Obligation.
   apply bv_eq in Hz. rewrite !Z_to_bv_small in Hz; lia.
 Qed.
 Next Obligation.
-  intros n x. apply elem_of_list_lookup. eexists (Z.to_nat (bv_unsigned x)).
+  intros n x. apply list_elem_of_lookup. eexists (Z.to_nat (bv_unsigned x)).
   rewrite list_lookup_fmap. apply fmap_Some. eexists _.
   pose proof (bv_unsigned_in_range _ x). split.
   - apply lookup_seqZ. split; [done|]. rewrite Z2Nat.id; lia.
@@ -1144,7 +1144,7 @@ Section little.
     rewrite list_lookup_fmap, list_lookup_fmap.
     destruct (Z_to_little_endian m (Z.of_N n) z !! i) eqn: Heq; [simpl |done].
     rewrite Z_to_bv_small; [done|].
-    eapply (Forall_forall (λ z, _ ≤ z < _)); [ |by eapply elem_of_list_lookup_2].
+    eapply (Forall_forall (λ z, _ ≤ z < _)); [ |by eapply list_elem_of_lookup_2].
     eapply Z_to_little_endian_bound; lia.
   Qed.
 
@@ -1155,7 +1155,7 @@ Section little.
     intros ->. apply (inj (fmap bv_unsigned)).
     rewrite bv_to_litte_endian_unsigned; [|lia].
     apply Z_to_little_endian_to_Z; [by rewrite fmap_length | lia |].
-    apply Forall_forall. intros ? [?[->?]]%elem_of_list_fmap_2. apply bv_unsigned_in_range.
+    apply Forall_forall. intros ? [?[->?]]%list_elem_of_fmap. apply bv_unsigned_in_range.
   Qed.
 
   Lemma little_endian_to_bv_to_little_endian m n z:
@@ -1180,7 +1180,7 @@ Section little.
   Proof.
     unfold little_endian_to_bv. rewrite <-(fmap_length bv_unsigned bs).
     apply little_endian_to_Z_bound; [lia|].
-    apply Forall_forall. intros ? [? [-> ?]]%elem_of_list_fmap.
+    apply Forall_forall. intros ? [? [-> ?]]%list_elem_of_fmap.
     apply bv_unsigned_in_range.
   Qed.