diff --git a/CHANGELOG.md b/CHANGELOG.md
index 39e38bb4d6487d66d17f5fcd4e902295dc7896c4..25e3b0cd50efb805ec177dc49d7306cc0a9e5f1e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,6 +49,8 @@ Coq 8.8 and 8.9 are no longer supported.
 - Generalize `omap_insert`, `omap_singleton`, `map_size_insert`, and
   `map_size_delete` to cover the `Some` and `None` case. Add `_Some` and `_None`
   versions of the lemmas for the specific cases.
+- Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes
+  are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -70,6 +72,14 @@ s/\bomap_insert\b/omap_insert_Some/g
 s/\bomap_singleton\b/omap_singleton_Some/g
 s/\bomap_size_insert\b/map_size_insert_None/g
 s/\bomap_size_delete\b/map_size_delete_Some/g
+s/\bNoDup_cons_11\b/NoDup_cons_1_1/g
+s/\bNoDup_cons_12\b/NoDup_cons_1_2/g
+s/\bmap_filter_lookup_Some_11\b/map_filter_lookup_Some_1_1/g
+s/\bmap_filter_lookup_Some_12\b/map_filter_lookup_Some_1_2/g
+s/\bmap_Forall_insert_11\b/map_Forall_insert_1_1/g
+s/\bmap_Forall_insert_12\b/map_Forall_insert_1_2/g
+s/\bmap_Forall_union_11\b/map_Forall_union_1_1/g
+s/\bmap_Forall_union_12\b/map_Forall_union_1_2/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 5fd54b14e1136e467c80b686f2102b9165513d25..95a4aa6ccd64f734a76d216f0364ef0c8af3220f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1264,10 +1264,10 @@ Section map_filter.
       + rewrite Eq, Hm, lookup_insert. naive_solver.
       + by rewrite lookup_insert_ne.
   Qed.
-  Lemma map_filter_lookup_Some_11 m i x :
+  Lemma map_filter_lookup_Some_1_1 m i x :
     filter P m !! i = Some x → m !! i = Some x.
   Proof. apply map_filter_lookup_Some. Qed.
-  Lemma map_filter_lookup_Some_12 m i x :
+  Lemma map_filter_lookup_Some_1_2 m i x :
     filter P m !! i = Some x → P (i,x).
   Proof. apply map_filter_lookup_Some. Qed.
   Lemma map_filter_lookup_Some_2 m i x :
@@ -1393,9 +1393,9 @@ Section map_Forall.
   Lemma map_Forall_impl (Q : K → A → Prop) m :
     map_Forall P m → (∀ i x, P i x → Q i x) → map_Forall Q m.
   Proof. unfold map_Forall; naive_solver. Qed.
-  Lemma map_Forall_insert_11 m i x : map_Forall P (<[i:=x]>m) → P i x.
+  Lemma map_Forall_insert_1_1 m i x : map_Forall P (<[i:=x]>m) → P i x.
   Proof. intros Hm. by apply Hm; rewrite lookup_insert. Qed.
-  Lemma map_Forall_insert_12 m i x :
+  Lemma map_Forall_insert_1_2 m i x :
     m !! i = None → map_Forall P (<[i:=x]>m) → map_Forall P m.
   Proof.
     intros ? Hm j y ?; apply Hm. by rewrite lookup_insert_ne by congruence.
@@ -1406,8 +1406,8 @@ Section map_Forall.
   Lemma map_Forall_insert m i x :
     m !! i = None → map_Forall P (<[i:=x]>m) ↔ P i x ∧ map_Forall P m.
   Proof.
-    naive_solver eauto using map_Forall_insert_11,
-      map_Forall_insert_12, map_Forall_insert_2.
+    naive_solver eauto using map_Forall_insert_1_1,
+      map_Forall_insert_1_2, map_Forall_insert_2.
   Qed.
   Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
   Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
@@ -2073,10 +2073,10 @@ Qed.
 Lemma delete_union {A} (m1 m2 : M A) i :
   delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
 Proof. apply delete_union_with. Qed.
-Lemma map_Forall_union_11 {A} (m1 m2 : M A) P :
+Lemma map_Forall_union_1_1 {A} (m1 m2 : M A) P :
   map_Forall P (m1 ∪ m2) → map_Forall P m1.
 Proof. intros HP i x ?. apply HP, lookup_union_Some_raw; auto. Qed.
-Lemma map_Forall_union_12 {A} (m1 m2 : M A) P :
+Lemma map_Forall_union_1_2 {A} (m1 m2 : M A) P :
   m1 ##ₘ m2 → map_Forall P (m1 ∪ m2) → map_Forall P m2.
 Proof. intros ? HP i x ?. apply HP, lookup_union_Some; auto. Qed.
 Lemma map_Forall_union_2 {A} (m1 m2 : M A) P :
@@ -2086,8 +2086,8 @@ Lemma map_Forall_union {A} (m1 m2 : M A) P :
   m1 ##ₘ m2 →
   map_Forall P (m1 ∪ m2) ↔ map_Forall P m1 ∧ map_Forall P m2.
 Proof.
-  naive_solver eauto using map_Forall_union_11,
-    map_Forall_union_12, map_Forall_union_2.
+  naive_solver eauto using map_Forall_union_1_1,
+    map_Forall_union_1_2, map_Forall_union_2.
 Qed.
 Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
   filter P m ∪ filter (λ v, ¬ P v) m = m.
diff --git a/theories/list.v b/theories/list.v
index 8977f94c3c37815d021b6c983d757161dee5d72d..4222076bb30ad9b23f707e4f4cb813242d8bc10b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -890,9 +890,9 @@ Lemma NoDup_nil : NoDup (@nil A) ↔ True.
 Proof. split; constructor. Qed.
 Lemma NoDup_cons x l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
 Proof. split; [by inversion 1|]. intros [??]. by constructor. Qed.
-Lemma NoDup_cons_11 x l : NoDup (x :: l) → x ∉ l.
+Lemma NoDup_cons_1_1 x l : NoDup (x :: l) → x ∉ l.
 Proof. rewrite NoDup_cons. by intros [??]. Qed.
-Lemma NoDup_cons_12 x l : NoDup (x :: l) → NoDup l.
+Lemma NoDup_cons_1_2 x l : NoDup (x :: l) → NoDup l.
 Proof. rewrite NoDup_cons. by intros [??]. Qed.
 Lemma NoDup_singleton x : NoDup [x].
 Proof. constructor; [apply not_elem_of_nil | constructor]. Qed.
@@ -937,11 +937,11 @@ Section no_dup_dec.
     | [] => left NoDup_nil_2
     | x :: l =>
       match decide_rel (∈) x l with
-      | left Hin => right (λ H, NoDup_cons_11 _ _ H Hin)
+      | left Hin => right (λ H, NoDup_cons_1_1 _ _ H Hin)
       | right Hin =>
         match NoDup_dec l with
         | left H => left (NoDup_cons_2 _ _ Hin H)
-        | right H => right (H ∘ NoDup_cons_12 _ _)
+        | right H => right (H ∘ NoDup_cons_1_2 _ _)
         end
       end
     end.