diff --git a/algebra/auth.v b/algebra/auth.v
index f9cfc7c35542adb66bc5b586e7ed0d4b5253ada6..c473c83b6c5f5f868a789d489536841fff1810d2 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -127,7 +127,7 @@ Proof.
   - by split; simpl; rewrite ?cmra_core_l.
   - by split; simpl; rewrite ?cmra_core_idemp.
   - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply cmra_core_preserving.
+    by split; simpl; apply cmra_core_mono.
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
    intros n [[[a1|]|] b1] [[[a2|]|] b2];
@@ -222,9 +222,9 @@ Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
 Proof.
   split; try apply _.
   - intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
-      naive_solver eauto using includedN_preserving, validN_preserving.
+      naive_solver eauto using cmra_monotoneN, validN_preserving.
   - by intros [x a] [y b]; rewrite !auth_included /=;
-      intros [??]; split; simpl; apply: included_preserving.
+      intros [??]; split; simpl; apply: cmra_monotone.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
   CofeMor (auth_map f).
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 177c51ec9f91ba22b84a3484fb0f3f00afe5f0ef..a388fc743e13b18b44abb721d60e912c754d373b 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -48,7 +48,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
   mixin_cmra_comm : Comm (≡) (⋅);
   mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
   mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
-  mixin_cmra_pcore_preserving x y cx :
+  mixin_cmra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
   mixin_cmra_extend n x y1 y2 :
@@ -113,9 +113,9 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.
   Lemma cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx.
   Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.
-  Lemma cmra_pcore_preserving x y cx :
+  Lemma cmra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
-  Proof. apply (mixin_cmra_pcore_preserving _ (cmra_mixin A)). Qed.
+  Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
   Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
   Lemma cmra_extend n x y1 y2 :
@@ -217,10 +217,10 @@ Class CMRADiscrete (A : cmraT) := {
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
   validN_preserving n x : ✓{n} x → ✓{n} f x;
-  included_preserving x y : x ≼ y → f x ≼ f y
+  cmra_monotone x y : x ≼ y → f x ≼ f y
 }.
 Arguments validN_preserving {_ _} _ {_} _ _ _.
-Arguments included_preserving {_ _} _ {_} _ _ _.
+Arguments cmra_monotone {_ _} _ {_} _ _ _.
 
 (** * Properties **)
 Section cmra.
@@ -364,18 +364,18 @@ Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
 Lemma cmra_included_r x y : y ≼ x ⋅ y.
 Proof. rewrite (comm op); apply cmra_included_l. Qed.
 
-Lemma cmra_pcore_preserving' x y cx :
+Lemma cmra_pcore_mono' x y cx :
   x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
 Proof.
   intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
