diff --git a/_CoqProject b/_CoqProject
index eb848e99c0ed05a5fff7646346eb6a348eb8c0c8..42e6e96ce7f2688c07946d50d67fb8415f7d87c5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -77,6 +77,7 @@ iris/bi/monpred.v
 iris/bi/embedding.v
 iris/bi/weakestpre.v
 iris/bi/telescopes.v
+iris/bi/lib/cmra.v
 iris/bi/lib/counterexamples.v
 iris/bi/lib/fixpoint.v
 iris/bi/lib/fractional.v
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index d0e87654bf359bdbaf45d007c4fc5f6c2f19de78..4b27896974f6c4ff389ee59231d090c46e344db3 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -637,6 +637,9 @@ Global Instance exclusive_id_free x : Exclusive x → IdFree x.
 Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
 End cmra.
 
+Global Hint Extern 0 (?a ≼ ?a ⋅ _) => apply: cmra_included_l : core.
+Global Hint Extern 0 (?a ≼ _ ⋅ ?a) => apply: cmra_included_r : core.
+
 (** * Properties about CMRAs with a unit element **)
 Section ucmra.
   Context {A : ucmra}.
@@ -667,6 +670,7 @@ Section ucmra.
 End ucmra.
 
 Global Hint Immediate cmra_unit_cmra_total : core.
+Global Hint Extern 0 (ε ≼ _) => apply: ucmra_unit_least : core.
 
 (** * Properties about CMRAs with Leibniz equality *)
 Section cmra_leibniz.
@@ -1380,7 +1384,7 @@ Section option.
       destruct ma as [a|]; [right|by left].
       destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
       destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
-        setoid_subst; eauto using cmra_included_l.
+        setoid_subst; eauto.
     - intros [->|(a&b&->&->&[Hc|[c Hc]])].
       + exists mb. by destruct mb.
       + exists None; by constructor.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 8220fa9810bcee75bf9d93d6046d42679ebd36b5..47b946117291e9ffd323af9745ac527e552590e8 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -199,6 +199,9 @@ Lemma Cinl_included a a' : Cinl a ≼ Cinl a' ↔ a ≼ a'.
 Proof. rewrite csum_included. naive_solver. Qed.
 Lemma Cinr_included b b' : Cinr b ≼ Cinr b' ↔ b ≼ b'.
 Proof. rewrite csum_included. naive_solver. Qed.
+Lemma CsumBot_included x : x ≼ CsumBot.
+Proof. exists CsumBot. by destruct x. Qed.
+(** We register a hint for [CsumBot_included] below. *)
 
 Lemma csum_includedN n x y :
   x ≼{n} y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
@@ -366,6 +369,7 @@ Proof.
 Qed.
 End cmra.
 
+Global Hint Extern 4 (_ ≼ CsumBot) => apply: CsumBot_included : core.
 Global Arguments csumR : clear implicits.
 
 (* Functor *)
diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index cad2ad5b0aa10d4e1c87a73759046b9685c20fec..fd59b3a80f9d7e0300c553bc2d65ced54efd8c1b 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -240,9 +240,10 @@ Section cmra.
   Proof.
       by rewrite {2}/op /dyn_reservation_map_op_instance /dyn_reservation_map_data /= singleton_op left_id_L.
   Qed.
+
   Lemma dyn_reservation_map_data_mono k a b :
     a ≼ b → dyn_reservation_map_data k a ≼ dyn_reservation_map_data k b.
-  Proof. intros [c ->]. rewrite dyn_reservation_map_data_op. apply cmra_included_l. Qed.
+  Proof. intros [c ->]. rewrite dyn_reservation_map_data_op. eauto. Qed.
   Global Instance dyn_reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index 54646d39061617ee363302fe07098796b069f2fa..7ffff44b84966998972e903b6a01eabaf47ad604 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -112,8 +112,12 @@ Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b.
 Proof.
   split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
 Qed.
