iris/bi/lib/fractional.v

+From iris.bi Require Export bi.
+From iris.proofmode Require Import classes classes_make proofmode.
+From iris.prelude Require Import options.
+
+Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
+  fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
+Global Arguments Fractional {_} _%_I : simpl never.
+Global Arguments fractional {_ _ _} _ _.
+
+(** The [AsFractional] typeclass eta-expands a proposition [P] into [Φ q] such
+that [Φ] is a fractional predicate. This is needed because higher-order
+unification cannot be relied upon to guess the right [Φ].
+
+[AsFractional] should generally be used in APIs that work with fractional
+predicates (instead of [Fractional]): when the user provides the original
+resource [P], have a premise [AsFractional P Φ 1] to convert that into some
+fractional predicate.
+
+The equivalence in [as_fractional] should hold definitionally; various typeclass
+instances assume that [Φ q] will un-do the eta-expansion performed by
+[AsFractional]. *)
+Class AsFractional {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
+  as_fractional : P ⊣⊢ Φ q;
+  as_fractional_fractional : Fractional Φ
+}.
+Global Arguments AsFractional {_} _%_I _%_I _%_Qp.
+Global Hint Mode AsFractional - ! - - : typeclass_instances.
+
+(** The class [FrameFractionalQp] is used for fractional framing, it subtracts
+the fractional of the hypothesis from the goal: it computes [r := qP - qR].
+See [frame_fractional] for how it is used. *)
+Class FrameFractionalQp (qR qP r : Qp) :=
+  frame_fractional_qp : qP = (qR + r)%Qp.
+Global Hint Mode FrameFractionalQp ! ! - : typeclass_instances.
+
+Section fractional.
+  Context {PROP : bi}.
+  Implicit Types P Q : PROP.
+  Implicit Types Φ : Qp → PROP.
+  Implicit Types q : Qp.
+
+  Global Instance Fractional_proper :
+    Proper (pointwise_relation _ (≡) ==> iff) (@Fractional PROP).
+  Proof.
+    rewrite /Fractional.
+    intros Φ1 Φ2 Hequiv.
+    by setoid_rewrite Hequiv.
+  Qed.
+
+  (* Every [Fractional] predicate admits an obvious [AsFractional] instance.
+
+  Ideally, this instance would mean that a user never has to define a manual
+  [AsFractional] instance for a [Fractional] predicate (even if it's of the
+  form [λ q, Φ a1 ‥ q ‥ an] for some n-ary predicate [Φ].) However, Coq's
+  lack of guarantees for higher-order unification mean this instance wouldn't
+  guarantee to apply for every [AsFractional] goal.
+
+  Therefore, this instance is not global to avoid conflicts with existing instances
+  defined by our users, since we can't ask users to universally delete their
+  manually-defined [AsFractional] instances for their own [Fractional] predicates.
+
+  (We could just support this instance for predicates with the fractional argument
+  in the final position, but that was felt to be a bit of a foot-gun - users would
+  have to remember to *not* define an [AsFractional] some of the time.) *)
+  Local Instance fractional_as_fractional Φ q :
+    Fractional Φ → AsFractional (Φ q) Φ q.
+  Proof. done. Qed.
+
+  (** This lemma is meant to be used when [P] is known. But really you should be
+   using [iDestruct "H" as "[H1 H2]"], which supports splitting at fractions. *)
+  Lemma fractional_split P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) →
+    P ⊣⊢ Φ q1 ∗ Φ q2.
+  Proof. by move=>-[-> ->]. Qed.
+  (** This lemma is meant to be used when [P] is known. But really you should be
+   using [iDestruct "H" as "[H1 H2]"], which supports halving fractions. *)
+  Lemma fractional_half P Φ q :
+    AsFractional P Φ q →
+    P ⊣⊢ Φ (q/2)%Qp ∗ Φ (q/2)%Qp.
+  Proof. by rewrite -{1}(Qp.div_2 q)=>-[->->]. Qed.
+  (** This lemma is meant to be used when [P1], [P2] are known. But really you
+   should be using [iCombine "H1 H2" as "H"] (for forwards reasoning) or
+   [iSplitL]/[iSplitR] (for goal-oriented reasoning), which support merging
+   fractions. *)
+  Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    P1 ∗ P2 ⊣⊢ Φ (q1 + q2)%Qp.
+  Proof. move=>-[-> _] [-> _]. rewrite fractional //. Qed.
+
+  (** Fractional and logical connectives *)
+  Global Instance persistent_fractional (P : PROP) :
+    Persistent P → TCOr (Affine P) (Absorbing P) → Fractional (λ _, P).
+  Proof. intros ?? q q'. apply: bi.persistent_sep_dup. Qed.
+
+  (** We do not have [AsFractional] instances for [∗] and the big operators
+  because the [iDestruct] tactic already turns [P ∗ Q] into [P] and [Q],
+  [[∗ list] k↦x ∈ y :: l, Φ k x] into [Φ 0 i] and [[∗ list] k↦x ∈ l, Φ (S k) x],
+  etc. Hence, an [AsFractional] instance would cause ambiguity because for
+  example [l ↦{1} v ∗ l' ↦{1} v'] could be turned into [l ↦{1} v] and
+  [l' ↦{1} v'], or into two times [l ↦{1/2} v ∗ l' ↦{1/2} v'].
+
+  We do provide the [Fractional] instances so that when one defines a derived
+  connection in terms of [∗] or a big operator (and makes that opaque in some
+  way), one could choose to split along the [∗] or along the fraction. *)
+  Global Instance fractional_sep Φ Ψ :
+    Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
+  Proof.
+    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
+    rewrite !assoc. f_equiv. by rewrite comm.
+  Qed.
+
+  Global Instance fractional_embed `{!BiEmbed PROP PROP'} Φ :
+    Fractional Φ → Fractional (λ q, ⎡ Φ q ⎤ : PROP')%I.
+  Proof. intros ???. by rewrite fractional embed_sep. Qed.
+
+  Global Instance as_fractional_embed `{!BiEmbed PROP PROP'} P Φ q :
+    AsFractional P Φ q → AsFractional (⎡ P ⎤) (λ q, ⎡ Φ q ⎤)%I q.
+  Proof. intros [??]; split; [by f_equiv|apply _]. Qed.
+
+  Global Instance fractional_big_sepL {A} (l : list A) Ψ :
+    (∀ k x, Fractional (Ψ k x)) →
+    Fractional (PROP:=PROP) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
+  Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed.
+
+  Global Instance fractional_big_sepL2 {A B} (l1 : list A) (l2 : list B) Ψ :
+    (∀ k x1 x2, Fractional (Ψ k x1 x2)) →
+    Fractional (PROP:=PROP) (λ q, [∗ list] k↦x1; x2 ∈ l1; l2, Ψ k x1 x2 q)%I.
+  Proof. intros ? q q'. rewrite -big_sepL2_sep. by setoid_rewrite fractional. Qed.
+
+  Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
+    (∀ k x, Fractional (Ψ k x)) →
+    Fractional (PROP:=PROP) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I.
+  Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
+
+  Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
+    (∀ x, Fractional (Ψ x)) →
+    Fractional (PROP:=PROP) (λ q, [∗ set] x ∈ X, Ψ x q)%I.
+  Proof. intros ? q q'. rewrite -big_sepS_sep. by setoid_rewrite fractional. Qed.
+
+  Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
+    (∀ x, Fractional (Ψ x)) →
+    Fractional (PROP:=PROP) (λ q, [∗ mset] x ∈ X, Ψ x q)%I.
+  Proof. intros ? q q'. rewrite -big_sepMS_sep. by setoid_rewrite fractional. Qed.
+
+  (** Proof mode instances *)
+  Global Instance from_sep_fractional P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) → FromSep P (Φ q1) (Φ q2).
+  Proof. rewrite /FromSep=>-[-> ->] //. Qed.
+  Global Instance combine_sep_as_fractional P1 P2 Φ q1 q2 :
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    CombineSepAs P1 P2 (Φ (q1 + q2)%Qp) | 50.
+  (* Explicit cost, to make it easier to provide instances with higher or
+     lower cost. Higher-cost instances exist to combine (for example)
+     [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
+  Proof. rewrite /CombineSepAs =>-[-> _] [-> <-] //. Qed.
+
+  Global Instance from_sep_fractional_half P Φ q :
+    AsFractional P Φ q → FromSep P (Φ (q / 2)%Qp) (Φ (q / 2)%Qp) | 10.
+  Proof. rewrite /FromSep -{1}(Qp.div_2 q). intros [-> <-]. rewrite Qp.div_2 //. Qed.
+  Global Instance combine_sep_as_fractional_half P Φ q :
+    AsFractional P Φ (q/2) → CombineSepAs P P (Φ q) | 50.
+  (* Explicit cost, to make it easier to provide instances with higher or
+     lower cost. Higher-cost instances exist to combine (for example)
+     [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
+  Proof. rewrite /CombineSepAs=>-[-> <-]. by rewrite Qp.div_2. Qed.
+
+  Global Instance into_sep_fractional P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) → IntoSep P (Φ q1) (Φ q2).
+  Proof. intros [??]. rewrite /IntoSep [P]fractional_split //. Qed.
+
+  Global Instance into_sep_fractional_half P Φ q :
+    AsFractional P Φ q → IntoSep P (Φ (q / 2)%Qp) (Φ (q / 2)%Qp) | 100.
+  Proof. intros [??]. rewrite /IntoSep [P]fractional_half //. Qed.
+
+  Global Instance frame_fractional_qp_add_l q q' : FrameFractionalQp q (q + q') q'.
+  Proof. by rewrite /FrameFractionalQp. Qed.
+  Global Instance frame_fractional_qp_add_r q q' : FrameFractionalQp q' (q + q') q.
+  Proof. by rewrite /FrameFractionalQp Qp.add_comm. Qed.
+  Global Instance frame_fractional_qp_half q : FrameFractionalQp (q/2) q (q/2).
+  Proof. by rewrite /FrameFractionalQp Qp.div_2. Qed.
+
+  (* Not an instance because of performance; you can locally add it if you are
+  willing to pay the cost. We have concrete instances for certain fractional
+  assertions such as ↦.
+
+  Coq is sometimes unable to infer the [Φ], hence it might be useful to write
+  [apply: (frame_fractional (λ q, ...))] when using the lemma to prove your
+  custom instance. See also https://github.com/coq/coq/issues/17688 *)
+  Lemma frame_fractional Φ p R P qR qP r :
+    AsFractional R Φ qR →
+    AsFractional P Φ qP →
+    FrameFractionalQp qR qP r →
+    Frame p R P (Φ r).
+  Proof.
+    rewrite /Frame /FrameFractionalQp=> -[-> _] [-> ?] ->.
+    by rewrite bi.intuitionistically_if_elim fractional.
+  Qed.
+End fractional.
+
+(** Marked [tc_opaque] instead [Typeclasses Opaque] so that you can use
+[iDestruct] to eliminate and [iModIntro] to introduce [internal_fractional],
+while still preventing [iFrame] and [iNext] from unfolding. *)
+Definition internal_fractional {PROP : bi} (Φ : Qp → PROP) : PROP :=
+  tc_opaque (□ ∀ p q, Φ (p + q)%Qp ∗-∗ Φ p ∗ Φ q)%I.
+Global Instance: Params (@internal_fractional) 1 := {}.
+
+Section internal_fractional.
+  Context {PROP : bi}.
+  Implicit Types Φ Ψ : Qp → PROP.
+  Implicit Types q : Qp.
+
+  Global Instance internal_fractional_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@internal_fractional PROP).
+  Proof. solve_proper. Qed.
+  Global Instance internal_fractional_proper :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (@internal_fractional PROP).
+  Proof. solve_proper. Qed.
+
+  Global Instance internal_fractional_affine Φ : Affine (internal_fractional Φ).
+  Proof. rewrite /internal_fractional /=. apply _. Qed.
+  Global Instance internal_fractional_persistent Φ :
+    Persistent (internal_fractional Φ).
+  Proof. rewrite /internal_fractional /=. apply _. Qed.
+
+  Lemma fractional_internal_fractional Φ :
+    Fractional Φ → ⊢ internal_fractional Φ.
+  Proof.
+    intros. iIntros "!>" (q1 q2).
+    rewrite [Φ (q1 + q2)%Qp]fractional //=; auto.
+  Qed.
+
+  Lemma internal_fractional_iff Φ Ψ:
+    □ (∀ q, Φ q ∗-∗ Ψ q) ⊢ internal_fractional Φ -∗ internal_fractional Ψ.
+  Proof.
+    iIntros "#Hiff #HΦdup !>" (p q).
+    iSplit.
+    - iIntros "H".
+      iDestruct ("Hiff" with "H") as "HΦ".
+      iDestruct ("HΦdup" with "HΦ") as "[H1 ?]".
+      iSplitL "H1"; iApply "Hiff"; iFrame.
+    - iIntros "[H1 H2]".
+      iDestruct ("Hiff" with "H1") as "HΦ1".
+      iDestruct ("Hiff" with "H2") as "HΦ2".
+      iApply "Hiff".
+      iApply "HΦdup".
+      iFrame.
+  Qed.
+End internal_fractional.

iris/bi/lib/laterable.v

+From iris.bi Require Export bi.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+(** The class of laterable assertions *)
+Class Laterable {PROP : bi} (P : PROP) := laterable :
+  P ⊢ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
+Global Arguments Laterable {_} _%_I : simpl never.
+Global Arguments laterable {_} _%_I {_}.
+Global Hint Mode Laterable + ! : typeclass_instances.
+
+(** Proofmode class for turning [P] into a laterable [Q].
+    Will be the identity if [P] already is laterable, and add
+    [▷] otherwise. *)
+Class IntoLaterable {PROP : bi} (P Q : PROP) : Prop := {
+  (** This is non-standard; usually we would just demand
+      [P ⊢ make_laterable Q]. However, we need these stronger properties for
+      the [make_laterable_id] hack in [atomic.v]. *)
+  into_laterable : P ⊢ Q;
+  into_laterable_result_laterable : Laterable Q;
+}.
+Global Arguments IntoLaterable {_} P%_I Q%_I.
+Global Arguments into_laterable {_} P%_I Q%_I {_}.
+Global Arguments into_laterable_result_laterable {_} P%_I Q%_I {_}.
+Global Hint Mode IntoLaterable + ! - : typeclass_instances.
+
+Section instances.
+  Context {PROP : bi}.
+  Implicit Types P : PROP.
+  Implicit Types Ps : list PROP.
+
+  Global Instance laterable_proper : Proper ((⊣⊢) ==> (↔)) (@Laterable PROP).
+  Proof. solve_proper. Qed.
+
+  Global Instance later_laterable P : Laterable (▷ P).
+  Proof.
+    rewrite /Laterable. iIntros "HP". iExists P. iFrame.
+    iIntros "!> HP !>". done.
+  Qed.
+
+  Global Instance timeless_laterable P :
+    Timeless P → Laterable P.
+  Proof.
+    rewrite /Laterable. iIntros (?) "HP". iExists P%I. iFrame.
+    iSplitR; first by iNext. iIntros "!> >HP !>". done.
+  Qed.
+
+  (** This lemma is not very useful: It needs a strange assumption about
+      emp, and most of the time intuitionistic propositions can be just kept
+      around anyway and don't need to be "latered".  The lemma exists
+      because the fact that it needs the side-condition is interesting;
+      it is not an instance because it won't usually get used. *)
+  Lemma intuitionistic_laterable P :
+    Timeless (PROP:=PROP) emp → Affine P → Persistent P → Laterable P.
+  Proof.
+    rewrite /Laterable. iIntros (???) "#HP".
+    iExists emp%I. iSplitL; first by iNext.
+    iIntros "!> >_". done.
+  Qed.
+
+  (** This instance, together with the one below, can lead to massive
+      backtracking, but only when searching for [Laterable]. In the future, it
+      should be rewritten using [Hint Immediate] or [Hint Cut], where the latter
+      is preferred once we figure out how to use it. *)
+  Global Instance persistent_laterable `{!BiAffine PROP} P :
+    Persistent P → Laterable P.
+  Proof.
+    intros ?. apply intuitionistic_laterable; apply _.
+  Qed.
+
+  Global Instance sep_laterable P Q :
+    Laterable P → Laterable Q → Laterable (P ∗ Q).
+  Proof.
+    rewrite /Laterable. iIntros (LP LQ) "[HP HQ]".
+    iDestruct (LP with "HP") as (P') "[HP' #HP]".
+    iDestruct (LQ with "HQ") as (Q') "[HQ' #HQ]".
+    iExists (P' ∗ Q')%I. iSplitL; first by iFrame.
+    iIntros "!> [HP' HQ']". iSplitL "HP'".
+    - iApply "HP". done.
+    - iApply "HQ". done.
+  Qed.
+
+  Global Instance exist_laterable {A} (Φ : A → PROP) :
+    (∀ x, Laterable (Φ x)) → Laterable (∃ x, Φ x).
+  Proof.
+    rewrite /Laterable. iIntros (LΦ). iDestruct 1 as (x) "H".
+    iDestruct (LΦ with "H") as (Q) "[HQ #HΦ]".
+    iExists Q. iIntros "{$HQ} !> HQ". iExists x. by iApply "HΦ".
+  Qed.
+
+  Lemma big_sep_sepL_laterable Q Ps :
+    Laterable Q →
+    TCForall Laterable Ps →
+    Laterable (Q ∗ [∗] Ps).
+  Proof.
+    intros HQ HPs. revert Q HQ. induction HPs as [|P Ps ?? IH]; intros Q HQ.
+    { simpl. rewrite right_id. done. }
+    simpl. rewrite assoc. apply IH; by apply _.
+  Qed.
+
+  Global Instance big_sepL_laterable Ps :
+    Laterable (PROP:=PROP) emp →
+    TCForall Laterable Ps →
+    Laterable ([∗] Ps).
+  Proof.
+    intros. assert (Laterable (emp ∗ [∗] Ps)) as Hlater.
+    { apply big_sep_sepL_laterable; done. }
+    rewrite ->left_id in Hlater; last by apply _. done.
+  Qed.
+
+  (** A wrapper to obtain a weaker, laterable form of any assertion.
+     Alternatively: the modality corresponding to [Laterable].
+     The ◇ is required to make [make_laterable_intro'] hold.
+   TODO: Define [Laterable] in terms of this (see [laterable_alt] below). *)
+  Definition make_laterable (Q : PROP) : PROP :=
+    ∃ P, ▷ P ∗ □ (▷ P -∗ ◇ Q).
+
+  Global Instance make_laterable_ne : NonExpansive make_laterable.
+  Proof. solve_proper. Qed.
+  Global Instance make_laterable_proper : Proper ((≡) ==> (≡)) make_laterable := ne_proper _.
+  Global Instance make_laterable_mono' : Proper ((⊢) ==> (⊢)) make_laterable.
+  Proof. solve_proper. Qed.
+  Global Instance make_laterable_flip_mono' :
+    Proper (flip (⊢) ==> flip (⊢)) make_laterable.
+  Proof. solve_proper. Qed.
+
+  Lemma make_laterable_mono Q1 Q2 :
+    (Q1 ⊢ Q2) → (make_laterable Q1 ⊢ make_laterable Q2).
+  Proof. by intros ->. Qed.
+
+  Lemma make_laterable_except_0 Q :
+    make_laterable (◇ Q) ⊢ make_laterable Q.
+  Proof.
+    iIntros "(%P & HP & #HPQ)". iExists P. iFrame.
+    iIntros "!# HP". iMod ("HPQ" with "HP"). done.
+  Qed.
+
+  Lemma make_laterable_sep Q1 Q2 :
+    make_laterable Q1 ∗ make_laterable Q2 ⊢ make_laterable (Q1 ∗ Q2).
+  Proof.
+    iIntros "[HQ1 HQ2]".
+    iDestruct "HQ1" as (P1) "[HP1 #HQ1]".
+    iDestruct "HQ2" as (P2) "[HP2 #HQ2]".
+    iExists (P1 ∗ P2)%I. iFrame. iIntros "!# [HP1 HP2]".
+    iDestruct ("HQ1" with "HP1") as ">$".
+    iDestruct ("HQ2" with "HP2") as ">$".
+    done.
+  Qed.
+
+  (** A stronger version of [make_laterable_mono] that lets us keep laterable
+  resources. We cannot keep arbitrary resources since that would let us "frame
+  in" non-laterable things. *)
+  Lemma make_laterable_wand Q1 Q2 :
+    make_laterable (Q1 -∗ Q2) ⊢ (make_laterable Q1 -∗ make_laterable Q2).
+  Proof.
+    iIntros "HQ HQ1".
+    iDestruct (make_laterable_sep with "[$HQ $HQ1 //]") as "HQ".
+    iApply make_laterable_mono; last done.
+    by rewrite bi.wand_elim_l.
+  Qed.
+
+  (** A variant of the above for keeping arbitrary intuitionistic resources.
+      Sadly, this is not implied by the above for non-affine BIs. *)
+  Lemma make_laterable_intuitionistic_wand Q1 Q2 :
+    □ (Q1 -∗ Q2) ⊢ (make_laterable Q1 -∗ make_laterable Q2).
+  Proof.
+    iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
+    iExists P. iFrame. iIntros "!> HP".
+    iDestruct ("HQ1" with "HP") as "{HQ1} >HQ1".
+    iModIntro. iApply "HQ". done.
+  Qed.
+
+  Global Instance make_laterable_laterable Q :
+    Laterable (make_laterable Q).
+  Proof.
+    rewrite /Laterable. iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]".
+    iExists P. iFrame. iIntros "!> HP !>". iExists P. by iFrame.
+  Qed.
+
+  Lemma make_laterable_elim Q :
+    make_laterable Q ⊢ ◇ Q.
+  Proof.
+    iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
+  Qed.
+
+  (** Written internally (as an entailment of wands) to reflect
+      that persistent assertions can be kept unchanged. *)
+  Lemma make_laterable_intro P Q :
+    Laterable P →
+    □ (P -∗ Q) -∗ P -∗ make_laterable Q.
+  Proof.
+    iIntros (?) "#HQ HP".
+    iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
+    iFrame. iIntros "!> HP'".
+    iDestruct ("HPi" with "HP'") as ">HP". iModIntro.
+    iApply "HQ". done.
+  Qed.
+  Lemma make_laterable_intro' Q :
+    Laterable Q →
+    Q ⊢ make_laterable Q.
+  Proof.
+    intros ?. iApply make_laterable_intro. iIntros "!# $".
+  Qed.
+
+  Lemma make_laterable_idemp Q :
+    make_laterable (make_laterable Q) ⊣⊢ make_laterable Q.
+  Proof.
+    apply (anti_symm (⊢)).
+    - trans (make_laterable (◇ Q)).
+      + apply make_laterable_mono, make_laterable_elim.
+      + apply make_laterable_except_0.
+    - apply make_laterable_intro', _.
+  Qed.
+
+  Lemma laterable_alt Q :
+    Laterable Q ↔ (Q ⊢ make_laterable Q).
+  Proof.
+    split.
+    - intros ?. apply make_laterable_intro'. done.
+    - intros ?. done.
+  Qed.
+
+  (** * Proofmode integration
+
+      We integrate [make_laterable] with [iModIntro]. All non-laterable
+      hypotheses have a ▷ added in front of them to ensure a laterable context.
+  *)
+  Global Instance into_laterable_laterable P :
+    Laterable P →
+    IntoLaterable P P.
+  Proof. intros ?. constructor; done. Qed.
+
+  Global Instance into_laterable_fallback P :
+    IntoLaterable P (▷ P) | 100.
+  Proof. constructor; last by apply _. apply bi.later_intro. Qed.
+
+  Lemma modality_make_laterable_mixin `{!Timeless (PROP:=PROP) emp} :
+    modality_mixin make_laterable MIEnvId (MIEnvTransform IntoLaterable).
+  Proof.
+    split; simpl; eauto using make_laterable_intro', make_laterable_mono,
+      make_laterable_sep, intuitionistic_laterable with typeclass_instances; [].
+    intros P Q ?. rewrite (into_laterable P).
+    apply make_laterable_intro'. eapply (into_laterable_result_laterable P), _.
+  Qed.
+
+  Definition modality_make_laterable `{!Timeless (PROP:=PROP) emp} :=
+    Modality _ modality_make_laterable_mixin.
+
+  Global Instance from_modal_make_laterable `{!Timeless (PROP:=PROP) emp} P :
+    FromModal True modality_make_laterable (make_laterable P) (make_laterable P) P.
+  Proof. by rewrite /FromModal. Qed.
+
+End instances.
+
+Global Typeclasses Opaque make_laterable.

iris/bi/lib/relations.v

+(** This file provides constructions to lift
+a PROP-level binary relation to various closures. *)
+From iris.bi.lib Require Export fixpoint_mono.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
+
+(** * Definitions *)
+Section definitions.
+  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Context {A : ofe}.
+
+  Local Definition bi_rtc_pre (R : A → A → PROP)
+      (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
+    <affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x'.
+
+  (** The reflexive transitive closure. *)
+  Definition bi_rtc (R : A → A → PROP) (x1 x2 : A) : PROP :=
+    bi_least_fixpoint (bi_rtc_pre R x2) x1.
+
+  Global Instance: Params (@bi_rtc) 4 := {}.
+
+  Local Definition bi_tc_pre (R : A → A → PROP)
+      (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
+    R x1 x2 ∨ ∃ x', R x1 x' ∗ rec x'.
+
+  (** The transitive closure. *)
+  Definition bi_tc (R : A → A → PROP) (x1 x2 : A) : PROP :=
+    bi_least_fixpoint (bi_tc_pre R x2) x1.
+
+  Global Instance: Params (@bi_tc) 4 := {}.
+
+  (** Reductions of exactly [n] steps. *)
+  Fixpoint bi_nsteps (R : A → A → PROP) (n : nat) (x1 x2 : A) : PROP :=
+    match n with
+    | 0    => <affine> (x1 ≡ x2)
+    | S n' => ∃ x', R x1 x' ∗ bi_nsteps R n' x' x2
+    end.
+
+  Global Instance: Params (@bi_nsteps) 5 := {}.
+End definitions.
+
+Local Instance bi_rtc_pre_mono {PROP : bi} `{!BiInternalEq PROP}
+    {A : ofe} (R : A → A → PROP) `{!NonExpansive2 R} (x : A) :
+  BiMonoPred (bi_rtc_pre R x).
+Proof.
+  constructor; [|solve_proper].
+  iIntros (rec1 rec2 ??) "#H". iIntros (x1) "[Hrec | Hrec]".
+  { by iLeft. }
+  iRight.
+  iDestruct "Hrec" as (x') "[HP Hrec]".
+  iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
+Qed.
+
+Global Instance bi_rtc_ne {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP) :
+  NonExpansive2 (bi_rtc R).
+Proof.
+  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
+  solve_proper.
+Qed.
+
+Global Instance bi_rtc_proper {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP)
+  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
+Proof. apply ne_proper_2. apply _. Qed.
+
+Local Instance bi_tc_pre_mono `{!BiInternalEq PROP}
+    {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+  BiMonoPred (bi_tc_pre R x).
+Proof.
+  constructor; [|solve_proper].
+  iIntros (rec1 rec2 ??) "#H". iIntros (x1) "Hrec".
+  iDestruct "Hrec" as "[Hrec | Hrec]".
+  { by iLeft. }
+  iDestruct "Hrec" as (x') "[HR Hrec]".
+  iRight. iExists x'. iFrame "HR". by iApply "H".
+Qed.
+
+Global Instance bi_tc_ne `{!BiInternalEq PROP} {A : ofe}
+    (R : A → A → PROP) `{NonExpansive2 R} :
+  NonExpansive2 (bi_tc R).
+Proof.
+  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_tc Hx. f_equiv=> rec z.
+  solve_proper.
+Qed.
+
+Global Instance bi_tc_proper `{!BiInternalEq PROP} {A : ofe}
+    (R : A → A → PROP) `{NonExpansive2 R}
+  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_tc R).
+Proof. apply ne_proper_2. apply _. Qed.
+
+Global Instance bi_nsteps_ne {PROP : bi} `{!BiInternalEq PROP}
+    {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat) :
+  NonExpansive2 (bi_nsteps R n).
+Proof. induction n; solve_proper. Qed.
+
+Global Instance bi_nsteps_proper {PROP : bi} `{!BiInternalEq PROP}
+    {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat)
+  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_nsteps R n).
+Proof. apply ne_proper_2. apply _. Qed.
+
+(** * General theorems *)
+Section general.
+  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Context {A : ofe}.
+  Context (R : A → A → PROP) `{!NonExpansive2 R}.
+
+  (** ** Results about the reflexive-transitive closure [bi_rtc] *)
+  Local Lemma bi_rtc_unfold (x1 x2 : A) :
+    bi_rtc R x1 x2 ≡ bi_rtc_pre R x2 (λ x1, bi_rtc R x1 x2) x1.
+  Proof. by rewrite /bi_rtc; rewrite -least_fixpoint_unfold. Qed.
+
+  Lemma bi_rtc_strong_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ (Φ x' ∧ bi_rtc R x' x2)) -∗ Φ x1) -∗
+    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
+ Proof.
+    iIntros (?) "#IH". rewrite /bi_rtc.
+    by iApply (least_fixpoint_ind (bi_rtc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_rtc_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ Φ x') -∗ Φ x1) -∗
+    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
+  Proof.
+    iIntros (?) "#IH". rewrite /bi_rtc.
+    by iApply (least_fixpoint_iter (bi_rtc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_rtc_refl x : ⊢ bi_rtc R x x.
+  Proof. rewrite bi_rtc_unfold. by iLeft. Qed.
+
+  Lemma bi_rtc_l x1 x2 x3 : R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
+  Proof.
+    iIntros "H1 H2".
+    iEval (rewrite bi_rtc_unfold /bi_rtc_pre). iRight.
+    iExists x2. iFrame.
+  Qed.
+
+  Lemma bi_rtc_once x1 x2 : R x1 x2 -∗ bi_rtc R x1 x2.
+  Proof. iIntros "H". iApply (bi_rtc_l with "H"). iApply bi_rtc_refl. Qed.
+
+  Lemma bi_rtc_trans x1 x2 x3 : bi_rtc R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
+  Proof.
+    iRevert (x1).
+    iApply bi_rtc_ind_l.
+    { solve_proper. }
+    iIntros "!>" (x1) "[H | H] H2".
+    { by iRewrite "H". }
+    iDestruct "H" as (x') "[H IH]".
+    iApply (bi_rtc_l with "H").
+    by iApply "IH".
+  Qed.
+
+  Lemma bi_rtc_r x y z : bi_rtc R x y -∗ R y z -∗ bi_rtc R x z.
+  Proof.
+    iIntros "H H'".
+    iApply (bi_rtc_trans with "H").
+    by iApply bi_rtc_once.
+  Qed.
+
+  Lemma bi_rtc_inv x z :
+    bi_rtc R x z -∗ <affine> (x ≡ z) ∨ ∃ y, R x y ∗ bi_rtc R y z.
+  Proof. rewrite bi_rtc_unfold. iIntros "[H | H]"; eauto. Qed.
+
+  Global Instance bi_rtc_affine :
+    (∀ x y, Affine (R x y)) →
+    ∀ x y, Affine (bi_rtc R x y).
+  Proof. intros. apply least_fixpoint_affine; apply _. Qed.
+
+  (* FIXME: It would be nicer to use the least_fixpoint_persistent lemmas,
+            but they seem to weak. *)
+  Global Instance bi_rtc_persistent :
+    (∀ x y, Persistent (R x y)) →
+    ∀ x y, Persistent (bi_rtc R x y).
+  Proof.
+    intros ? x y. rewrite /Persistent.
+    iRevert (x). iApply bi_rtc_ind_l; first solve_proper.
+    iIntros "!>" (x) "[#Heq | (%x' & #Hxx' & #Hx'y)]".
+    { iRewrite "Heq". iApply bi_rtc_refl. }
+    iApply (bi_rtc_l with "Hxx' Hx'y").
+  Qed.
+
+  (** ** Results about the transitive closure [bi_tc] *)
+  Local Lemma bi_tc_unfold (x1 x2 : A) :
+    bi_tc R x1 x2 ≡ bi_tc_pre R x2 (λ x1, bi_tc R x1 x2) x1.
+  Proof. by rewrite /bi_tc; rewrite -least_fixpoint_unfold. Qed.
+
+  Lemma bi_tc_strong_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, (R x1 x2 ∨ (∃ x', R x1 x' ∗ (Φ x' ∧ bi_tc R x' x2))) -∗ Φ x1) -∗
+    ∀ x1, bi_tc R x1 x2 -∗ Φ x1.
+  Proof.
+    iIntros (?) "#IH". rewrite /bi_tc.
+    iApply (least_fixpoint_ind (bi_tc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_tc_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, (R x1 x2 ∨ (∃ x', R x1 x' ∗ Φ x')) -∗ Φ x1) -∗
+    ∀ x1, bi_tc R x1 x2 -∗ Φ x1.
+  Proof.
+    iIntros (?) "#IH". rewrite /bi_tc.
+    iApply (least_fixpoint_iter (bi_tc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_tc_l x1 x2 x3 : R x1 x2 -∗ bi_tc R x2 x3 -∗ bi_tc R x1 x3.
+  Proof.
+    iIntros "H1 H2".
+    iEval (rewrite bi_tc_unfold /bi_tc_pre).
+    iRight. iExists x2. iFrame.
+  Qed.
+
+  Lemma bi_tc_once x1 x2 : R x1 x2 -∗ bi_tc R x1 x2.
+  Proof.
+    iIntros "H".
+    iEval (rewrite bi_tc_unfold /bi_tc_pre).
+    by iLeft.
+  Qed.
+
+  Lemma bi_tc_trans x1 x2 x3 : bi_tc R x1 x2 -∗ bi_tc R x2 x3 -∗ bi_tc R x1 x3.
+  Proof.
+    iRevert (x1).
+    iApply bi_tc_ind_l.
+    { solve_proper. }
+    iIntros "!>" (x1) "H H2".
+    iDestruct "H" as "[H | H]".
+    { iApply (bi_tc_l with "H H2"). }
+    iDestruct "H" as (x') "[H IH]".
+    iApply (bi_tc_l with "H").
+    by iApply "IH".
+  Qed.
+
+  Lemma bi_tc_r x y z : bi_tc R x y -∗ R y z -∗ bi_tc R x z.
+  Proof.
+    iIntros "H H'".
+    iApply (bi_tc_trans with "H").
+    by iApply bi_tc_once.
+  Qed.
+
+  Lemma bi_tc_rtc_l x y z : bi_rtc R x y -∗ bi_tc R y z -∗ bi_tc R x z.
+  Proof.
+    iRevert (x).
+    iApply bi_rtc_ind_l. { solve_proper. }
+    iIntros "!>" (x) "[Heq | H] Hyz".
+    { by iRewrite "Heq". }
+    iDestruct "H" as (x') "[H IH]".
+    iApply (bi_tc_l with "H").
+    by iApply "IH".
+  Qed.
+
+  Lemma bi_tc_rtc_r x y z : bi_tc R x y -∗ bi_rtc R y z -∗ bi_tc R x z.
+  Proof.
+    iIntros "Hxy Hyz".
+    iRevert (x) "Hxy". iRevert (y) "Hyz".
+    iApply bi_rtc_ind_l. { solve_proper. }
+    iIntros "!>" (y) "[Heq | H] %x Hxy".
+    { by iRewrite -"Heq". }
+    iDestruct "H" as (y') "[H IH]".
+    iApply "IH". iApply (bi_tc_r with "Hxy H").
+  Qed.
+
+  Lemma bi_tc_rtc x y : bi_tc R x y -∗ bi_rtc R x y.
+  Proof.
+    iRevert (x). iApply bi_tc_ind_l. { solve_proper. }
+    iIntros "!>" (x) "[Hxy | H]".
+    { by iApply bi_rtc_once. }
+    iDestruct "H" as (x') "[H H']".
+    iApply (bi_rtc_l with "H H'").
+  Qed.
+
+  Global Instance bi_tc_affine :
+    (∀ x y, Affine (R x y)) →
+    ∀ x y, Affine (bi_tc R x y).
+  Proof. intros. apply least_fixpoint_affine; apply _. Qed.
+
+  Global Instance bi_tc_absorbing :
+    (∀ x y, Absorbing (R x y)) →
+    ∀ x y, Absorbing (bi_tc R x y).
+  Proof. intros. apply least_fixpoint_absorbing; apply _. Qed.
+
+  (* FIXME: It would be nicer to use the least_fixpoint_persistent lemmas,
+            but they seem to weak. *)
+  Global Instance bi_tc_persistent :
+    (∀ x y, Persistent (R x y)) →
+    ∀ x y, Persistent (bi_tc R x y).
+  Proof.
+    intros ? x y. rewrite /Persistent.
+    iRevert (x). iApply bi_tc_ind_l; first solve_proper.
+    iIntros "!# %x [#H|(%x'&#?&#?)] !>"; first by iApply bi_tc_once.
+    by iApply bi_tc_l.
+  Qed.
+
+  (** ** Results about [bi_nsteps] *)
+  Lemma bi_nsteps_O x : ⊢ bi_nsteps R 0 x x.
+  Proof. auto. Qed.
+  Lemma bi_nsteps_once x y : R x y -∗ bi_nsteps R 1 x y.
+  Proof. simpl. eauto. Qed.
+  Lemma bi_nsteps_once_inv x y : bi_nsteps R 1 x y -∗ R x y.
+  Proof. iDestruct 1 as (x') "[Hxx' Heq]". by iRewrite -"Heq". Qed.
+  Lemma bi_nsteps_l n x y z : R x y -∗ bi_nsteps R n y z -∗ bi_nsteps R (S n) x z.
+  Proof. iIntros "? ?". iExists y. iFrame. Qed.
+
+  Lemma bi_nsteps_trans n m x y z :
+    bi_nsteps R n x y -∗ bi_nsteps R m y z -∗ bi_nsteps R (n + m) x z.
+  Proof.
+    iInduction n as [|n IH] forall (x); simpl.
+    - iIntros "Heq". iRewrite "Heq". auto.
+    - iDestruct 1 as (x') "[Hxx' Hx'y]". iIntros "Hyz".
+      iExists x'. iFrame "Hxx'". iApply ("IH" with "Hx'y Hyz").
+  Qed.
+
+  Lemma bi_nsteps_r n x y z :
+    bi_nsteps R n x y -∗ R y z -∗ bi_nsteps R (S n) x z.
+  Proof.
+    iIntros "Hxy Hyx". rewrite -Nat.add_1_r.
+    iApply (bi_nsteps_trans with "Hxy").
+    by iApply bi_nsteps_once.
+  Qed.
+
+  Lemma bi_nsteps_add_inv n m x z :
+    bi_nsteps R (n + m) x z ⊢ ∃ y, bi_nsteps R n x y ∗ bi_nsteps R m y z.
+  Proof.
+    iInduction n as [|n IH] forall (x).
+    - iIntros "Hxz". iExists x. auto.
+    - iDestruct 1 as (y) "[Hxy Hyz]".
+      iDestruct ("IH" with "Hyz") as (y') "[Hyy' Hy'z]".
+      iExists y'. iFrame "Hy'z".
+      iApply (bi_nsteps_l with "Hxy Hyy'").
+  Qed.
+
+  Lemma bi_nsteps_inv_r n x z :
+    bi_nsteps R (S n) x z ⊢ ∃ y, bi_nsteps R n x y ∗ R y z.
+  Proof.
+    rewrite -Nat.add_1_r bi_nsteps_add_inv /=.
+    iDestruct 1 as (y) "[Hxy (%x' & Hxx' & Heq)]".
+    iExists y. iRewrite -"Heq". iFrame.
+  Qed.
+
+  (** ** Equivalences between closure operators *)
+  Lemma bi_rtc_tc x y : bi_rtc R x y ⊣⊢ <affine> (x ≡ y) ∨ bi_tc R x y.
+  Proof.
+    iSplit.
+    - iRevert (x). iApply bi_rtc_ind_l. { solve_proper. }
+      iIntros "!>" (x) "[Heq | H]".
+      { by iLeft. }
+      iRight.
+      iDestruct "H" as (x') "[H [Heq | IH]]".
+      { iRewrite -"Heq". by iApply bi_tc_once. }
+      iApply (bi_tc_l with "H IH").
+    - iIntros "[Heq | Hxy]".
+      { iRewrite "Heq". iApply bi_rtc_refl. }
+      by iApply bi_tc_rtc.
+  Qed.
+
+  Lemma bi_tc_nsteps x y :
+    bi_tc R x y ⊣⊢ ∃ n, <affine> ⌜0 < n⌝ ∗ bi_nsteps R n x y.
+  Proof.
+    iSplit.
+    - iRevert (x). iApply bi_tc_ind_l. { solve_proper. }
+      iIntros "!>" (x) "[Hxy | H]".
+      { iExists 1. iSplitR; first auto with lia.
+        iApply (bi_nsteps_l with "Hxy"). iApply bi_nsteps_O. }
+      iDestruct "H" as (x') "[Hxx' IH]".
+      iDestruct "IH" as (n ?) "Hx'y".
+      iExists (S n). iSplitR; first auto with lia.
+      iApply (bi_nsteps_l with "Hxx' Hx'y").
+    - iDestruct 1 as (n ?) "Hxy".
+      iInduction n as [|n IH] forall (y). { lia. }
+      rewrite bi_nsteps_inv_r.
+      iDestruct "Hxy" as (x') "[Hxx' Hx'y]".
+      destruct n.
+      { simpl. iRewrite "Hxx'". by iApply bi_tc_once. }
+      iApply (bi_tc_r with "[Hxx'] Hx'y").
+      iApply ("IH" with "[%] Hxx'"). lia.
+  Qed.
+
+  Lemma bi_rtc_nsteps x y : bi_rtc R x y ⊣⊢ ∃ n, bi_nsteps R n x y.
+  Proof.
+    iSplit.
+    - iRevert (x). iApply bi_rtc_ind_l. { solve_proper. }
+      iIntros "!>" (x) "[Heq | H]".
+      { iExists 0. iRewrite "Heq". iApply bi_nsteps_O. }
+      iDestruct "H" as (x') "[Hxx' IH]".
+      iDestruct "IH" as (n) "Hx'y".
+      iExists (S n). iApply (bi_nsteps_l with "Hxx' Hx'y").
+    - iDestruct 1 as (n) "Hxy".
+      iInduction n as [|n IH] forall (y).
+      { simpl. iRewrite "Hxy". iApply bi_rtc_refl. }
+      iDestruct (bi_nsteps_inv_r with "Hxy") as (x') "[Hxx' Hx'y]".
+      iApply (bi_rtc_r with "[Hxx'] Hx'y").
+      by iApply "IH".
+  Qed.
+End general.
+
+Section timeless.
+  Context {PROP : bi} `{!BiInternalEq PROP, !BiAffine PROP}.
+  Context `{!OfeDiscrete A}.
+  Context (R : A → A → PROP) `{!NonExpansive2 R}.
+
+  Global Instance bi_nsteps_timeless n :
+    (∀ x y, Timeless (R x y)) →
+    ∀ x y, Timeless (bi_nsteps R n x y).
+  Proof. induction n; apply _. Qed.
+
+  Global Instance bi_rtc_timeless :
+    (∀ x y, Timeless (R x y)) →
+    ∀ x y, Timeless (bi_rtc R x y).
+  Proof. intros ? x y. rewrite bi_rtc_nsteps. apply _. Qed.
+
+  Global Instance bi_tc_timeless :
+    (∀ x y, Timeless (R x y)) →
+    ∀ x y, Timeless (bi_tc R x y).
+  Proof. intros ? x y. rewrite bi_tc_nsteps. apply _. Qed.
+End timeless.
+
+Global Typeclasses Opaque bi_rtc.
+Global Typeclasses Opaque bi_tc.
+Global Typeclasses Opaque bi_nsteps.

iris/bi/monpred.v

+From stdpp Require Import coPset.
+From iris.bi Require Import bi.
+From iris.prelude Require Import options.
+
+(** Definitions. *)
+Structure biIndex :=
+  BiIndex
+    { bi_index_type :> Type;
+      bi_index_inhabited : Inhabited bi_index_type;
+      bi_index_rel : SqSubsetEq bi_index_type;
+      bi_index_rel_preorder : PreOrder (⊑@{bi_index_type}) }.
+Global Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
+
+(* We may want to instantiate monPred with the reflexivity relation in
+   the case where there is no relevant order. In that case, there is
+   no bottom element, so that we do not want to force any BI index to
+   have one. *)
+Class BiIndexBottom {I : biIndex} (bot : I) :=
+  bi_index_bot i : bot ⊑ i.
+
+Section cofe.
+  Context {I : biIndex} {PROP : bi}.
+  Implicit Types i : I.
+
+  Record monPred :=
+    MonPred { monPred_at :> I → PROP;
+              monPred_mono : Proper ((⊑) ==> (⊢)) monPred_at }.
+  Local Existing Instance monPred_mono.
+
+  Bind Scope bi_scope with monPred.
+
+  Implicit Types P Q : monPred.
+
+  (** Ofe + Cofe instances  *)
+
+  Section cofe_def.
+    Inductive monPred_equiv' P Q : Prop :=
+      { monPred_in_equiv i : P i ≡ Q i } .
+    Local Instance monPred_equiv : Equiv monPred := monPred_equiv'.
+    Inductive monPred_dist' (n : nat) (P Q : monPred) : Prop :=
+      { monPred_in_dist i : P i ≡{n}≡ Q i }.
+    Local Instance monPred_dist : Dist monPred := monPred_dist'.
+
+    Definition monPred_sig P : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f } :=
+      exist _ (monPred_at P) (monPred_mono P).
+
+    Definition sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f })
+      : monPred :=
+      MonPred (proj1_sig P') (proj2_sig P').
+
+    (* These two lemma use the wrong Equiv and Dist instance for
+      monPred. so we make sure they are not accessible outside of the
+      section by using Let. *)
+    Let monPred_sig_equiv:
+      ∀ P Q, P ≡ Q ↔ monPred_sig P ≡ monPred_sig Q.
+    Proof. by split; [intros []|]. Defined.
+    Let monPred_sig_dist:
+      ∀ n, ∀ P Q : monPred, P ≡{n}≡ Q ↔ monPred_sig P ≡{n}≡ monPred_sig Q.
+    Proof. by split; [intros []|]. Defined.
+
+    Definition monPred_ofe_mixin : OfeMixin monPred.
+    Proof.
+      by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist).
+    Qed.
+
+    Canonical Structure monPredO := Ofe monPred monPred_ofe_mixin.
+
+    Global Instance monPred_cofe `{!Cofe PROP} : Cofe monPredO.
+    Proof.
+      refine ((iso_cofe_subtype' (A:=I-d>PROP) _ MonPred monPred_at _ _ _) _);
+        [done..|].
+      apply limit_preserving_forall=> y. apply limit_preserving_forall=> x.
+      apply limit_preserving_impl; [solve_proper|].
+      apply bi.limit_preserving_entails; solve_proper.
+    Qed.
+  End cofe_def.
+
+  Lemma monPred_sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f }) :
+    monPred_sig (sig_monPred P') ≡ P'.
+  Proof. by change (P' ≡ P'). Qed.
+  Lemma sig_monPred_sig P : sig_monPred (monPred_sig P) ≡ P.
+  Proof. done. Qed.
+
+  Global Instance monPred_sig_ne : NonExpansive monPred_sig.
+  Proof. move=> ??? [?] ? //=. Qed.
+  Global Instance monPred_sig_proper : Proper ((≡) ==> (≡)) monPred_sig.
+  Proof. eapply (ne_proper _). Qed.
+  Global Instance sig_monPred_ne : NonExpansive (@sig_monPred).
+  Proof. split=>? //=. Qed.
+  Global Instance sig_monPred_proper : Proper ((≡) ==> (≡)) sig_monPred.
+  Proof. eapply (ne_proper _). Qed.
+
+  (* We generalize over the relation R which is morally the equivalence
+     relation over B. That way, the BI index can use equality as an
+     equivalence relation (and Coq is able to infer the Proper and
+     Reflexive instances properly), or any other equivalence relation,
+     provided it is compatible with (⊑). *)
+  Global Instance monPred_at_ne (R : relation I) :
+    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
+    ∀ n, Proper (dist n ==> R ==> dist n) monPred_at.
+  Proof.
+    intros ????? [Hd] ?? HR. rewrite Hd.
+    apply equiv_dist, bi.equiv_entails; split; f_equiv; rewrite ->HR; done.
+  Qed.
+  Global Instance monPred_at_proper (R : relation I) :
+    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
+    Proper ((≡) ==> R ==> (≡)) monPred_at.
+  Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
+End cofe.
+
+Global Arguments monPred _ _ : clear implicits.
+Global Arguments monPred_at {_ _} _%_I _.
+Local Existing Instance monPred_mono.
+Global Arguments monPredO _ _ : clear implicits.
+
+(** BI canonical structure and type class instances *)
+Module Export monPred_defs.
+Section monPred_defs.
+  Context {I : biIndex} {PROP : bi}.
+  Implicit Types i : I.
+  Notation monPred := (monPred I PROP).
+  Implicit Types P Q : monPred.
+
+  Inductive monPred_entails (P1 P2 : monPred) : Prop :=
+    { monPred_in_entails i : P1 i ⊢ P2 i }.
+  Local Hint Immediate monPred_in_entails : core.
+
+  Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
+    MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
+  Next Obligation. solve_proper. Qed.
+
+  Local Definition monPred_embed_def : Embed PROP monPred := λ (P : PROP),
+    MonPred (λ _, P) _.
+  Local Definition monPred_embed_aux : seal (@monPred_embed_def).
+  Proof. by eexists. Qed.
+  Definition monPred_embed := monPred_embed_aux.(unseal).
+  Local Definition monPred_embed_unseal :
+    @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
+
+  Local Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
+  Local Definition monPred_emp_aux : seal (@monPred_emp_def). Proof. by eexists. Qed.
+  Definition monPred_emp := monPred_emp_aux.(unseal).
+  Local Definition monPred_emp_unseal :
+    @monPred_emp = _ := monPred_emp_aux.(seal_eq).
+
+  Local Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φ⌝)%I _.
+  Local Definition monPred_pure_aux : seal (@monPred_pure_def).
+  Proof. by eexists. Qed.
+  Definition monPred_pure := monPred_pure_aux.(unseal).
+  Local Definition monPred_pure_unseal :
+    @monPred_pure = _ := monPred_pure_aux.(seal_eq).
+
+  Local Definition monPred_objectively_def P : monPred :=
+    MonPred (λ _, ∀ i, P i)%I _.
+  Local Definition monPred_objectively_aux : seal (@monPred_objectively_def).
+  Proof. by eexists. Qed.
+  Definition monPred_objectively := monPred_objectively_aux.(unseal).
+  Local Definition monPred_objectively_unseal :
+    @monPred_objectively = _ := monPred_objectively_aux.(seal_eq).
+
+  Local Definition monPred_subjectively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
+  Local Definition monPred_subjectively_aux : seal (@monPred_subjectively_def).
+  Proof. by eexists. Qed.
+  Definition monPred_subjectively := monPred_subjectively_aux.(unseal).
+  Local Definition monPred_subjectively_unseal :
+    @monPred_subjectively = _ := monPred_subjectively_aux.(seal_eq).
+
+  Local Program Definition monPred_and_def P Q : monPred :=
+    MonPred (λ i, P i ∧ Q i)%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_and_aux : seal (@monPred_and_def).
+  Proof. by eexists. Qed.
+  Definition monPred_and := monPred_and_aux.(unseal).
+  Local Definition monPred_and_unseal :
+    @monPred_and = _ := monPred_and_aux.(seal_eq).
+
+  Local Program Definition monPred_or_def P Q : monPred :=
+    MonPred (λ i, P i ∨ Q i)%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_or_aux : seal (@monPred_or_def).
+  Proof. by eexists. Qed.
+  Definition monPred_or := monPred_or_aux.(unseal).
+  Local Definition monPred_or_unseal :
+    @monPred_or = _ := monPred_or_aux.(seal_eq).
+
+  Local Definition monPred_impl_def P Q : monPred :=
+    monPred_upclosed (λ i, P i → Q i)%I.
+  Local Definition monPred_impl_aux : seal (@monPred_impl_def).
+  Proof. by eexists. Qed.
+  Definition monPred_impl := monPred_impl_aux.(unseal).
+  Local Definition monPred_impl_unseal :
+    @monPred_impl = _ := monPred_impl_aux.(seal_eq).
+
+  Local Program Definition monPred_forall_def A (Φ : A → monPred) : monPred :=
+    MonPred (λ i, ∀ x : A, Φ x i)%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_forall_aux : seal (@monPred_forall_def).
+  Proof. by eexists. Qed.
+  Definition monPred_forall := monPred_forall_aux.(unseal).
+  Local Definition monPred_forall_unseal :
+    @monPred_forall = _ := monPred_forall_aux.(seal_eq).
+
+  Local Program Definition monPred_exist_def A (Φ : A → monPred) : monPred :=
+    MonPred (λ i, ∃ x : A, Φ x i)%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_exist_aux : seal (@monPred_exist_def).
+  Proof. by eexists. Qed.
+  Definition monPred_exist := monPred_exist_aux.(unseal).
+  Local Definition monPred_exist_unseal :
+    @monPred_exist = _ := monPred_exist_aux.(seal_eq).
+
+  Local Program Definition monPred_sep_def P Q : monPred :=
+    MonPred (λ i, P i ∗ Q i)%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_sep_aux : seal (@monPred_sep_def).
+  Proof. by eexists. Qed.
+  Definition monPred_sep := monPred_sep_aux.(unseal).
+  Local Definition monPred_sep_unseal :
+    @monPred_sep = _ := monPred_sep_aux.(seal_eq).
+
+  Local Definition monPred_wand_def P Q : monPred :=
+    monPred_upclosed (λ i, P i -∗ Q i)%I.
+  Local Definition monPred_wand_aux : seal (@monPred_wand_def).
+  Proof. by eexists. Qed.
+  Definition monPred_wand := monPred_wand_aux.(unseal).
+  Local Definition monPred_wand_unseal :
+    @monPred_wand = _ := monPred_wand_aux.(seal_eq).
+
+  Local Program Definition monPred_persistently_def P : monPred :=
+    MonPred (λ i, <pers> (P i))%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_persistently_aux : seal (@monPred_persistently_def).
+  Proof. by eexists. Qed.
+  Definition monPred_persistently := monPred_persistently_aux.(unseal).
+  Local Definition monPred_persistently_unseal :
+    @monPred_persistently = _ := monPred_persistently_aux.(seal_eq).
+
+  Local Program Definition monPred_in_def (i0 : I) : monPred :=
+    MonPred (λ i : I, ⌜i0 ⊑ i⌝%I) _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
+  Definition monPred_in := monPred_in_aux.(unseal).
+  Local Definition monPred_in_unseal :
+    @monPred_in = _ := monPred_in_aux.(seal_eq).
+
+  Local Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_later_aux : seal monPred_later_def.
+  Proof. by eexists. Qed.
+  Definition monPred_later := monPred_later_aux.(unseal).
+  Local Definition monPred_later_unseal :
+    monPred_later = _ := monPred_later_aux.(seal_eq).
+
+  Local Definition monPred_internal_eq_def `{!BiInternalEq PROP}
+    (A : ofe) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _.
+  Local Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
+  Proof. by eexists. Qed.
+  Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
+  Global Arguments monPred_internal_eq {_}.
+  Local Definition monPred_internal_eq_unseal `{!BiInternalEq PROP} :
+    @internal_eq _ monPred_internal_eq = monPred_internal_eq_def.
+  Proof. by rewrite -monPred_internal_eq_aux.(seal_eq). Qed.
+
+  Local Program Definition monPred_bupd_def `{BiBUpd PROP}
+    (P : monPred) : monPred := MonPred (λ i, |==> P i)%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_bupd_aux : seal (@monPred_bupd_def).
+  Proof. by eexists. Qed.
+  Definition monPred_bupd := monPred_bupd_aux.(unseal).
+  Global Arguments monPred_bupd {_}.
+  Local Definition monPred_bupd_unseal `{BiBUpd PROP} :
+    @bupd _ monPred_bupd = monPred_bupd_def.
+  Proof. by rewrite -monPred_bupd_aux.(seal_eq). Qed.
+
+  Local Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
+    (P : monPred) : monPred := MonPred (λ i, |={E1,E2}=> P i)%I _.
+  Next Obligation. solve_proper. Qed.
+  Local Definition monPred_fupd_aux : seal (@monPred_fupd_def).
+  Proof. by eexists. Qed.
+  Definition monPred_fupd := monPred_fupd_aux.(unseal).
+  Global Arguments monPred_fupd {_}.
+  Local Definition monPred_fupd_unseal `{BiFUpd PROP} :
+    @fupd _ monPred_fupd = monPred_fupd_def.
+  Proof. by rewrite -monPred_fupd_aux.(seal_eq). Qed.
+
+  Local Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
+    MonPred (λ _, ∀ i, ■ (P i))%I _.
+  Local Definition monPred_plainly_aux : seal (@monPred_plainly_def).
+  Proof. by eexists. Qed.
+  Definition monPred_plainly := monPred_plainly_aux.(unseal).
+  Global Arguments monPred_plainly {_}.
+  Local Definition monPred_plainly_unseal `{BiPlainly PROP} :
+    @plainly _ monPred_plainly = monPred_plainly_def.
+  Proof. by rewrite -monPred_plainly_aux.(seal_eq). Qed.
+End monPred_defs.
+
+(** This is not the final collection of unsealing lemmas, below we redefine
+[monPred_unseal] to also unfold the BI layer (i.e., the projections of the BI
+structures/classes). *)
+Local Definition monPred_unseal :=
+  (@monPred_embed_unseal, @monPred_emp_unseal, @monPred_pure_unseal,
+   @monPred_objectively_unseal, @monPred_subjectively_unseal,
+   @monPred_and_unseal, @monPred_or_unseal, @monPred_impl_unseal,
+   @monPred_forall_unseal, @monPred_exist_unseal, @monPred_sep_unseal,
+   @monPred_wand_unseal, @monPred_persistently_unseal,
+   @monPred_in_unseal, @monPred_later_unseal).
+End monPred_defs.
+
+Global Arguments monPred_objectively {_ _} _%_I.
+Global Arguments monPred_subjectively {_ _} _%_I.
+Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
+Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
+
+Section instances.
+  Context (I : biIndex) (PROP : bi).
+
+  Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
+    monPred_entails monPred_emp monPred_pure monPred_and monPred_or
+    monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand.
+  Proof.
+    split; rewrite ?monPred_defs.monPred_unseal;
+      try by (split=> ? /=; repeat f_equiv).
+    - split.
+      + intros P. by split.
+      + intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
+    - split.
+      + intros [HPQ]. split; split => i; move: (HPQ i); by apply bi.equiv_entails.
+      + intros [[] []]. split=>i. by apply bi.equiv_entails.
+    - intros P φ ?. split=> i. by apply bi.pure_intro.
+    - intros φ P HP. split=> i. apply bi.pure_elim'=> ?. by apply HP.
+    - intros P Q. split=> i. by apply bi.and_elim_l.
+    - intros P Q. split=> i. by apply bi.and_elim_r.
+    - intros P Q R [?] [?]. split=> i. by apply bi.and_intro.
+    - intros P Q. split=> i. by apply bi.or_intro_l.
+    - intros P Q. split=> i. by apply bi.or_intro_r.
+    - intros P Q R [?] [?]. split=> i. by apply bi.or_elim.
+    - intros P Q R [HR]. split=> i /=. setoid_rewrite bi.pure_impl_forall.
+      apply bi.forall_intro=> j. apply bi.forall_intro=> Hij.
+      apply bi.impl_intro_r. by rewrite -HR /= !Hij.
+    - intros P Q R [HR]. split=> i /=.
+      rewrite HR /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+      apply bi.impl_elim_l.
+    - intros A P Ψ HΨ. split=> i. apply bi.forall_intro => ?. by apply HΨ.
+    - intros A Ψ. split=> i. by apply: bi.forall_elim.
+    - intros A Ψ a. split=> i. by rewrite /= -bi.exist_intro.
+    - intros A Ψ Q HΨ. split=> i. apply bi.exist_elim => a. by apply HΨ.
+    - intros P P' Q Q' [?] [?]. split=> i. by apply bi.sep_mono.
+    - intros P. split=> i. by apply bi.emp_sep_1.
+    - intros P. split=> i. by apply bi.emp_sep_2.
+    - intros P Q. split=> i. by apply bi.sep_comm'.
+    - intros P Q R. split=> i. by apply bi.sep_assoc'.
+    - intros P Q R [HR]. split=> i /=. setoid_rewrite bi.pure_impl_forall.
+      apply bi.forall_intro=> j. apply bi.forall_intro=> Hij.
+      apply bi.wand_intro_r. by rewrite -HR /= !Hij.
+    - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'.
+      rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+  Qed.
+
+  Lemma monPred_bi_persistently_mixin :
+    BiPersistentlyMixin (PROP:=monPred I PROP)
+      monPred_entails monPred_emp monPred_and
+      monPred_exist monPred_sep monPred_persistently.
+  Proof.
+    split; rewrite ?monPred_defs.monPred_unseal;
+      try by (split=> ? /=; repeat f_equiv).
+    - intros P Q [?]. split=> i /=. by f_equiv.
+    - intros P. split=> i. by apply bi.persistently_idemp_2.
+    - split=> i. by apply bi.persistently_emp_intro.
+    - intros A Ψ. split=> i. by apply bi.persistently_and_2.
+    - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
+    - intros P Q. split=> i. apply bi.sep_elim_l, _.
+    - intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
+  Qed.
+
+  Lemma monPred_bi_later_mixin :
+    BiLaterMixin (PROP:=monPred I PROP)
+      monPred_entails monPred_pure
+      monPred_or monPred_impl monPred_forall monPred_exist
+      monPred_sep monPred_persistently monPred_later.
+  Proof.
+    split; rewrite ?monPred_defs.monPred_unseal.
+    - by split=> ? /=; repeat f_equiv.
+    - intros P Q [?]. split=> i. by apply bi.later_mono.
+    - intros P. split=> i /=. by apply bi.later_intro.
+    - intros A Ψ. split=> i. by apply bi.later_forall_2.
+    - intros A Ψ. split=> i. by apply bi.later_exist_false.
+    - intros P Q. split=> i. by apply bi.later_sep_1.
+    - intros P Q. split=> i. by apply bi.later_sep_2.
+    - intros P. split=> i. by apply bi.later_persistently_1.
+    - intros P. split=> i. by apply bi.later_persistently_2.
+    - intros P. split=> i /=. rewrite -bi.forall_intro.
+      + apply bi.later_false_em.
+      + intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij.
+        by rewrite Hij.
+  Qed.
+
+  Canonical Structure monPredI : bi :=
+    {| bi_ofe_mixin := monPred_ofe_mixin;
+       bi_bi_mixin := monPred_bi_mixin;
+       bi_bi_persistently_mixin := monPred_bi_persistently_mixin;
+       bi_bi_later_mixin := monPred_bi_later_mixin |}.
+
+  (** We restate the unsealing lemmas so that they also unfold the BI layer. The
+  sealing lemmas are partially applied so that they also work under binders. *)
+  Local Lemma monPred_emp_unseal :
+    bi_emp = @monPred_defs.monPred_emp_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_emp_unseal. Qed.
+  Local Lemma monPred_pure_unseal :
+    bi_pure = @monPred_defs.monPred_pure_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_pure_unseal. Qed.
+  Local Lemma monPred_and_unseal :
+    bi_and = @monPred_defs.monPred_and_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_and_unseal. Qed.
+  Local Lemma monPred_or_unseal :
+    bi_or = @monPred_defs.monPred_or_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_or_unseal. Qed.
+  Local Lemma monPred_impl_unseal :
+    bi_impl = @monPred_defs.monPred_impl_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_impl_unseal. Qed.
+  Local Lemma monPred_forall_unseal :
+    @bi_forall _ = @monPred_defs.monPred_forall_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_forall_unseal. Qed.
+  Local Lemma monPred_exist_unseal :
+    @bi_exist _ = @monPred_defs.monPred_exist_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_exist_unseal. Qed.
+  Local Lemma monPred_sep_unseal :
+    bi_sep = @monPred_defs.monPred_sep_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_sep_unseal. Qed.
+  Local Lemma monPred_wand_unseal :
+    bi_wand = @monPred_defs.monPred_wand_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_wand_unseal. Qed.
+  Local Lemma monPred_persistently_unseal :
+    bi_persistently = @monPred_defs.monPred_persistently_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_persistently_unseal. Qed.
+  Local Lemma monPred_later_unseal :
+    bi_later = @monPred_defs.monPred_later_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_later_unseal. Qed.
+
+  (** This definition only includes the unseal lemmas for the [bi] connectives.
+  After we have defined the right class instances, we define [monPred_unseal],
+  which also includes [embed], [internal_eq], [bupd], [fupd], [plainly],
+  [monPred_objectively], [monPred_subjectively] and [monPred_in]. *)
+  Local Definition monPred_unseal_bi :=
+    (monPred_emp_unseal, monPred_pure_unseal, monPred_and_unseal,
+    monPred_or_unseal, monPred_impl_unseal, monPred_forall_unseal,
+    monPred_exist_unseal, monPred_sep_unseal, monPred_wand_unseal,
+    monPred_persistently_unseal, monPred_later_unseal).
+
+  Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
+  Proof.
+    split; try apply _; rewrite /bi_emp_valid
+      !(monPred_defs.monPred_embed_unseal, monPred_unseal_bi); try done.
+    - move=> P /= [/(_ inhabitant) ?] //.
+    - intros PROP' ? P Q.
+      set (f P := @monPred_at I PROP P inhabitant).
+      assert (NonExpansive f) by solve_proper.
+      apply (f_equivI f).
+    - intros P Q. split=> i /=.
+      by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+    - intros P Q. split=> i /=.
+      by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+  Qed.
+  Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
+    {| bi_embed_mixin := monPred_embedding_mixin |}.
+
+  Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
+    BiInternalEqMixin monPredI monPred_internal_eq.
+  Proof.
+    split;
+      rewrite !(monPred_defs.monPred_internal_eq_unseal, monPred_unseal_bi).
+    - split=> i /=. solve_proper.
+    - intros A P a. split=> i /=. apply internal_eq_refl.
+    - intros A a b Ψ ?. split=> i /=.
+      setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro => ?.
+      erewrite (internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
+    - intros A1 A2 f g. split=> i /=. by apply fun_extI.
+    - intros A P x y. split=> i /=. by apply sig_equivI_1.
+    - intros A a b ?. split=> i /=. by apply discrete_eq_1.
+    - intros A x y. split=> i /=. by apply later_equivI_1.
+    - intros A x y. split=> i /=. by apply later_equivI_2.
+  Qed.
+  Global Instance monPred_bi_internal_eq `{BiInternalEq PROP} :
+      BiInternalEq monPredI :=
+    {| bi_internal_eq_mixin := monPred_internal_eq_mixin |}.
+
+  Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
+  Proof.
+    split; rewrite !(monPred_defs.monPred_bupd_unseal, monPred_unseal_bi).
+    - split=>/= i. solve_proper.
+    - intros P. split=>/= i. apply bupd_intro.
+    - intros P Q [HPQ]. split=>/= i. by rewrite HPQ.
+    - intros P. split=>/= i. apply bupd_trans.
+    - intros P Q. split=>/= i. apply bupd_frame_r.
+  Qed.
+  Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
+    {| bi_bupd_mixin := monPred_bupd_mixin |}.
+
+  Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
+  Proof.
+    split; rewrite /bi_emp_valid /bi_except_0
+      !(monPred_defs.monPred_fupd_unseal, monPred_unseal_bi).
+    - split=>/= i. solve_proper.
+    - intros E1 E2 HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
+    - intros E1 E2 P. split=>/= i. apply except_0_fupd.
+    - intros E1 E2 P Q [HPQ]. split=>/= i. by rewrite HPQ.
+    - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
+    - intros E1 E2 Ef P HE1f. split=>/= i.
+      by rewrite (bi.forall_elim i) bi.pure_True // left_id fupd_mask_frame_r'.
+    - intros E1 E2 P Q. split=>/= i. apply fupd_frame_r.
+  Qed.
+  Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI :=
+    {| bi_fupd_mixin := monPred_fupd_mixin |}.
+
+  Lemma monPred_plainly_mixin `{BiPlainly PROP} :
+    BiPlainlyMixin monPredI monPred_plainly.
+  Proof.
+    split; rewrite !(monPred_defs.monPred_plainly_unseal, monPred_unseal_bi).
+    - by (split=> ? /=; repeat f_equiv).
+    - intros P Q [?]. split=> i /=. by do 3 f_equiv.
+    - intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently.
+    - intros P. split=> i /=. do 3 setoid_rewrite <-plainly_forall.
+      rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
+    - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
+      rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
+    - intros P Q. split=> i /=.
+      setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
+      do 2 setoid_rewrite <-plainly_forall.
+      setoid_rewrite plainly_impl_plainly. f_equiv.
+      do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
+    - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
+    - intros P Q. split=> i. apply bi.sep_elim_l, _.
+    - intros P. split=> i /=.
+      rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
+    - intros P. split=> i /=.
+      rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
+  Qed.
+  Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
+    {| bi_plainly_mixin := monPred_plainly_mixin |}.
+
+  Local Lemma monPred_embed_unseal :
+    embed = @monPred_defs.monPred_embed_def I PROP.
+  Proof. by rewrite -monPred_defs.monPred_embed_unseal. Qed.
+  Local Lemma monPred_internal_eq_unseal `{!BiInternalEq PROP} :
+    @internal_eq _ _ = @monPred_defs.monPred_internal_eq_def I PROP _.
+  Proof. by rewrite -monPred_defs.monPred_internal_eq_unseal. Qed.
+  Local Lemma monPred_bupd_unseal `{BiBUpd PROP} :
+    bupd = @monPred_defs.monPred_bupd_def I PROP _.
+  Proof. by rewrite -monPred_defs.monPred_bupd_unseal. Qed.
+  Local Lemma monPred_fupd_unseal `{BiFUpd PROP} :
+    fupd = @monPred_defs.monPred_fupd_def I PROP _.
+  Proof. by rewrite -monPred_defs.monPred_fupd_unseal. Qed.
+  Local Lemma monPred_plainly_unseal `{BiPlainly PROP} :
+    plainly = @monPred_defs.monPred_plainly_def I PROP _.
+  Proof. by rewrite -monPred_defs.monPred_plainly_unseal. Qed.
+
+  (** And finally the proper [unseal] tactic (which we also redefine outside
+  of the section since Ltac definitions do not outlive a section). *)
+  Local Definition monPred_unseal :=
+    (monPred_unseal_bi,
+    @monPred_defs.monPred_objectively_unseal,
+    @monPred_defs.monPred_subjectively_unseal,
+    @monPred_embed_unseal, @monPred_internal_eq_unseal,
+    @monPred_bupd_unseal, @monPred_fupd_unseal, @monPred_plainly_unseal,
+    @monPred_defs.monPred_in_unseal).
+  Ltac unseal := rewrite !monPred_unseal /=.
+
+  Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
+  Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
+  Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
+  Proof. split => ?. rewrite /bi_affinely. unseal. apply bi_positive. Qed.
+  Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
+  Proof. split => ?. unseal. by apply affine. Qed.
+
+  Global Instance monPred_bi_persistently_forall :
+    BiPersistentlyForall PROP → BiPersistentlyForall monPredI.
+  Proof. intros ? A φ. split=> /= i. unseal. by apply persistently_forall_2. Qed.
+
+  Global Instance monPred_bi_pure_forall :
+    BiPureForall PROP → BiPureForall monPredI.
+  Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
+
+  Global Instance monPred_bi_later_contractive :
+    BiLaterContractive PROP → BiLaterContractive monPredI.
+  Proof. intros ? n. unseal=> P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
+
+  Global Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
+  Proof. split. by unseal. Qed.
+
+  Global Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
+  Proof. split; by unseal. Qed.
+
+  Global Instance monPred_bi_embed_internal_eq `{BiInternalEq PROP} :
+    BiEmbedInternalEq PROP monPredI.
+  Proof. split. by unseal. Qed.
+
+  Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
+  Proof. intros E P. split=> i. unseal. apply bupd_fupd. Qed.
+
+  Global Instance monPred_bi_embed_bupd `{!BiBUpd PROP} :
+    BiEmbedBUpd PROP monPredI.
+  Proof. split. by unseal. Qed.
+
+  Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
+  Proof. split. by unseal. Qed.
+
+  Global Instance monPred_bi_persistently_impl_plainly
+       `{!BiPlainly PROP, !BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} :
+    BiPersistentlyImplPlainly monPredI.
+  Proof.
+    intros P Q. split=> i. unseal. setoid_rewrite bi.pure_impl_forall.
+    setoid_rewrite <-plainly_forall.
+    do 2 setoid_rewrite bi.persistently_forall.
+    by setoid_rewrite persistently_impl_plainly.
+  Qed.
+
+  Global Instance monPred_bi_prop_ext
+    `{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
+  Proof.
+    intros P Q. split=> i /=. rewrite /bi_wand_iff. unseal.
+    rewrite -{3}(sig_monPred_sig P) -{3}(sig_monPred_sig Q)
+      -f_equivI -sig_equivI !discrete_fun_equivI /=.
+    f_equiv=> j. rewrite prop_ext.
+    by rewrite !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
+  Qed.
+
+  Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP, @BiIndexBottom I bot} :
+    BiPlainlyExist PROP → BiPlainlyExist monPredI.
+  Proof.
+    split=> ? /=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1.
+    do 2 f_equiv. apply bi.forall_intro=> ?. by do 2 f_equiv.
+  Qed.
+
+  Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
+    BiEmbedPlainly PROP monPredI.
+  Proof.
+    split=> i. unseal. apply (anti_symm _).
+    - by apply bi.forall_intro.
+    - by rewrite (bi.forall_elim inhabitant).
+  Qed.
+
+  Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} :
+    BiBUpdPlainly monPredI.
+  Proof.
+    intros P. split=> /= i. unseal. by rewrite bi.forall_elim bupd_plainly.
+  Qed.
+
+  Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} :
+    BiFUpdPlainly monPredI.
+  Proof.
+    split; rewrite /bi_except_0; unseal.
+    - intros E E' P R. split=>/= i.
+      rewrite (bi.forall_elim i) bi.pure_True // bi.True_impl.
+      by rewrite (bi.forall_elim i) fupd_plainly_keep_l.
+    - intros E P. split=>/= i.
+      by rewrite (bi.forall_elim i) fupd_plainly_later.
+    - intros E A Φ. split=>/= i.
+      rewrite -fupd_plainly_forall_2. apply bi.forall_mono=> x.
+      by rewrite (bi.forall_elim i).
+  Qed.
+End instances.
+
+(** The final unseal tactic that also unfolds the BI layer. *)
+Module Import monPred.
+  Ltac unseal := rewrite !monPred_unseal /=.
+End monPred.
+
+Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
+  objective_at i j : P i ⊢ P j.
+Global Arguments Objective {_ _} _%_I.
+Global Arguments objective_at {_ _} _%_I {_}.
+Global Hint Mode Objective + + ! : typeclass_instances.
+Global Instance: Params (@Objective) 2 := {}.
+
+(** Primitive facts that cannot be deduced from the BI structure. *)
+Section bi_facts.
+  Context {I : biIndex} {PROP : bi}.
+  Local Notation monPred := (monPred I PROP).
+  Local Notation monPredI := (monPredI I PROP).
+  Local Notation monPred_at := (@monPred_at I PROP).
+  Local Notation BiIndexBottom := (@BiIndexBottom I).
+  Implicit Types i : I.
+  Implicit Types P Q : monPred.
+
+  (** monPred_at unfolding laws *)
+  Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i ⊣⊢ ⌜φ⌝.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_emp i : monPred_at emp i ⊣⊢ emp.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_and i P Q : (P ∧ Q) i ⊣⊢ P i ∧ Q i.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_or i P Q : (P ∨ Q) i ⊣⊢ P i ∨ Q i.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_impl i P Q : (P → Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j → Q j.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_forall {A} i (Φ : A → monPred) : (∀ x, Φ x) i ⊣⊢ ∀ x, Φ x i.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_exist {A} i (Φ : A → monPred) : (∃ x, Φ x) i ⊣⊢ ∃ x, Φ x i.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_sep i P Q : (P ∗ Q) i ⊣⊢ P i ∗ Q i.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_wand i P Q : (P -∗ Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j -∗ Q j.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_persistently i P : (<pers> P) i ⊣⊢ <pers> (P i).
+  Proof. by unseal. Qed.
+  Lemma monPred_at_in i j : monPred_at (monPred_in j) i ⊣⊢ ⌜j ⊑ i⌝.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_objectively i P : (<obj> P) i ⊣⊢ ∀ j, P j.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_subjectively i P : (<subj> P) i ⊣⊢ ∃ j, P j.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_persistently_if i p P : (<pers>?p P) i ⊣⊢ <pers>?p (P i).
+  Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
+  Lemma monPred_at_affinely i P : (<affine> P) i ⊣⊢ <affine> (P i).
+  Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
+  Lemma monPred_at_affinely_if i p P : (<affine>?p P) i ⊣⊢ <affine>?p (P i).
+  Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
+  Lemma monPred_at_intuitionistically i P : (□ P) i ⊣⊢ □ (P i).
+  Proof.
+    by rewrite /bi_intuitionistically monPred_at_affinely monPred_at_persistently.
+  Qed.
+  Lemma monPred_at_intuitionistically_if i p P : (□?p P) i ⊣⊢ □?p (P i).
+  Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
+  Lemma monPred_at_absorbingly i P : (<absorb> P) i ⊣⊢ <absorb> (P i).
+  Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
+  Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i ⊣⊢ <absorb>?p (P i).
+  Proof. destruct p=>//=. apply monPred_at_absorbingly. Qed.
+
+  Lemma monPred_wand_force i P Q : (P -∗ Q) i ⊢ (P i -∗ Q i).
+  Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
+  Lemma monPred_impl_force i P Q : (P → Q) i ⊢ (P i → Q i).
+  Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
+
+  (** Instances *)
+  Global Instance monPred_at_mono :
+    Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at.
+  Proof. by move=> ?? [?] ?? ->. Qed.
+  Global Instance monPred_at_flip_mono :
+    Proper (flip (⊢) ==> flip (⊑) ==> flip (⊢)) monPred_at.
+  Proof. solve_proper. Qed.
+
+  Global Instance monPred_in_proper (R : relation I) :
+    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
+    Proper (R ==> (≡)) (@monPred_in I PROP).
+  Proof. unseal. split. solve_proper. Qed.
+  Global Instance monPred_in_mono : Proper (flip (⊑) ==> (⊢)) (@monPred_in I PROP).
+  Proof. unseal. split. solve_proper. Qed.
+  Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
+  Proof. solve_proper. Qed.
+
+  Lemma monPred_persistent P : (∀ i, Persistent (P i)) → Persistent P.
+  Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
+  Lemma monPred_absorbing P : (∀ i, Absorbing (P i)) → Absorbing P.
+  Proof. intros HP. constructor=> i. rewrite /bi_absorbingly. unseal. apply HP. Qed.
+  Lemma monPred_affine P : (∀ i, Affine (P i)) → Affine P.
+  Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
+
+  Global Instance monPred_at_persistent P i : Persistent P → Persistent (P i).
+  Proof. move => [] /(_ i). by unseal. Qed.
+  Global Instance monPred_at_absorbing P i : Absorbing P → Absorbing (P i).
+  Proof. move => [] /(_ i). rewrite /Absorbing /bi_absorbingly. by unseal. Qed.
+  Global Instance monPred_at_affine P i : Affine P → Affine (P i).
+  Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
+
+  (** Note that [monPred_in] is *not* [Plain], because it depends on the index. *)
+  Global Instance monPred_in_persistent i : Persistent (@monPred_in I PROP i).
+  Proof. apply monPred_persistent=> j. rewrite monPred_at_in. apply _. Qed.
+  Global Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i).
+  Proof. apply monPred_absorbing=> j. rewrite monPred_at_in. apply _. Qed.
+
+  Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P.
+  Proof. by unseal. Qed.
+
+  Lemma monPred_emp_unfold : emp%I =@{monPred} ⎡emp : PROP⎤%I.
+  Proof. by unseal. Qed.
+  Lemma monPred_pure_unfold : bi_pure =@{_ → monPred} λ φ, ⎡ ⌜ φ ⌝ : PROP⎤%I.
+  Proof. by unseal. Qed.
+  Lemma monPred_objectively_unfold : monPred_objectively = λ P, ⎡∀ i, P i⎤%I.
+  Proof. by unseal. Qed.
+  Lemma monPred_subjectively_unfold : monPred_subjectively = λ P, ⎡∃ i, P i⎤%I.
+  Proof. by unseal. Qed.
+
+  Global Instance monPred_objectively_ne : NonExpansive (@monPred_objectively I PROP).
+  Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
+  Global Instance monPred_objectively_proper :
+    Proper ((≡) ==> (≡)) (@monPred_objectively I PROP).
+  Proof. apply (ne_proper _). Qed.
+  Lemma monPred_objectively_mono P Q : (P ⊢ Q) → (<obj> P ⊢ <obj> Q).
+  Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
+  Global Instance monPred_objectively_mono' :
+    Proper ((⊢) ==> (⊢)) (@monPred_objectively I PROP).
+  Proof. intros ???. by apply monPred_objectively_mono. Qed.
+  Global Instance monPred_objectively_flip_mono' :
+    Proper (flip (⊢) ==> flip (⊢)) (@monPred_objectively I PROP).
+  Proof. intros ???. by apply monPred_objectively_mono. Qed.
+
+  Global Instance monPred_objectively_persistent `{!BiPersistentlyForall PROP} P :
+    Persistent P → Persistent (<obj> P).
+  Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+  Global Instance monPred_objectively_absorbing P : Absorbing P → Absorbing (<obj> P).
+  Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+  Global Instance monPred_objectively_affine P : Affine P → Affine (<obj> P).
+  Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+
+  Global Instance monPred_subjectively_ne : NonExpansive (@monPred_subjectively I PROP).
+  Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
+  Global Instance monPred_subjectively_proper :
+    Proper ((≡) ==> (≡)) (@monPred_subjectively I PROP).
+  Proof. apply (ne_proper _). Qed.
+  Lemma monPred_subjectively_mono P Q : (P ⊢ Q) → <subj> P ⊢ <subj> Q.
+  Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
+  Global Instance monPred_subjectively_mono' :
+    Proper ((⊢) ==> (⊢)) (@monPred_subjectively I PROP).
+  Proof. intros ???. by apply monPred_subjectively_mono. Qed.
+  Global Instance monPred_subjectively_flip_mono' :
+    Proper (flip (⊢) ==> flip (⊢)) (@monPred_subjectively I PROP).
+  Proof. intros ???. by apply monPred_subjectively_mono. Qed.
+
+  Global Instance monPred_subjectively_persistent P :
+    Persistent P → Persistent (<subj> P).
+  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+  Global Instance monPred_subjectively_absorbing P :
+    Absorbing P → Absorbing (<subj> P).
+  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+  Global Instance monPred_subjectively_affine P : Affine P → Affine (<subj> P).
+  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+
+  (* Laws for monPred_objectively and of Objective. *)
+  Lemma monPred_objectively_elim P : <obj> P ⊢ P.
+  Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
+  Lemma monPred_objectively_idemp P : <obj> <obj> P ⊣⊢ <obj> P.
+  Proof.
+    apply bi.equiv_entails; split; [by apply monPred_objectively_elim|].
+    unseal. split=>i /=. by apply bi.forall_intro=>_.
+  Qed.
+
+  Lemma monPred_objectively_forall {A} (Φ : A → monPred) :
+    <obj> (∀ x, Φ x) ⊣⊢ ∀ x, <obj> (Φ x).
+  Proof.
+    unseal. split=>i. apply bi.equiv_entails; split=>/=;
+      do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
+  Qed.
+  Lemma monPred_objectively_and P Q : <obj> (P ∧ Q) ⊣⊢ <obj> P ∧ <obj> Q.
+  Proof.
+    unseal. split=>i. apply bi.equiv_entails; split=>/=.
+    - apply bi.and_intro; do 2 f_equiv.
+      + apply bi.and_elim_l.
+      + apply bi.and_elim_r.
+    - apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
+  Qed.
+  Lemma monPred_objectively_exist {A} (Φ : A → monPred) :
+    (∃ x, <obj> (Φ x)) ⊢ <obj> (∃ x, (Φ x)).
+  Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
+  Lemma monPred_objectively_or P Q : <obj> P ∨ <obj> Q ⊢ <obj> (P ∨ Q).
+  Proof.
+    apply bi.or_elim; f_equiv.
+    - apply bi.or_intro_l.
+    - apply bi.or_intro_r.
+  Qed.
+
+  Lemma monPred_objectively_sep_2 P Q : <obj> P ∗ <obj> Q ⊢ <obj> (P ∗ Q).
+  Proof.
+    unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
+  Qed.
+  Lemma monPred_objectively_sep `{BiIndexBottom bot} P Q :
+    <obj> (P ∗ Q) ⊣⊢ <obj> P ∗ <obj> Q.
+  Proof.
+    apply bi.equiv_entails, conj, monPred_objectively_sep_2. unseal. split=>i /=.
+    rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
+  Qed.
+  Lemma monPred_objectively_embed (P : PROP) : <obj> ⎡P⎤ ⊣⊢@{monPredI} ⎡P⎤.
+  Proof.
+    apply bi.equiv_entails; split; unseal; split=>i /=.
+    - by rewrite (bi.forall_elim inhabitant).
+    - by apply bi.forall_intro.
+  Qed.
+  Lemma monPred_objectively_emp : <obj> (emp : monPred) ⊣⊢ emp.
+  Proof. rewrite monPred_emp_unfold. apply monPred_objectively_embed. Qed.
+  Lemma monPred_objectively_pure φ : <obj> (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
+  Proof. rewrite monPred_pure_unfold. apply monPred_objectively_embed. Qed.
+
+  Lemma monPred_subjectively_intro P : P ⊢ <subj> P.
+  Proof. unseal. split=>?. apply bi.exist_intro. Qed.
+
+  Lemma monPred_subjectively_forall {A} (Φ : A → monPred) :
+    (<subj> (∀ x, Φ x)) ⊢ ∀ x, <subj> (Φ x).
+  Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
+  Lemma monPred_subjectively_and P Q : <subj> (P ∧ Q) ⊢ <subj> P ∧ <subj> Q.
+  Proof.
+    apply bi.and_intro; f_equiv.
+    - apply bi.and_elim_l.
+    - apply bi.and_elim_r.
+  Qed.
+  Lemma monPred_subjectively_exist {A} (Φ : A → monPred) :
+    <subj> (∃ x, Φ x) ⊣⊢ ∃ x, <subj> (Φ x).
+  Proof.
+    unseal. split=>i. apply bi.equiv_entails; split=>/=;
+      do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
+  Qed.
+  Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj> Q.
+  Proof. split=>i. unseal. apply bi.or_exist. Qed.
+
+  Lemma monPred_subjectively_sep P Q : <subj> (P ∗ Q) ⊢ <subj> P ∗ <subj> Q.
+  Proof.
+    unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
+  Qed.
+
+  Lemma monPred_subjectively_idemp P : <subj> <subj> P ⊣⊢ <subj> P.
+  Proof.
+    apply bi.equiv_entails; split; [|by apply monPred_subjectively_intro].
+    unseal. split=>i /=. by apply bi.exist_elim=>_.
+  Qed.
+
+  Lemma objective_objectively P `{!Objective P} : P ⊢ <obj> P.
+  Proof.
+    rewrite monPred_objectively_unfold /= embed_forall. apply bi.forall_intro=>?.
+    split=>?. unseal. apply objective_at, _.
+  Qed.
+  Lemma objective_subjectively P `{!Objective P} : <subj> P ⊢ P.
+  Proof.
+    rewrite monPred_subjectively_unfold /= embed_exist. apply bi.exist_elim=>?.
+    split=>?. unseal. apply objective_at, _.
+  Qed.
+
+  Global Instance embed_objective (P : PROP) : @Objective I PROP ⎡P⎤.
+  Proof. intros ??. by unseal. Qed.
+  Global Instance pure_objective φ : @Objective I PROP ⌜φ⌝.
+  Proof. intros ??. by unseal. Qed.
+  Global Instance emp_objective : @Objective I PROP emp.
+  Proof. intros ??. by unseal. Qed.
+  Global Instance objectively_objective P : Objective (<obj> P).
+  Proof. intros ??. by unseal. Qed.
+  Global Instance subjectively_objective P : Objective (<subj> P).
+  Proof. intros ??. by unseal. Qed.
+
+  Global Instance and_objective P Q `{!Objective P, !Objective Q} :
+    Objective (P ∧ Q).
+  Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
+  Global Instance or_objective P Q `{!Objective P, !Objective Q} :
+    Objective (P ∨ Q).
+  Proof. intros i j. by rewrite !monPred_at_or !(objective_at _ i j). Qed.
+  Global Instance impl_objective P Q `{!Objective P, !Objective Q} :
+    Objective (P → Q).
+  Proof.
+    intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
+    rewrite bi.forall_elim //. apply bi.forall_intro=> k.
+    rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
+    rewrite (objective_at Q i). by rewrite (objective_at P k).
+  Qed.
+  Global Instance forall_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
+    @Objective I PROP (∀ x, Φ x)%I.
+  Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
+  Global Instance exists_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
+    @Objective I PROP (∃ x, Φ x)%I.
+  Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
+
+  Global Instance sep_objective P Q `{!Objective P, !Objective Q} :
+    Objective (P ∗ Q).
+  Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
+  Global Instance wand_objective P Q `{!Objective P, !Objective Q} :
+    Objective (P -∗ Q).
+  Proof.
+    intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
+    rewrite bi.forall_elim //. apply bi.forall_intro=> k.
+    rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
+    rewrite (objective_at Q i). by rewrite (objective_at P k).
+  Qed.
+  Global Instance persistently_objective P `{!Objective P} : Objective (<pers> P).
+  Proof. intros i j. unseal. by rewrite objective_at. Qed.
+
+  Global Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
+  Proof. rewrite /bi_affinely. apply _. Qed.
+  Global Instance intuitionistically_objective P `{!Objective P} : Objective (□ P).
+  Proof. rewrite /bi_intuitionistically. apply _. Qed.
+  Global Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
+  Proof. rewrite /bi_absorbingly. apply _. Qed.
+  Global Instance persistently_if_objective P p `{!Objective P} :
+    Objective (<pers>?p P).
+  Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
+  Global Instance affinely_if_objective P p `{!Objective P} :
+    Objective (<affine>?p P).
+  Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
+  Global Instance absorbingly_if_objective P p `{!Objective P} :
+    Objective (<absorb>?p P).
+  Proof. rewrite /bi_absorbingly_if. destruct p; apply _. Qed.
+  Global Instance intuitionistically_if_objective P p `{!Objective P} :
+    Objective (□?p P).
+  Proof. rewrite /bi_intuitionistically_if. destruct p; apply _. Qed.
+
+  (** monPred_in *)
+  Lemma monPred_in_intro P : P ⊢ ∃ i, monPred_in i ∧ ⎡P i⎤.
+  Proof.
+    unseal. split=>i /=.
+    rewrite /= -(bi.exist_intro i). apply bi.and_intro=>//. by apply bi.pure_intro.
+  Qed.
+  Lemma monPred_in_elim P i : monPred_in i ⊢ ⎡P i⎤ → P .
+  Proof.
+    apply bi.impl_intro_r. unseal. split=>i' /=.
+    eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
+  Qed.
+
+  (** Big op *)
+  Global Instance monPred_at_monoid_and_homomorphism i :
+    MonoidHomomorphism bi_and bi_and (≡) (flip monPred_at i).
+  Proof.
+    split; [split|]; try apply _; [apply monPred_at_and | apply monPred_at_pure].
+  Qed.
+  Global Instance monPred_at_monoid_or_homomorphism i :
+    MonoidHomomorphism bi_or bi_or (≡) (flip monPred_at i).
+  Proof.
+    split; [split|]; try apply _; [apply monPred_at_or | apply monPred_at_pure].
+  Qed.
+  Global Instance monPred_at_monoid_sep_homomorphism i :
+    MonoidHomomorphism bi_sep bi_sep (≡) (flip monPred_at i).
+  Proof.
+    split; [split|]; try apply _; [apply monPred_at_sep | apply monPred_at_emp].
+  Qed.
+
+  Lemma monPred_at_big_sepL {A} i (Φ : nat → A → monPred) l :
+    ([∗ list] k↦x ∈ l, Φ k x) i ⊣⊢ [∗ list] k↦x ∈ l, Φ k x i.
+  Proof. apply (big_opL_commute (flip monPred_at i)). Qed.
+  Lemma monPred_at_big_sepM `{Countable K} {A} i (Φ : K → A → monPred) (m : gmap K A) :
+    ([∗ map] k↦x ∈ m, Φ k x) i ⊣⊢ [∗ map] k↦x ∈ m, Φ k x i.
+  Proof. apply (big_opM_commute (flip monPred_at i)). Qed.
+  Lemma monPred_at_big_sepS `{Countable A} i (Φ : A → monPred) (X : gset A) :
+    ([∗ set] y ∈ X, Φ y) i ⊣⊢ [∗ set] y ∈ X, Φ y i.
+  Proof. apply (big_opS_commute (flip monPred_at i)). Qed.
+  Lemma monPred_at_big_sepMS `{Countable A} i (Φ : A → monPred) (X : gmultiset A) :
+    ([∗ mset] y ∈ X, Φ y) i ⊣⊢ ([∗ mset] y ∈ X, Φ y i).
+  Proof. apply (big_opMS_commute (flip monPred_at i)). Qed.
+
+  Global Instance monPred_objectively_monoid_and_homomorphism :
+    MonoidHomomorphism bi_and bi_and (≡) (@monPred_objectively I PROP).
+  Proof.
+    split; [split|]; try apply _.
+    - apply monPred_objectively_and.
+    - apply monPred_objectively_pure.
+  Qed.
+  Global Instance monPred_objectively_monoid_sep_entails_homomorphism :
+    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_objectively I PROP).
+  Proof.
+    split; [split|]; try apply _.
+    - apply monPred_objectively_sep_2.
+    - by rewrite monPred_objectively_emp.
+  Qed.
+  Global Instance monPred_objectively_monoid_sep_homomorphism `{BiIndexBottom bot} :
+    MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_objectively I PROP).
+  Proof.
+    split; [split|]; try apply _.
+    - apply monPred_objectively_sep.
+    - by rewrite monPred_objectively_emp.
+  Qed.
+
+  Lemma monPred_objectively_big_sepL_entails {A} (Φ : nat → A → monPred) l :
+    ([∗ list] k↦x ∈ l, <obj> (Φ k x)) ⊢ <obj> ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. apply (big_opL_commute monPred_objectively (R:=flip (⊢))). Qed.
+  Lemma monPred_objectively_big_sepM_entails
+        `{Countable K} {A} (Φ : K → A → monPred) (m : gmap K A) :
+    ([∗ map] k↦x ∈ m, <obj> (Φ k x)) ⊢ <obj> ([∗ map] k↦x ∈ m, Φ k x).
+  Proof. apply (big_opM_commute monPred_objectively (R:=flip (⊢))). Qed.
+  Lemma monPred_objectively_big_sepS_entails `{Countable A}
+      (Φ : A → monPred) (X : gset A) :
+    ([∗ set] y ∈ X, <obj> (Φ y)) ⊢ <obj> ([∗ set] y ∈ X, Φ y).
+  Proof. apply (big_opS_commute monPred_objectively (R:=flip (⊢))). Qed.
+  Lemma monPred_objectively_big_sepMS_entails `{Countable A}
+      (Φ : A → monPred) (X : gmultiset A) :
+    ([∗ mset] y ∈ X, <obj> (Φ y)) ⊢ <obj> ([∗ mset] y ∈ X, Φ y).
+  Proof. apply (big_opMS_commute monPred_objectively (R:=flip (⊢))). Qed.
+
+  Lemma monPred_objectively_big_sepL `{BiIndexBottom bot} {A}
+      (Φ : nat → A → monPred) l :
+    <obj> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, <obj> (Φ k x)).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma monPred_objectively_big_sepM `{BiIndexBottom bot} `{Countable K} {A}
+        (Φ : K → A → monPred) (m : gmap K A) :
+    <obj> ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, <obj> (Φ k x)).
+  Proof. apply (big_opM_commute _). Qed.
+  Lemma monPred_objectively_big_sepS `{BiIndexBottom bot} `{Countable A}
+        (Φ : A → monPred) (X : gset A) :
+    <obj> ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, <obj> (Φ y)).
+  Proof. apply (big_opS_commute _). Qed.
+  Lemma monPred_objectively_big_sepMS `{BiIndexBottom bot} `{Countable A}
+        (Φ : A → monPred) (X : gmultiset A) :
+    <obj> ([∗ mset] y ∈ X, Φ y) ⊣⊢  ([∗ mset] y ∈ X, <obj> (Φ y)).
+  Proof. apply (big_opMS_commute _). Qed.
+
+  Global Instance big_sepL_objective {A} (l : list A) Φ `{∀ n x, Objective (Φ n x)} :
+    @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x).
+  Proof. generalize dependent Φ. induction l=>/=; apply _. Qed.
+  Global Instance big_sepM_objective `{Countable K} {A}
+         (Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Objective (Φ k x)} :
+    Objective ([∗ map] k↦x ∈ m, Φ k x).
+  Proof.
+    intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply objective_at.
+  Qed.
+  Global Instance big_sepS_objective `{Countable A} (Φ : A → monPred)
+         (X : gset A) `{∀ y, Objective (Φ y)} :
+    Objective ([∗ set] y ∈ X, Φ y).
+  Proof.
+    intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply objective_at.
+  Qed.
+  Global Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
+         (X : gmultiset A) `{∀ y, Objective (Φ y)} :
+    Objective ([∗ mset] y ∈ X, Φ y).
+  Proof.
+    intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at.
+  Qed.
+
+  (** BUpd *)
+  Lemma monPred_at_bupd `{!BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
+  Proof. by rewrite monPred_bupd_unseal. Qed.
+
+  Global Instance bupd_objective `{!BiBUpd PROP} P `{!Objective P} :
+    Objective (|==> P).
+  Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
+
+  (** Later *)
+  Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
+  Proof. move => [] /(_ i). rewrite /Timeless /bi_except_0. by unseal. Qed.
+  Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
+  Proof. split => ? /=. rewrite /bi_except_0. unseal. apply timeless, _. Qed.
+  Global Instance monPred_objectively_timeless P : Timeless P → Timeless (<obj> P).
+  Proof.
+    move=>[]. rewrite /Timeless /bi_except_0. unseal=>Hti. split=> ? /=.
+    by apply timeless, bi.forall_timeless.
+  Qed.
+  Global Instance monPred_subjectively_timeless P : Timeless P → Timeless (<subj> P).
+  Proof.
+    move=>[]. rewrite /Timeless /bi_except_0. unseal=>Hti. split=> ? /=.
+    by apply timeless, bi.exist_timeless.
+  Qed.
+
+  Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
+  Proof. by unseal. Qed.
+  Lemma monPred_at_laterN n i P : (▷^n P) i ⊣⊢ ▷^n P i.
+  Proof. induction n as [|? IHn]; first done. rewrite /= monPred_at_later IHn //. Qed.
+  Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
+  Proof. rewrite /bi_except_0. by unseal. Qed.
+
+  Global Instance later_objective P `{!Objective P} : Objective (▷ P).
+  Proof. intros ??. unseal. by rewrite objective_at. Qed.
+  Global Instance laterN_objective P `{!Objective P} n : Objective (▷^n P).
+  Proof. induction n; apply _. Qed.
+  Global Instance except0_objective P `{!Objective P} : Objective (◇ P).
+  Proof. rewrite /bi_except_0. apply _. Qed.
+
+  (** Internal equality *)
+  Lemma monPred_internal_eq_unfold `{!BiInternalEq PROP} :
+    @internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
+  Proof. rewrite monPred_internal_eq_unseal. by unseal. Qed.
+
+  Lemma monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} i (a b : A) :
+    @monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
+  Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
+
+  Lemma monPred_equivI `{!BiInternalEq PROP'} P Q :
+    P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
+  Proof.
+    apply bi.equiv_entails. split.
+    - apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
+    - by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
+                 -f_equivI -sig_equivI !discrete_fun_equivI.
+  Qed.
+
+  Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofe} (x y : A) :
+    @Objective I PROP (x ≡ y).
+  Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
+
+  (** FUpd  *)
+  Lemma monPred_at_fupd `{!BiFUpd PROP} i E1 E2 P :
+    (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
+  Proof. by rewrite monPred_fupd_unseal. Qed.
+
+  Global Instance fupd_objective E1 E2 P `{!Objective P} `{!BiFUpd PROP} :
+    Objective (|={E1,E2}=> P).
+  Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
+
+  (** Plainly *)
+  Lemma monPred_plainly_unfold `{!BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■ (P i) ⎤%I.
+  Proof. by rewrite monPred_plainly_unseal monPred_embed_unseal. Qed.
+  Lemma monPred_at_plainly `{!BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
+  Proof. by rewrite monPred_plainly_unseal. Qed.
+
+  Global Instance monPred_at_plain `{!BiPlainly PROP} P i : Plain P → Plain (P i).
+  Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
+
+  Global Instance plainly_objective `{!BiPlainly PROP} P : Objective (■ P).
+  Proof. rewrite monPred_plainly_unfold. apply _. Qed.
+  Global Instance plainly_if_objective `{!BiPlainly PROP} P p `{!Objective P} :
+    Objective (■?p P).
+  Proof. rewrite /plainly_if. destruct p; apply _. Qed.
+
+  Global Instance monPred_objectively_plain `{!BiPlainly PROP} P :
+    Plain P → Plain (<obj> P).
+  Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+  Global Instance monPred_subjectively_plain `{!BiPlainly PROP} P :
+    Plain P → Plain (<subj> P).
+  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+End bi_facts.

iris/bi/notation.v

+From iris.prelude Require Import options.
+(** Just reserve the notation. *)
+
+(** * Turnstiles *)
+Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "(⊢)".
+Reserved Notation "'(⊢@{' PROP } )".
+Reserved Notation "( P ⊣⊢.)".
+Reserved Notation "(.⊣⊢ Q )".
+
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
+Reserved Notation "(⊣⊢)".
+Reserved Notation "'(⊣⊢@{' PROP } )".
+Reserved Notation "(.⊢ Q )".
+Reserved Notation "( P ⊢.)".
+
+Reserved Notation "⊢ Q" (at level 20, Q at level 200).
+Reserved Notation "'⊢@{' PROP } Q" (at level 20, Q at level 200).
+(** The definition must coincide with "'⊢@{' PROP } Q". *)
+Reserved Notation "'(⊢@{' PROP } Q )".
+(**
+Rationale:
+Notation [( '⊢@{' PROP } )] prevents parsing [(⊢@{PROP} Q)] using the
+[⊢@{PROP} Q] notation; since the latter parse arises from composing two
+notations, it is missed by the automatic left-factorization.
+
+To fix that, we force left-factorization by explicitly composing parentheses with
+['⊢@{' PROP } Q] into the new notation [( '⊢@{' PROP } Q )],
+which successfully undergoes automatic left-factoring. *)
+
+
+(** * BI connectives *)
+Reserved Notation "'emp'".
+Reserved Notation "'⌜' φ '⌝'" (at level 0, φ at level 200, format "⌜ φ ⌝").
+Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").
+Reserved Notation "P -∗ Q"
+  (at level 99, Q at level 200, right associativity,
+   format "'[' P  -∗  '/' '[' Q ']' ']'").
+
+Reserved Notation "⎡ P ⎤".
+
+(** Modalities *)
+Reserved Notation "'<pers>' P" (at level 20, right associativity).
+Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<pers>?' p  P").
+
+Reserved Notation "▷ P" (at level 20, right associativity).
+Reserved Notation "▷? p P" (at level 20, p at level 9, P at level 20,
+   format "▷? p  P").
+Reserved Notation "▷^ n P" (at level 20, n at level 9, P at level 20,
+   format "▷^ n  P").
+
+Reserved Infix "∗-∗" (at level 95, no associativity).
+
+Reserved Notation "'<affine>' P" (at level 20, right associativity).
+Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<affine>?' p  P").
+
+Reserved Notation "'<absorb>' P" (at level 20, right associativity).
+Reserved Notation "'<absorb>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<absorb>?' p  P").
+
+Reserved Notation "□ P" (at level 20, right associativity).
+Reserved Notation "'□?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'□?' p  P").
+
+Reserved Notation "◇ P" (at level 20, right associativity).
+
+Reserved Notation "■ P" (at level 20, right associativity).
+Reserved Notation "■? p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "■? p  P").
+
+Reserved Notation "'<obj>' P" (at level 20, right associativity).
+Reserved Notation "'<subj>' P" (at level 20, right associativity).
+
+(** * Update modalities *)
+Reserved Notation "|==> Q" (at level 99, Q at level 200, format "'[  ' |==>  '/' Q ']'").
+Reserved Notation "P ==∗ Q"
+  (at level 99, Q at level 200, format "'[' P  ==∗  '/' Q ']'").
+
+Reserved Notation "|={ E1 , E2 }=> Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "'[  ' |={ E1 , E2 }=>  '/' Q ']'").
+Reserved Notation "P ={ E1 , E2 }=∗ Q"
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "'[' P  ={ E1 , E2 }=∗  '/' '[' Q ']' ']'").
+
+Reserved Notation "|={ E }=> Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "'[  ' |={ E }=>  '/' Q ']'").
+Reserved Notation "P ={ E }=∗ Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "'[' P  ={ E }=∗  '/' '[' Q ']' ']'").
+
+(** Step-taking fancy updates *)
+Reserved Notation "|={ E1 } [ E2 ]▷=> Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "'[  ' |={ E1 } [ E2 ]▷=>  '/' Q ']'").
+Reserved Notation "P ={ E1 } [ E2 ]▷=∗ Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "'[' P  ={ E1 } [ E2 ]▷=∗  '/' '[' Q ']' ']'").
+Reserved Notation "|={ E }▷=> Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "'[  ' |={ E }▷=>  '/' Q ']'").
+Reserved Notation "P ={ E }▷=∗ Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "'[' P  ={ E }▷=∗  '/' '[' Q ']' ']'").
+
+(** Multi-step-taking fancy updates *)
+Reserved Notation "|={ E1 } [ E2 ]▷=>^ n Q"
+  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
+   format "'[  ' |={ E1 } [ E2 ]▷=>^ n  '/' Q ']'").
+Reserved Notation "P ={ E1 } [ E2 ]▷=∗^ n Q"
+  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
+   format "'[' P  ={ E1 } [ E2 ]▷=∗^ n  '/' '[' Q ']' ']'").
+Reserved Notation "|={ E }▷=>^ n Q"
+  (at level 99, E at level 50, n at level 9, Q at level 200,
+   format "'[  ' |={ E }▷=>^ n  '/' Q ']'").
+Reserved Notation "P ={ E }▷=∗^ n Q"
+  (at level 99, E at level 50, n at level 9, Q at level 200,
+   format "'[' P  ={ E }▷=∗^ n  '/' '[' Q ']' ']'").
+
+(** * Big Ops *)
+Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
+  (at level 200, l at level 10, k binder, x binder, right associativity,
+   format "[∗  list]  k ↦ x  ∈  l ,  P").
+Reserved Notation "'[∗' 'list]' x ∈ l , P"
+  (at level 200, l at level 10, x binder, right associativity,
+   format "[∗  list]  x  ∈  l ,  P").
+
+Reserved Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P"
+  (at level 200, l1, l2 at level 10, k binder, x1 binder, x2 binder,
+   right associativity,
+   format "[∗  list]  k ↦ x1 ; x2  ∈  l1 ; l2 ,  P").
+Reserved Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P"
+  (at level 200, l1, l2 at level 10, x1 binder, x2 binder, right associativity,
+   format "[∗  list]  x1 ; x2  ∈  l1 ; l2 ,  P").
+
+Reserved Notation "'[∗]' Ps" (at level 20).
+
+Reserved Notation "'[∧' 'list]' k ↦ x ∈ l , P"
+  (at level 200, l at level 10, k binder, x binder, right associativity,
+   format "[∧  list]  k ↦ x  ∈  l ,  P").
+Reserved Notation "'[∧' 'list]' x ∈ l , P"
+  (at level 200, l at level 10, x binder, right associativity,
+   format "[∧  list]  x  ∈  l ,  P").
+
+Reserved Notation "'[∧]' Ps" (at level 20).
+
+Reserved Notation "'[∨' 'list]' k ↦ x ∈ l , P"
+  (at level 200, l at level 10, k binder, x binder, right associativity,
+   format "[∨  list]  k ↦ x  ∈  l ,  P").
+Reserved Notation "'[∨' 'list]' x ∈ l , P"
+  (at level 200, l at level 10, x binder, right associativity,
+   format "[∨  list]  x  ∈  l ,  P").
+
+Reserved Notation "'[∨]' Ps" (at level 20).
+
+Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
+  (at level 200, m at level 10, k binder, x binder, right associativity,
+   format "[∗  map]  k ↦ x  ∈  m ,  P").
+Reserved Notation "'[∗' 'map]' x ∈ m , P"
+  (at level 200, m at level 10, x binder, right associativity,
+   format "[∗  map]  x  ∈  m ,  P").
+
+Reserved Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
+  (at level 200, m1, m2 at level 10,
+   k binder, x1 binder, x2 binder, right associativity,
+   format "[∗  map]  k ↦ x1 ; x2  ∈  m1 ; m2 ,  P").
+Reserved Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
+  (at level 200, m1, m2 at level 10, x1 binder, x2 binder, right associativity,
+   format "[∗  map]  x1 ; x2  ∈  m1 ; m2 ,  P").
+
+Reserved Notation "'[∧' 'map]' k ↦ x ∈ m , P"
+  (at level 200, m at level 10, k binder, x binder, right associativity,
+   format "[∧  map]  k ↦ x  ∈  m ,  P").
+Reserved Notation "'[∧' 'map]' x ∈ m , P"
+  (at level 200, m at level 10, x binder, right associativity,
+   format "[∧  map]  x  ∈  m ,  P").
+
+Reserved Notation "'[∗' 'set]' x ∈ X , P"
+  (at level 200, X at level 10, x binder, right associativity,
+   format "[∗  set]  x  ∈  X ,  P").
+
+Reserved Notation "'[∗' 'mset]' x ∈ X , P"
+  (at level 200, X at level 10, x binder, right associativity,
+   format "[∗  mset]  x  ∈  X ,  P").
+
+(** Define the scope *)
+Declare Scope bi_scope.
+Delimit Scope bi_scope with I.