-  destruct (cmra_pcore_preserving x y cx') as (cy&->&?); auto.
+  destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
   exists cy; by rewrite Hcx.
 Qed.
-Lemma cmra_pcore_preservingN' n x y cx :
+Lemma cmra_pcore_monoN' n x y cx :
   x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
 Proof.
   intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'.
-  destruct (cmra_pcore_preserving x (x â‹… z) cx')
+  destruct (cmra_pcore_mono x (x â‹… z) cx')
     as (cy&Hxy&?); auto using cmra_included_l.
   assert (pcore y ≡{n}≡ Some cy) as (cy'&?&Hcy')%dist_Some_inv_r'.
   { by rewrite Hy Hxy. }
@@ -384,14 +384,14 @@ Proof.
 Qed.
 Lemma cmra_included_pcore x cx : pcore x = Some cx → cx ≼ x.
 Proof. exists x. by rewrite cmra_pcore_l. Qed.
-Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
+Lemma cmra_monoN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
 Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
-Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
+Lemma cmra_mono_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
 Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
-Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
-Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
-Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
-Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
+Lemma cmra_monoN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
+Proof. by intros; rewrite -!(comm _ z); apply cmra_monoN_l. Qed.
+Lemma cmra_mono_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
+Proof. by intros; rewrite -!(comm _ z); apply cmra_mono_l. Qed.
 
 Lemma cmra_included_dist_l n x1 x2 x1' :
   x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2.
@@ -412,10 +412,10 @@ Section total_core.
   Proof.
     destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_idemp.
   Qed.
-  Lemma cmra_core_preserving x y : x ≼ y → core x ≼ core y.
+  Lemma cmra_core_mono x y : x ≼ y → core x ≼ core y.
   Proof.
     intros; destruct (cmra_total x) as [cx Hcx].
-    destruct (cmra_pcore_preserving x y cx) as (cy&Hcy&?); auto.
+    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
     by rewrite /core /= Hcx Hcy.
   Qed.
 
@@ -461,10 +461,10 @@ Section total_core.
   Proof.
     split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
   Qed.
-  Lemma cmra_core_preservingN n x y : x ≼{n} y → core x ≼{n} core y.
+  Lemma cmra_core_monoN n x y : x ≼{n} y → core x ≼{n} core y.
   Proof.
     intros [z ->].
-    apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
+    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
   Qed.
 End total_core.
 
@@ -519,7 +519,7 @@ Section ucmra.
 
   Global Instance cmra_unit_total : CMRATotal A.
   Proof.
-    intros x. destruct (cmra_pcore_preserving' ∅ x ∅) as (cx&->&?);
+    intros x. destruct (cmra_pcore_mono' ∅ x ∅) as (cx&->&?);
       eauto using ucmra_unit_least, (persistent ∅).
   Qed.
 End ucmra.
@@ -538,7 +538,7 @@ Section cmra_total.
   Context (op_comm : Comm (≡) (@op A _)).
   Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
   Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
-  Context (core_preserving : ∀ x y : A, x ≼ y → core x ≼ core y).
+  Context (core_mono : ∀ x y : A, x ≼ y → core x ≼ core y).
   Context (validN_op_l : ∀ n (x y : A), ✓{n} (x ⋅ y) → ✓{n} x).
   Context (extend : ∀ n (x y1 y2 : A),
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
@@ -551,7 +551,7 @@ Section cmra_total.
     - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
     - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
       case (total cx)=>[ccx ->]; by constructor.
-    - intros x y cx Hxy%core_preserving Hx. move: Hxy.
+    - intros x y cx Hxy%core_mono Hx. move: Hxy.
       rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
   Qed.
 End cmra_total.
@@ -565,16 +565,16 @@ Proof.
   split.
   - apply _. 
   - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
-  - move=> x y Hxy /=. by apply included_preserving, included_preserving.
+  - move=> x y Hxy /=. by apply cmra_monotone, cmra_monotone.
 Qed.
 
 Section cmra_monotone.
   Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}.
   Global Instance cmra_monotone_proper : Proper ((≡) ==> (≡)) f := ne_proper _.
-  Lemma includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y.
+  Lemma cmra_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
   Proof.
     intros [z ->].
-    apply cmra_included_includedN, (included_preserving f), cmra_included_l.
+    apply cmra_included_includedN, (cmra_monotone f), cmra_included_l.
   Qed.
   Lemma valid_preserving x : ✓ x → ✓ f x.
   Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
@@ -677,7 +677,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
   ra_comm : Comm (≡) (⋅);
   ra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
   ra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
-  ra_pcore_preserving x y cx :
+  ra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
   ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x
 }.
@@ -715,7 +715,7 @@ Section ra_total.
   Context (op_comm : Comm (≡) (@op A _)).
   Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
   Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
-  Context (core_preserving : ∀ x y : A, x ≼ y → core x ≼ core y).
+  Context (core_mono : ∀ x y : A, x ≼ y → core x ≼ core y).
   Context (valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x).
   Lemma ra_total_mixin : RAMixin A.
   Proof.
@@ -725,7 +725,7 @@ Section ra_total.
     - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
     - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
       case (total cx)=>[ccx ->]; by constructor.
-    - intros x y cx Hxy%core_preserving Hx. move: Hxy.
+    - intros x y cx Hxy%core_mono Hx. move: Hxy.
       rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
   Qed.
 End ra_total.
@@ -878,8 +878,8 @@ Section prod.
     - intros x y; rewrite prod_pcore_Some prod_pcore_Some'.
       naive_solver eauto using cmra_pcore_idemp.
     - intros x y cx; rewrite prod_included prod_pcore_Some=> -[??] [??].
-      destruct (cmra_pcore_preserving (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
-      destruct (cmra_pcore_preserving (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
+      destruct (cmra_pcore_mono (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
+      destruct (cmra_pcore_mono (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
       exists (z1,z2). by rewrite prod_included prod_pcore_Some.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
     - intros n x y1 y2 [??] [??]; simpl in *.
@@ -942,7 +942,7 @@ Proof.
   split; first apply _.
   - by intros n x [??]; split; simpl; apply validN_preserving.
   - intros x y; rewrite !prod_included=> -[??] /=.
-    by split; apply included_preserving.
+    by split; apply cmra_monotone.
 Qed.
 
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
@@ -1043,7 +1043,7 @@ Section option.
     - intros mx my; setoid_rewrite option_included.
       intros [->|(x&y&->&->&[?|?])]; simpl; eauto.
       + destruct (pcore x) as [cx|] eqn:?; eauto.
-        destruct (cmra_pcore_preserving x y cx) as (?&?&?); eauto 10.
+        destruct (cmra_pcore_mono x y cx) as (?&?&?); eauto 10.
       + destruct (pcore x) as [cx|] eqn:?; eauto.
         destruct (cmra_pcore_proper x y cx) as (?&?&?); eauto 10.
     - intros n [x|] [y|]; rewrite /validN /option_validN /=;
@@ -1102,7 +1102,7 @@ Proof.
   split; first apply _.
   - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
   - intros mx my; rewrite !option_included.
-    intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @included_preserving.
+    intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @cmra_monotone.
     right; exists (f x), (f y). by rewrite {4}Hxy; eauto.
 Qed.
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
diff --git a/algebra/csum.v b/algebra/csum.v
index 341aa6bede821e124e433cfb4cded175515827fc..a1d053517d42620852e5384082054203d5233705 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -202,10 +202,10 @@ Proof.
   - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
     + exists CsumBot. rewrite csum_included; eauto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
-      destruct (cmra_pcore_preserving a a' ca) as (ca'&->&?); auto.
+      destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
       exists (Cinl ca'). rewrite csum_included; eauto 10.
     + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
-      destruct (cmra_pcore_preserving b b' cb) as (cb'&->&?); auto.
+      destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
       exists (Cinr cb'). rewrite csum_included; eauto 10.
   - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
   - intros n [a|b|] y1 y2 Hx Hx'.
@@ -330,7 +330,7 @@ Proof.
   - intros n [a|b|]; simpl; auto using validN_preserving.
   - intros x y; rewrite !csum_included.
     intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
-    eauto 10 using included_preserving.
+    eauto 10 using cmra_monotone.
 Qed.
 
 Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
diff --git a/algebra/dra.v b/algebra/dra.v
index ce053438cce74bb4699c754957398e8a0d03cd2a..059729ff008246b40701209fa586afc270d88133 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -20,7 +20,7 @@ Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
   mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
   mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_preserving x y : 
+  mixin_dra_core_mono x y : 
     ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
 }.
 Structure draT := DRAT {
@@ -78,9 +78,9 @@ Section dra_mixin.
   Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
   Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
   Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_preserving x y : 
+  Lemma dra_core_mono x y : 
     ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
-  Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
+  Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
 End dra_mixin.
 
 Record validity (A : draT) := Validity {
@@ -166,7 +166,7 @@ Proof.
       naive_solver eauto using dra_core_l, dra_core_disjoint_l.
   - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
   - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
-    destruct (dra_core_preserving x z) as (z'&Hz').
+    destruct (dra_core_mono x z) as (z'&Hz').
     unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
     { intros (?&?&?); apply Hz'; tauto. }
     + tauto.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 2b074fb799fa5ba4958fd06021ee1314ade1ba68..c0e59099a938be9bfa46d84683d27cbc8e32a458 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -134,7 +134,7 @@ Proof.
   - intros m i. by rewrite lookup_op lookup_core cmra_core_l.
   - intros m i. by rewrite !lookup_core cmra_core_idemp.
   - intros m1 m2; rewrite !lookup_included=> Hm i.
-    rewrite !lookup_core. by apply cmra_core_preserving.
+    rewrite !lookup_core. by apply cmra_core_mono.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
   - intros n m m1 m2 Hm Hm12.
@@ -399,7 +399,7 @@ Proof.
   split; try apply _.
   - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
   - intros m1 m2; rewrite !lookup_included=> Hm i.
-    by rewrite !lookup_fmap; apply: included_preserving.
+    by rewrite !lookup_fmap; apply: cmra_monotone.
 Qed.
 Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
   gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B).
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 06fc17e017ffb67521709121085b8c17e22ad9dd..312017cea454555ce4d2e965ba03bdc6a7e4e26d 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -114,7 +114,7 @@ Section iprod_cmra.
     - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
     - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
     - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
-      by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
+      by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
     - intros n f f1 f2 Hf Hf12.
       set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
@@ -282,7 +282,7 @@ Proof.
   split; first apply _.
   - intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg.
   - intros g1 g2; rewrite !iprod_included_spec=> Hf x.
-    rewrite /iprod_map; apply (included_preserving _), Hf.
+    rewrite /iprod_map; apply (cmra_monotone _), Hf.
 Qed.
 
 Definition iprodC_map `{Finite A} {B1 B2 : A → cofeT}
diff --git a/algebra/list.v b/algebra/list.v
index b4f0803a3bcfe32fd932cdd73a79bb9b71114976..3ab4d27c259f3b75a130ae1163f0814ff01d522b 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -187,7 +187,7 @@ Section cmra.
     - intros l; rewrite list_equiv_lookup=> i.
       by rewrite !list_lookup_core cmra_core_idemp.
     - intros l1 l2; rewrite !list_lookup_included=> Hl i.
-      rewrite !list_lookup_core. by apply cmra_core_preserving.
+      rewrite !list_lookup_core. by apply cmra_core_mono.
     - intros n l1 l2. rewrite !list_lookup_validN.
       setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
     - intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
@@ -374,7 +374,7 @@ Proof.
   - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
     by apply (validN_preserving (fmap f : option A → option B)).
   - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
-    by apply (included_preserving (fmap f : option A → option B)).
+    by apply (cmra_monotone (fmap f : option A → option B)).
 Qed.
 
 Program Definition listURF (F : urFunctor) : urFunctor := {|
diff --git a/algebra/upred.v b/algebra/upred.v
index be93b5991b0ac932cf9de389c7f0b72b56e57277..a8fe0398abf3342910385840c277f2de42a4863b 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -68,7 +68,7 @@ Qed.
 Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
   `{!CMRAMonotone f} (P : uPred M1) :
   uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. naive_solver eauto using uPred_mono, includedN_preserving. Qed.
+Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
 Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed.
 
 Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
@@ -212,7 +212,7 @@ Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
 Next Obligation.
   intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
   apply uPred_mono with (x1 â‹… x3);
-    eauto using cmra_validN_includedN, cmra_preservingN_r, cmra_includedN_le.
+    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
 Qed.
 Next Obligation. naive_solver. Qed.
 Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
@@ -223,7 +223,7 @@ Definition uPred_wand_eq :
 Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Next Obligation.
-  intros M; naive_solver eauto using uPred_mono, @cmra_core_preservingN.
+  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
 Qed.
 Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
 Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
@@ -1038,7 +1038,7 @@ Qed.
 Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
   split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
-  rewrite -(persistent_core a). by apply cmra_core_preservingN.
+  rewrite -(persistent_core a). by apply cmra_core_monoN.
 Qed.
 Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
 Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index b12df6173c90aab79155eb1b6bc57f8bd210b5a0..1590ee7374bdb68b0b5ddd2fb16d1b7f7b28f680 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -109,7 +109,7 @@ Proof.
   - by intros ?; constructor; rewrite /= cmra_core_l.
   - by intros ?; constructor; rewrite /= cmra_core_idemp.
   - intros r1 r2; rewrite !res_included.
-    by intros (?&?&?); split_and!; apply cmra_core_preserving.
+    by intros (?&?&?); split_and!; apply cmra_core_mono.
   - intros n r1 r2 (?&?&?);
       split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
   - intros n r r1 r2 (?&?&?) [???]; simpl in *.
@@ -212,7 +212,7 @@ Proof.
   split; first apply _.
   - intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
   - by intros r1 r2; rewrite !res_included;
-      intros (?&?&?); split_and!; simpl; try apply: included_preserving.
+      intros (?&?&?); split_and!; simpl; try apply: cmra_monotone.
 Qed.
 Definition resC_map {Λ} {A A' : cofeT} {M M' : ucmraT}
     (f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=