+Lemma ExclBot_included ea : ea ≼ ExclBot.
+Proof. by exists ExclBot. Qed.
 End excl.
 
+Global Hint Extern 4 (_ ≼ ExclBot) => apply: ExclBot_included : core.
+
 Global Arguments exclO : clear implicits.
 Global Arguments exclR : clear implicits.
 
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 20d6ae2aa2497132ff8adb36cd0c628e1c1d0fa5..4715bdc62f79a0f46bad6b498e933174209f7161 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -346,8 +346,7 @@ Lemma singleton_included_l m i x :
 Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    exists (x â‹…? m' !! i). rewrite -Some_op_opM.
-    split; first done. apply cmra_included_l.
+    exists (x â‹…? m' !! i). rewrite -Some_op_opM. eauto.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
diff --git a/iris/algebra/max_prefix_list.v b/iris/algebra/max_prefix_list.v
index 0b77a925bd805e79702830fd07c83cb76906a91e..fb4e36ad5fa5f1b6f0e1bae1079fbb0f8231c350 100644
--- a/iris/algebra/max_prefix_list.v
+++ b/iris/algebra/max_prefix_list.v
@@ -104,7 +104,7 @@ Section max_prefix_list.
     split.
     - intros. eexists. apply equiv_dist=> n.
       apply to_max_prefix_list_includedN_aux. by apply: cmra_included_includedN.
-    - intros [l ->]. rewrite to_max_prefix_list_app. apply: cmra_included_l.
+    - intros [l ->]. rewrite to_max_prefix_list_app. eauto.
   Qed.
   Lemma to_max_prefix_list_included_L `{!LeibnizEquiv A} l1 l2 :
     to_max_prefix_list l1 ≼ to_max_prefix_list l2 ↔ l1 `prefix_of` l2.
diff --git a/iris/algebra/reservation_map.v b/iris/algebra/reservation_map.v
index 18355e232995502c2f1262582b3352e62a745542..ea300bbf5adb17d9075f2627bc9ad05b19343616 100644
--- a/iris/algebra/reservation_map.v
+++ b/iris/algebra/reservation_map.v
@@ -225,7 +225,7 @@ Section cmra.
   Qed.
   Lemma reservation_map_data_mono k a b :
     a ≼ b → reservation_map_data k a ≼ reservation_map_data k b.
-  Proof. intros [c ->]. rewrite reservation_map_data_op. apply cmra_included_l. Qed.
+  Proof. intros [c ->]. rewrite reservation_map_data_op. eauto. Qed.
   Global Instance reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (reservation_map_data k a) (reservation_map_data k b1) (reservation_map_data k b2).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 303430eb39d97b918385a31521c5e67d6ad74fd2..5add4f59d560053bd2034300086edc42af8d3eb9 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -288,7 +288,7 @@ Section cmra.
   Lemma view_frag_op b1 b2 : â—¯V (b1 â‹… b2) = â—¯V b1 â‹… â—¯V b2.
   Proof. done. Qed.
   Lemma view_frag_mono b1 b2 : b1 ≼ b2 → ◯V b1 ≼ ◯V b2.
-  Proof. intros [c ->]. rewrite view_frag_op. apply cmra_included_l. Qed.
+  Proof. intros [c ->]. rewrite view_frag_op. eauto. Qed.
   Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
   Proof. done. Qed.
   Lemma view_both_core_discarded a b :
@@ -409,7 +409,7 @@ Section cmra.
     split.
     - intros [[[[dqf agf]|] bf]
         [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
-      + split; [left; apply: cmra_included_l|]. apply to_agree_includedN. by exists agf.
+      + split; [eauto|]. apply to_agree_includedN. by exists agf.
       + split; [right; done|]. by apply (inj to_agree).
     - intros [[[? ->]| ->] ->].
       + rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.
@@ -424,8 +424,8 @@ Section cmra.
       + apply equiv_dist=> n.
         by eapply view_auth_dfrac_includedN, cmra_included_includedN.
     - intros [[[dq ->]| ->] ->].
-      + rewrite view_auth_dfrac_op -assoc. apply cmra_included_l.
-      + apply cmra_included_l.
+      + rewrite view_auth_dfrac_op -assoc. eauto.
+      + eauto.
   Qed.
   Lemma view_auth_includedN n a1 a2 b :
     ●V a1 ≼{n} ●V a2 ⋅ ◯V b ↔ a1 ≡{n}≡ a2.
@@ -448,7 +448,7 @@ Section cmra.
     split.
     - intros [xf [_ Hb]]; simpl in *.
       revert Hb; rewrite left_id. by exists (view_frag_proj xf).
-    - intros [bf ->]. rewrite comm view_frag_op -assoc. apply cmra_included_l.
+    - intros [bf ->]. rewrite comm view_frag_op -assoc. eauto.
   Qed.
 
   (** The weaker [view_both_included] lemmas below are a consequence of the
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index ec0f1f863186940d2b6206d9dfe5e3934095fb2c..6059dd538ecde7248185b9d5dd65e7a0b18a7212 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -59,20 +59,8 @@ Section upred.
 
   Section excl.
     Context {A : ofe}.
-    Implicit Types a b : A.
-    Implicit Types x y : excl A.
-
-    Lemma excl_equivI x y :
-      x ≡ y ⊣⊢ match x, y with
-                          | Excl a, Excl b => a ≡ b
-                          | ExclBot, ExclBot => True
-                          | _, _ => False
-                          end.
-    Proof.
-      uPred.unseal. do 2 split.
-      - by destruct 1.
-      - by destruct x, y; try constructor.
-    Qed.
+    Implicit Types x : excl A.
+
     Lemma excl_validI x :
       ✓ x ⊣⊢ if x is ExclBot then False else True.
     Proof. uPred.unseal. by destruct x. Qed.
@@ -132,24 +120,6 @@ Section upred.
     Qed.
   End agree.
 
-  Section csum_ofe.
-    Context {A B : ofe}.
-    Implicit Types a : A.
-    Implicit Types b : B.
-
-    Lemma csum_equivI (x y : csum A B) :
-      x ≡ y ⊣⊢ match x, y with
-                          | Cinl a, Cinl a' => a ≡ a'
-                          | Cinr b, Cinr b' => b ≡ b'
-                          | CsumBot, CsumBot => True
-                          | _, _ => False
-                          end.
-    Proof.
-      uPred.unseal; do 2 split; first by destruct 1.
-        by destruct x, y; try destruct 1; try constructor.
-    Qed.
-  End csum_ofe.
-
   Section csum_cmra.
     Context {A B : cmra}.
     Implicit Types a : A.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 796aa71d55d5fdda77133a7b32ae1d47455a6d7e..5041d5690791cf62c25eebfae9bcbe3b9d8d6192 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -1,5 +1,6 @@
 From iris.bi Require Import derived_laws_later big_op.
 From iris.prelude Require Import options.
+From iris.algebra Require Import excl csum.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (* We enable primitive projections in this file to improve the performance of the Iris proofmode:
@@ -157,6 +158,47 @@ Section internal_eq_derived.
     - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
   Qed.
 
+  Lemma csum_equivI {A B : ofe} (sx sy : csum A B) :
+    sx ≡ sy ⊣⊢
+              match sx, sy with
+               | Cinl x, Cinl y => x ≡ y
+               | Cinr x, Cinr y => x ≡ y
+               | CsumBot, CsumBot => True
+               | _, _ => False
+               end.
+  Proof.
+    apply (anti_symm _).
+    - apply (internal_eq_rewrite' sx sy (λ sy',
+               match sx, sy' with
+               | Cinl x, Cinl y => x ≡ y
+               | Cinr x, Cinr y => x ≡ y
+               | CsumBot, CsumBot => True
+               | _, _ => False
+               end)%I); [solve_proper|auto|].
+      destruct sx; eauto.
+    - destruct sx; destruct sy; eauto;
+      apply f_equivI, _.
+  Qed.
+
+  Lemma excl_equivI {O : ofe} (x y : excl O) :
+    x ≡ y ⊣⊢ match x, y with
+             | Excl a, Excl b => a ≡ b
+             | ExclBot, ExclBot => True
+             | _, _ => False
+             end.
+  Proof.
+    apply (anti_symm _).
+    - apply (internal_eq_rewrite' x y (λ y',
+               match x, y' with
+               | Excl a, Excl b => a ≡ b
+               | ExclBot, ExclBot => True
+               | _, _ => False
+               end)%I); [solve_proper|auto|].
+      destruct x; eauto.
+    - destruct x as [e1|]; destruct y as [e2|]; [|by eauto..].
+      apply f_equivI, _.
+  Qed.
+
   Lemma sig_equivI {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
   Proof.
     apply (anti_symm _).
diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v
new file mode 100644
index 0000000000000000000000000000000000000000..0dddfee15598ba9a5172904853e1c60b5e810d31
--- /dev/null
+++ b/iris/bi/lib/cmra.v
@@ -0,0 +1,137 @@
+From iris.proofmode Require Import proofmode.
+From iris.bi Require Import internal_eq.
+From iris.algebra Require Import cmra csum excl agree.
+From iris.prelude Require Import options.
+
+
+(** Derived [≼] connective on [cmra] elements. This can be defined on
+    any [bi] that has internal equality [≡]. It corresponds to the
+    step-indexed [≼{n}] connective in the [uPred] model. *)
+Definition internal_included `{!BiInternalEq PROP} {A : cmra} (a b : A) : PROP
+  := ∃ c, b ≡ a ⋅ c.
+Global Arguments internal_included {_ _ _} _ _ : simpl never.
+Global Instance: Params (@internal_included) 3 := {}.
+Global Typeclasses Opaque internal_included.
+
+Infix "≼" := internal_included : bi_scope.
+
+
+Section internal_included_laws.
+  Context `{!BiInternalEq PROP}.
+  Implicit Type A B : cmra.
+
+  (* Force implicit argument PROP *)
+  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+  (** Propers *)
+  Global Instance internal_included_nonexpansive A :
+    NonExpansive2 (internal_included (PROP := PROP) (A := A)).
+  Proof. solve_proper. Qed.
+  Global Instance internal_included_proper A :
+    Proper ((≡) ==> (≡) ==> (⊣⊢)) (internal_included (PROP := PROP) (A := A)).
+  Proof. solve_proper. Qed.
+
+  (** Proofmode support *)
+  Global Instance into_pure_internal_included {A} (a b : A) `{!Discrete b} :
+    @IntoPure PROP (a ≼ b) (a ≼ b).
+  Proof. rewrite /IntoPure /internal_included. eauto. Qed.
+
+  Global Instance from_pure_internal_included {A} (a b : A) :
+    @FromPure PROP false (a ≼ b) (a ≼ b).
+  Proof. rewrite /FromPure /= /internal_included. eauto. Qed.
+
+  Global Instance into_exist_internal_included {A} (a b : A) :
+    IntoExist (PROP := PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I (λ x, x).
+  Proof. by rewrite /IntoExist. Qed.
+
+  Global Instance from_exist_internal_included {A} (a b : A) :
+    FromExist (PROP := PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I.
+  Proof. by rewrite /FromExist. Qed.
+
+  Global Instance internal_included_persistent {A} (a b : A) :
+    Persistent (PROP := PROP) (a ≼ b).
+  Proof. rewrite /internal_included. apply _. Qed.
+
+  Global Instance internal_included_absorbing {A} (a b : A) :
+    Absorbing (PROP := PROP) (a ≼ b).
+  Proof. rewrite /internal_included. apply _. Qed.
+
+  (** Simplification lemmas *)
+  Lemma f_homom_includedI {A B} (x y : A) (f : A → B) `{!NonExpansive f} :
+    (* This is a slightly weaker condition than being a [CmraMorphism] *)
+    (∀ c, f x ⋅ f c ≡ f (x ⋅ c)) →
+    (x ≼ y ⊢ f x ≼ f y).
+  Proof.
+    intros f_homom. iDestruct 1 as (z) "Hz".
+    iExists (f z). rewrite f_homom.
+    by iApply f_equivI.
+  Qed.
+
+  Lemma prod_includedI {A B} (x y : A * B) :
+    x ≼ y ⊣⊢ (x.1 ≼ y.1) ∧ (x.2 ≼ y.2).
+  Proof.
+    destruct x as [x1 x2]; destruct y as [y1 y2]; simpl; apply (anti_symm _).
+    - apply bi.exist_elim => [[z1 z2]]. rewrite -pair_op prod_equivI /=.
+      apply bi.and_mono; by eapply bi.exist_intro'.
+    - iIntros "[[%z1 Hz1] [%z2 Hz2]]". iExists (z1, z2).
+      rewrite -pair_op prod_equivI /=. eauto.
+  Qed.
+
+  Lemma option_includedI {A} (mx my : option A) :
+    mx ≼ my ⊣⊢ match mx, my with
+               | Some x, Some y => (x ≼ y) ∨ (x ≡ y)
+               | None, _ => True
+               | Some x, None => False
+               end.
+  Proof.
+    apply (anti_symm _); last first.
+    - destruct mx as [x|]; last (change None with (ε : option A); eauto).
+      destruct my as [y|]; last eauto.
+      iDestruct 1 as "[[%z H]|H]"; iRewrite "H".
+      * iApply f_homom_includedI; eauto.
+      * by iExists None.
+    - destruct mx as [x|]; last eauto.
+      iDestruct 1 as (c) "He". rewrite Some_op_opM option_equivI.
+      destruct my as [y|]; last eauto.
+      iRewrite "He". destruct c; simpl; eauto.
+  Qed.
+
+  Lemma csum_includedI {A B} (sx sy : csum A B) :
+    sx ≼ sy ⊣⊢ match sx, sy with
+               | Cinl x, Cinl y => x ≼ y
+               | Cinr x, Cinr y => x ≼ y
+               | _, CsumBot => True
+               | _, _ => False
+               end.
+  Proof.
+    apply (anti_symm _); last first.
+    - destruct sx as [x|x|]; destruct sy as [y|y|]; eauto;
+      eapply f_homom_includedI; eauto; apply _.
+    - iDestruct 1 as (c) "Hc". rewrite csum_equivI.
+      destruct sx; destruct sy; destruct c; eauto; by iExists _.
+  Qed.
+
+  Lemma excl_includedI {O : ofe} (x y : excl O) :
+    x ≼ y ⊣⊢ match y with
+             | ExclBot => True
+             |  _ => False
+             end.
+  Proof.
+    apply (anti_symm _).
+    - iIntros "[%z Hz]". iStopProof.
+      apply (internal_eq_rewrite' (x ⋅ z) y (λ y',
+               match y' with
+               | ExclBot => True
+               | _ => False
+               end)%I); [solve_proper|apply internal_eq_sym|].
+      destruct x; destruct z; eauto.
+    - destruct y; eauto.
+  Qed.
+
+  Lemma agree_includedI {O : ofe} (x y : agree O) : x ≼ y ⊣⊢ y ≡ x ⋅ y.
+  Proof.
+    apply (anti_symm _); last (iIntros "H"; by iExists _).
+    iIntros "[%c Hc]". iRewrite "Hc". by rewrite assoc agree_idemp.
+  Qed.
+End internal_included_laws.
\ No newline at end of file