diff --git a/theories/collections.v b/theories/collections.v
index 28a8f25b3eeb2cf405414ab52f22432bff71e1ee..b1546e7d5bf52ca804ae78dd8978a84aff63d220 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -346,11 +346,11 @@ Section simple_collection.
   Proof. set_solver. Qed.
   Lemma elem_of_union_r x X Y : x âˆˆ Y â†’ x âˆˆ X âˆª Y.
   Proof. set_solver. Qed.
-  Lemma union_preserving_l X Y1 Y2 : Y1 âŠ† Y2 â†’ X âˆª Y1 âŠ† X âˆª Y2.
+  Lemma union_mono_l X Y1 Y2 : Y1 âŠ† Y2 â†’ X âˆª Y1 âŠ† X âˆª Y2.
   Proof. set_solver. Qed.
-  Lemma union_preserving_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆª Y âŠ† X2 âˆª Y.
+  Lemma union_mono_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆª Y âŠ† X2 âˆª Y.
   Proof. set_solver. Qed.
-  Lemma union_preserving X1 X2 Y1 Y2 : X1 âŠ† X2 â†’ Y1 âŠ† Y2 â†’ X1 âˆª Y1 âŠ† X2 âˆª Y2.
+  Lemma union_mono X1 X2 Y1 Y2 : X1 âŠ† X2 â†’ Y1 âŠ† Y2 â†’ X1 âˆª Y1 âŠ† X2 âˆª Y2.
   Proof. set_solver. Qed.
 
   Global Instance union_idemp : IdemP ((â‰¡) : relation C) (âˆª).
@@ -444,8 +444,8 @@ Section simple_collection.
     by rewrite reverse_cons, union_list_app,
       union_list_singleton, (comm _), IH.
   Qed.
-  Lemma union_list_preserving Xs Ys : Xs âŠ†* Ys â†’ â‹ƒ Xs âŠ† â‹ƒ Ys.
-  Proof. induction 1; simpl; auto using union_preserving. Qed.
+  Lemma union_list_mono Xs Ys : Xs âŠ†* Ys â†’ â‹ƒ Xs âŠ† â‹ƒ Ys.
+  Proof. induction 1; simpl; auto using union_mono. Qed.
   Lemma empty_union_list Xs : â‹ƒ Xs â‰¡ âˆ… â†” Forall (â‰¡ âˆ…) Xs.
   Proof.
     split.
@@ -565,11 +565,11 @@ Section collection.
   Lemma intersection_greatest X Y Z : Z âŠ† X â†’ Z âŠ† Y â†’ Z âŠ† X âˆ© Y.
   Proof. set_solver. Qed.
 
-  Lemma intersection_preserving_l X Y1 Y2 : Y1 âŠ† Y2 â†’ X âˆ© Y1 âŠ† X âˆ© Y2.
+  Lemma intersection_mono_l X Y1 Y2 : Y1 âŠ† Y2 â†’ X âˆ© Y1 âŠ† X âˆ© Y2.
   Proof. set_solver. Qed.
-  Lemma intersection_preserving_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆ© Y âŠ† X2 âˆ© Y.
+  Lemma intersection_mono_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆ© Y âŠ† X2 âˆ© Y.
   Proof. set_solver. Qed.
-  Lemma intersection_preserving X1 X2 Y1 Y2 :
+  Lemma intersection_mono X1 X2 Y1 Y2 :
     X1 âŠ† X2 â†’ Y1 âŠ† Y2 â†’ X1 âˆ© Y1 âŠ† X2 âˆ© Y2.
   Proof. set_solver. Qed.
 
@@ -612,12 +612,12 @@ Section collection.
   Lemma difference_disjoint X Y : X âŠ¥ Y â†’ X âˆ– Y â‰¡ X.
   Proof. set_solver. Qed.
 
-  Lemma difference_preserving X1 X2 Y1 Y2 :
+  Lemma difference_mono X1 X2 Y1 Y2 :
     X1 âŠ† X2 â†’ Y2 âŠ† Y1 â†’ X1 âˆ– Y1 âŠ† X2 âˆ– Y2.
   Proof. set_solver. Qed.
