diff --git a/CHANGELOG.md b/CHANGELOG.md
index e0cf578f7426a2df2ebeb38ea060415828294468..4b290acc607ea8deeb1d72795438d25b6cd30c72 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -44,6 +44,9 @@ Coq 8.13 is no longer supported.
   `x ≼ y`. This changes the statements of some lemmas: `singleton_included`,
   `local_update_valid0`, `local_update_valid`. Also add various new
   `Some_included` lemmas to help deal with these assertions.
+* Add hints for `a ≼ a ⋅ _` / `a ≼ _ ⋅ a` / `ε ≼ _` / `_ ≼ CsumBot` /
+  `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
+  proofs. (by Ike Mulder)
 
 **Changes in `bi`:**
 
@@ -100,7 +103,8 @@ Coq 8.13 is no longer supported.
 * Add missing transitivity, symmetry and reflexivity lemmas about the `↔`, `→`,
   `-∗` and `∗-∗` connectives. (by Ike Mulder)
 * Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q`
-  can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`
+  can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`.
+* Add `≼` connective (`internal_included`) on the BI level. (by Ike Mulder)
 
 **Changes in `proofmode`:**
 
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..bd69ec9a8bb60f1adc8a694ac6a895674102b2d4 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -637,6 +637,12 @@ 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.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+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 +673,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 +1387,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..3a76de3544392250902d61d410b9c73cffa08163 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,10 @@ Proof.
 Qed.
 End cmra.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ 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..b31404a902dd293b2b16ac91206e33f85624fedd 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 ->]. by rewrite dyn_reservation_map_data_op. 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..94b792756e991b665a3763e37f36233dc524f54a 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -112,8 +112,15 @@ 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.
 
+(* We use a [Hint Extern] with [apply:], instead of [Hint Immediate], to invoke
+  the new unification algorithm. The old unification algorithm sometimes gets
+  confused by going from [ucmra]'s to [cmra]'s and back. *)
+Global Hint Extern 0 (_ ≼ 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..58ce801bb6489895dcddc960a612b97d5a5e2d7d 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). by rewrite -Some_op_opM.
   - 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..1be3502ffcdd9a2fc0cbced105b95c6a13609ea5 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 ->]. by rewrite reservation_map_data_op. 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..5392eb6f05d2d9728d16f8c146dbcebd8bdb4e5b 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 ->]. by rewrite view_frag_op. 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.
+      + by rewrite view_auth_dfrac_op -assoc.
+      + done.
   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 ->]. by rewrite comm view_frag_op -assoc.
   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..6a7eca83d87be6eaeb683abc65814efb5a6cb835 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,46 @@ 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..f3a8b9a20f46e2d9f19823c2242b48da1a74daed
--- /dev/null
+++ b/iris/bi/lib/cmra.v
@@ -0,0 +1,152 @@
+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.
+
+  Lemma internal_included_refl `{!CmraTotal A} (x : A) : ⊢@{PROP} x ≼ x.
+  Proof. iExists (core x). by rewrite cmra_core_r. Qed.
+  Lemma internal_included_trans {A} (x y z : A) :
+    ⊢@{PROP} x ≼ y -∗ y ≼ z -∗ x ≼ z.
+  Proof.
+    iIntros "#[%x' Hx'] #[%y' Hy']". iExists (x' â‹… y').
+    rewrite assoc. by iRewrite -"Hx'".
+  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], y as [y1 y2]; simpl; iSplit.
+    - iIntros "#[%z H]". rewrite prod_equivI /=. iDestruct "H" as "[??]".
+      iSplit; by iExists _.
+    - iIntros "#[[%z1 Hz1] [%z2 Hz2]]". iExists (z1, z2).
+      rewrite prod_equivI /=; auto.
+  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.
+    iSplit.
+    - iIntros "[%mz H]". rewrite option_equivI.
+      destruct mx as [x|], my as [y|], mz as [z|]; simpl; auto; [|].
+      + iLeft. by iExists z.
+      + iRight. by iRewrite "H".
+    - destruct mx as [x|], my as [y|]; simpl; auto; [|].
+      + iDestruct 1 as "[[%z H]|H]"; iRewrite "H".
+        * by iExists (Some z).
+        * by iExists None.
+      + iIntros "_". by iExists (Some y).
+  Qed.
+
+  Lemma option_included_totalI `{!CmraTotal A} (mx my : option A) :
+    mx ≼ my ⊣⊢ match mx, my with
+               | Some x, Some y => x ≼ y
+               | None, _ => True
+               | Some x, None => False
+               end.
+  Proof.
+    rewrite option_includedI. destruct mx as [x|], my as [y|]; [|done..].
+    iSplit; [|by auto].
+    iIntros "[Hx|Hx] //". iRewrite "Hx". iApply (internal_included_refl y).
+  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.
+    iSplit.
+    - iDestruct 1 as (sz) "H". rewrite csum_equivI.
+      destruct sx, sy, sz; rewrite /internal_included /=; auto.
+    - destruct sx as [x|x|], sy as [y|y|]; eauto; [|].
+      + iIntros "#[%z H]". iExists (Cinl z). by rewrite csum_equivI.
+      + iIntros "#[%z H]". iExists (Cinr z). by rewrite csum_equivI.
+  Qed.
+
+  Lemma excl_includedI {O : ofe} (x y : excl O) :
+    x ≼ y ⊣⊢ match y with
+             | ExclBot => True
+             |  _ => False
+             end.
+  Proof.
+    iSplit.
+    - iIntros "[%z Hz]". rewrite excl_equivI. destruct y, x, z; auto.
+    - destruct y; [done|]. iIntros "_". by iExists ExclBot.
+  Qed.
+
+  Lemma agree_includedI {O : ofe} (x y : agree O) : x ≼ y ⊣⊢ y ≡ x ⋅ y.
+  Proof.
+    iSplit.
+    + iIntros "[%z Hz]". iRewrite "Hz". by rewrite assoc agree_idemp.
+    + iIntros "H". by iExists _.
+  Qed.
+End internal_included_laws.
\ No newline at end of file