-  Lemma difference_preserving_l X Y1 Y2 : Y2 âŠ† Y1 â†’ X âˆ– Y1 âŠ† X âˆ– Y2.
+  Lemma difference_mono_l X Y1 Y2 : Y2 âŠ† Y1 â†’ X âˆ– Y1 âŠ† X âˆ– Y2.
   Proof. set_solver. Qed.
-  Lemma difference_preserving_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆ– Y âŠ† X2 âˆ– Y.
+  Lemma difference_mono_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆ– Y âŠ† X2 âˆ– Y.
   Proof. set_solver. Qed.
 
   (** Disjointness *)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2d10c3f8225414f52bf3a6ccb7952bab3f5172ad..902c6b0444d9071951d5ff21cdc7f4498b3412b6 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1322,17 +1322,17 @@ Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
 Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
   m2 âŠ¥â‚˜ m3 â†’ m1 âŠ† m3 â†’ m1 âŠ† m2 âˆª m3.
 Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
-Lemma map_union_preserving_l {A} (m1 m2 m3 : M A) : m1 âŠ† m2 â†’ m3 âˆª m1 âŠ† m3 âˆª m2.
+Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 âŠ† m2 â†’ m3 âˆª m1 âŠ† m3 âˆª m2.
 Proof.
   rewrite !map_subseteq_spec. intros ???.
   rewrite !lookup_union_Some_raw. naive_solver.
 Qed.
-Lemma map_union_preserving_r {A} (m1 m2 m3 : M A) :
+Lemma map_union_mono_r {A} (m1 m2 m3 : M A) :
   m2 âŠ¥â‚˜ m3 â†’ m1 âŠ† m2 â†’ m1 âˆª m3 âŠ† m2 âˆª m3.
 Proof.
   intros. rewrite !(map_union_comm _ m3)
     by eauto using map_disjoint_weaken_l.
-  by apply map_union_preserving_l.
+  by apply map_union_mono_l.
 Qed.
 Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) :
   m3 âŠ¥â‚˜ m1 â†’ m3 âŠ¥â‚˜ m2 â†’ m3 âˆª m1 âŠ† m3 âˆª m2 â†’ m1 âŠ† m2.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 773b72e0cef7be13d54631a708fee58dfcbd9864..f30c72519ddbddc8b5214c9a138c24c11e9eec4e 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -288,12 +288,12 @@ Lemma gmultiset_union_subseteq_l X Y : X âŠ† X âˆª Y.
 Proof. intros x. rewrite multiplicity_union. omega. Qed.
 Lemma gmultiset_union_subseteq_r X Y : Y âŠ† X âˆª Y.
 Proof. intros x. rewrite multiplicity_union. omega. Qed.
-Lemma gmultiset_union_preserving X1 X2 Y1 Y2 : X1 âŠ† X2 â†’ Y1 âŠ† Y2 â†’ X1 âˆª Y1 âŠ† X2 âˆª Y2.
+Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 âŠ† X2 â†’ Y1 âŠ† Y2 â†’ X1 âˆª Y1 âŠ† X2 âˆª Y2.
 Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed.
-Lemma gmultiset_union_preserving_l X Y1 Y2 : Y1 âŠ† Y2 â†’ X âˆª Y1 âŠ† X âˆª Y2.
-Proof. intros. by apply gmultiset_union_preserving. Qed.
-Lemma gmultiset_union_preserving_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆª Y âŠ† X2 âˆª Y.
-Proof. intros. by apply gmultiset_union_preserving. Qed.
+Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 âŠ† Y2 â†’ X âˆª Y1 âŠ† X âˆª Y2.
+Proof. intros. by apply gmultiset_union_mono. Qed.
+Lemma gmultiset_union_mono_r X1 X2 Y : X1 âŠ† X2 â†’ X1 âˆª Y âŠ† X2 âˆª Y.
+Proof. intros. by apply gmultiset_union_mono. Qed.
 
 Lemma gmultiset_subset X Y : X âŠ† Y â†’ size X < size Y â†’ X âŠ‚ Y.
 Proof. intros. apply strict_spec_alt; split; naive_solver auto with omega. Qed.