From ce22aecad8ff7c42f11fd09df530da96ac6e2759 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 4 Mar 2023 15:51:52 +0100
Subject: [PATCH] Indent some sections.

---
 iris/base_logic/algebra.v   | 593 ++++++++++++------------
 iris/base_logic/bi.v        | 132 +++---
 iris/base_logic/derived.v   | 238 +++++-----
 iris/base_logic/proofmode.v |  61 ++-
 iris/base_logic/upred.v     | 882 ++++++++++++++++++------------------
 iris/si_logic/siprop.v      | 366 +++++++--------
 6 files changed, 1134 insertions(+), 1138 deletions(-)

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 98857b9cb..34fba7aef 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -7,305 +7,304 @@ From iris.prelude Require Import options.
 Local Coercion uPred_holds : uPred >-> Funclass.
 
 Section upred.
-Context {M : ucmra}.
-
-(* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
-Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-Notation "⊢ Q" := (bi_entails (PROP:=uPredI M) True Q).
-
-Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. by uPred.unseal. Qed.
-Lemma option_validI {A : cmra} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-Proof. uPred.unseal. by destruct mx. Qed.
-Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
-  ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. by uPred.unseal. Qed.
-
-Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
-Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
-
-Section gmap_ofe.
-  Context `{Countable K} {A : ofe}.
-  Implicit Types m : gmap K A.
-  Implicit Types i : K.
-
-  Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
-  Proof. by uPred.unseal. Qed.
-End gmap_ofe.
+  Context {M : ucmra}.
 
-Section gmap_cmra.
-  Context `{Countable K} {A : cmra}.
-  Implicit Types m : gmap K A.
+  (* Force implicit argument M *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
+  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+  Notation "⊢ Q" := (bi_entails (PROP:=uPredI M) True Q).
 
-  Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
+  Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+  Proof. by uPred.unseal. Qed.
+  Lemma option_validI {A : cmra} (mx : option A) :
+    ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
+  Proof. uPred.unseal. by destruct mx. Qed.
+  Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
+    ✓ g ⊣⊢ ∀ i, ✓ g i.
   Proof. by uPred.unseal. Qed.
-  Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
-  Proof.
-    rewrite gmap_validI. apply: anti_symm.
-    - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
-    - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
-      + rewrite lookup_singleton option_validI. done.
-      + rewrite lookup_singleton_ne // option_validI.
-        apply bi.True_intro.
-  Qed.
-End gmap_cmra.
-
-Section list_ofe.
-  Context {A : ofe}.
-  Implicit Types l : list A.
-
-  Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
-  Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
-End list_ofe.
-
-Section excl.
-  Context {A : ofe}.
-  Implicit Types a b : A.
-  Implicit Types x y : excl A.
-
-  Lemma excl_equivI x y :
-    x ≡ y ⊣⊢ match x, y with
-                        | Excl a, Excl b => a ≡ b
-                        | ExclBot, ExclBot => True
-                        | _, _ => False
-                        end.
-  Proof.
-    uPred.unseal. do 2 split.
-    - by destruct 1.
-    - by destruct x, y; try constructor.
-  Qed.
-  Lemma excl_validI x :
-    ✓ x ⊣⊢ if x is ExclBot then False else True.
-  Proof. uPred.unseal. by destruct x. Qed.
-End excl.
-
-Section agree.
-  Context {A : ofe}.
-  Implicit Types a b : A.
-  Implicit Types x y : agree A.
-
-  Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
-  Proof.
-    uPred.unseal. do 2 split.
-    - intros Hx. exact: (inj to_agree).
-    - intros Hx. exact: to_agree_ne.
-  Qed.
-  Lemma agree_validI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
-  Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
-
-  Lemma to_agree_validI a : ⊢ ✓ to_agree a.
-  Proof. uPred.unseal; done. Qed.
-  Lemma to_agree_op_validI a b : ✓ (to_agree a ⋅ to_agree b) ⊣⊢ a ≡ b.
-  Proof.
-    apply bi.entails_anti_sym.
-    - rewrite agree_validI. by rewrite agree_equivI.
-    - pose (Ψ := (λ x : A, ✓ (to_agree a ⋅ to_agree x) : uPred M)%I).
-      assert (NonExpansive Ψ) as ? by solve_proper.
-      rewrite (internal_eq_rewrite a b Ψ).
-      eapply bi.impl_elim; first reflexivity.
-      etrans; first apply bi.True_intro.
-      subst Ψ; simpl.
-      rewrite agree_idemp. apply to_agree_validI.
-  Qed.
-
-  Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
-  Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
-End agree.
-
-Section csum_ofe.
-  Context {A B : ofe}.
-  Implicit Types a : A.
-  Implicit Types b : B.
-
-  Lemma csum_equivI (x y : csum A B) :
-    x ≡ y ⊣⊢ match x, y with
-                        | Cinl a, Cinl a' => a ≡ a'
-                        | Cinr b, Cinr b' => b ≡ b'
-                        | CsumBot, CsumBot => True
-                        | _, _ => False
-                        end.
-  Proof.
-    uPred.unseal; do 2 split; first by destruct 1.
-      by destruct x, y; try destruct 1; try constructor.
-  Qed.
-End csum_ofe.
-
-Section csum_cmra.
-  Context {A B : cmra}.
-  Implicit Types a : A.
-  Implicit Types b : B.
-
-  Lemma csum_validI (x : csum A B) :
-    ✓ x ⊣⊢ match x with
-                      | Cinl a => ✓ a
-                      | Cinr b => ✓ b
-                      | CsumBot => False
-                      end.
-  Proof. uPred.unseal. by destruct x. Qed.
-End csum_cmra.
-
-Section view.
-  Context {A B} (rel : view_rel A B).
-  Implicit Types a : A.
-  Implicit Types ag : option (frac * agree A).
-  Implicit Types b : B.
-  Implicit Types x y : view rel.
-
-  Lemma view_both_dfrac_validI_1 (relI : uPred M) dq a b :
-    (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ relI.
-  Proof.
-    intros Hrel. uPred.unseal. split=> n x _ /=.
-    rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
-  Qed.
-  Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
-    (∀ n (x : M), relI n x → rel n a b) →
-    ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
-  Proof.
-    intros Hrel. uPred.unseal. split=> n x _ /=.
-    rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
-  Qed.
-  Lemma view_both_dfrac_validI (relI : uPred M) dq a b :
-    (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
-  Proof.
-    intros. apply (anti_symm _);
-      [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
-  Qed.
-
-  Lemma view_both_validI_1 (relI : uPred M) a b :
-    (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V a ⋅ ◯V b : view rel) ⊢ relI.
-  Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
-  Lemma view_both_validI_2 (relI : uPred M) a b :
-    (∀ n (x : M), relI n x → rel n a b) →
-    relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
-  Proof.
-    intros. rewrite -view_both_dfrac_validI_2 //.
-    apply bi.and_intro; [|done]. by apply bi.pure_intro.
-  Qed.
-  Lemma view_both_validI (relI : uPred M) a b :
-    (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ relI.
-  Proof.
-    intros. apply (anti_symm _);
-      [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
-  Qed.
-
-  Lemma view_auth_dfrac_validI (relI : uPred M) dq a :
-    (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
-  Proof.
-    intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
-  Qed.
-  Lemma view_auth_validI (relI : uPred M) a :
-    (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V a : view rel) ⊣⊢ relI.
-  Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
-
-  Lemma view_frag_validI (relI : uPred M) b :
-    (∀ n (x : M), relI n x ↔ ∃ a, rel n a b) →
-    ✓ (◯V b : view rel) ⊣⊢ relI.
-  Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
-End view.
-
-Section auth.
-  Context {A : ucmra}.
-  Implicit Types a b : A.
-  Implicit Types x y : auth A.
-
-  Lemma auth_auth_dfrac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
-  Proof.
-    apply view_auth_dfrac_validI=> n. uPred.unseal; split; [|by intros [??]].
-    split; [|done]. apply ucmra_unit_leastN.
-  Qed.
-  Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
-  Proof.
-    by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
-  Qed.
-
-  Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
-  Proof.
-    apply view_frag_validI=> n x.
-    rewrite auth_view_rel_exists. by uPred.unseal.
-  Qed.
-
-  Lemma auth_both_dfrac_validI dq a b :
-    ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-  Proof. apply view_both_dfrac_validI=> n. by uPred.unseal. Qed.
-  Lemma auth_both_validI a b :
-    ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-  Proof.
-    by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
-  Qed.
-
-End auth.
-
-Section excl_auth.
-  Context {A : ofe}.
-  Implicit Types a b : A.
-
-  Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
-  Proof.
-    rewrite auth_both_validI bi.and_elim_l.
-    apply bi.exist_elim=> -[[c|]|];
-      by rewrite option_equivI /= excl_equivI //= bi.False_elim.
-  Qed.
-End excl_auth.
-
-Section dfrac_agree.
-  Context {A : ofe}.
-  Implicit Types a b : A.
-
-  Lemma dfrac_agree_validI dq a : ✓ (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
-  Proof.
-    rewrite prod_validI /= uPred.discrete_valid. apply bi.entails_anti_sym.
-    - by rewrite bi.and_elim_l.
-    - apply bi.and_intro; first done. etrans; last apply to_agree_validI.
-      apply bi.True_intro.
-  Qed.
-
-  Lemma dfrac_agree_validI_2 dq1 dq2 a b :
-    ✓ (to_dfrac_agree dq1 a ⋅ to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 ⋅ dq2)⌝ ∧ (a ≡ b).
-  Proof.
-    rewrite prod_validI /= uPred.discrete_valid to_agree_op_validI //.
-  Qed.
-
-  Lemma frac_agree_validI q a : ✓ (to_frac_agree q a) ⊣⊢ ⌜(q ≤ 1)%Qp⌝.
-  Proof.
-    rewrite dfrac_agree_validI dfrac_valid_own //.
-  Qed.
-
-  Lemma frac_agree_validI_2 q1 q2 a b :
-    ✓ (to_frac_agree q1 a ⋅ to_frac_agree q2 b) ⊣⊢ ⌜(q1 + q2 ≤ 1)%Qp⌝ ∧ (a ≡ b).
-  Proof.
-    rewrite dfrac_agree_validI_2 dfrac_valid_own //.
-  Qed.
-End dfrac_agree.
-
-Section gmap_view.
-  Context {K : Type} `{Countable K} {V : ofe}.
-  Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
-
-  Lemma gmap_view_both_validI m k dq v :
-    ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
-    ✓ dq ∧ m !! k ≡ Some v.
-  Proof.
-    rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
-    intros n a. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
-  Qed.
-
-  Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
-    ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
-  Proof.
-    rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
-    rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
-    rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
-  Qed.
-
-End gmap_view.
 
+  Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
+  Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
+
+  Section gmap_ofe.
+    Context `{Countable K} {A : ofe}.
+    Implicit Types m : gmap K A.
+    Implicit Types i : K.
+
+    Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
+    Proof. by uPred.unseal. Qed.
+  End gmap_ofe.
+
+  Section gmap_cmra.
+    Context `{Countable K} {A : cmra}.
+    Implicit Types m : gmap K A.
+
+    Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
+    Proof. by uPred.unseal. Qed.
+    Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
+    Proof.
+      rewrite gmap_validI. apply: anti_symm.
+      - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
+      - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
+        + rewrite lookup_singleton option_validI. done.
+        + rewrite lookup_singleton_ne // option_validI.
+          apply bi.True_intro.
+    Qed.
+  End gmap_cmra.
+
+  Section list_ofe.
+    Context {A : ofe}.
+    Implicit Types l : list A.
+
+    Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
+    Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
+  End list_ofe.
+
+  Section excl.
+    Context {A : ofe}.
+    Implicit Types a b : A.
+    Implicit Types x y : excl A.
+
+    Lemma excl_equivI x y :
+      x ≡ y ⊣⊢ match x, y with
+                          | Excl a, Excl b => a ≡ b
+                          | ExclBot, ExclBot => True
+                          | _, _ => False
+                          end.
+    Proof.
+      uPred.unseal. do 2 split.
+      - by destruct 1.
+      - by destruct x, y; try constructor.
+    Qed.
+    Lemma excl_validI x :
+      ✓ x ⊣⊢ if x is ExclBot then False else True.
+    Proof. uPred.unseal. by destruct x. Qed.
+  End excl.
+
+  Section agree.
+    Context {A : ofe}.
+    Implicit Types a b : A.
+    Implicit Types x y : agree A.
+
+    Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
+    Proof.
+      uPred.unseal. do 2 split.
+      - intros Hx. exact: (inj to_agree).
+      - intros Hx. exact: to_agree_ne.
+    Qed.
+    Lemma agree_validI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
+    Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
+
+    Lemma to_agree_validI a : ⊢ ✓ to_agree a.
+    Proof. uPred.unseal; done. Qed.
+    Lemma to_agree_op_validI a b : ✓ (to_agree a ⋅ to_agree b) ⊣⊢ a ≡ b.
+    Proof.
+      apply bi.entails_anti_sym.
+      - rewrite agree_validI. by rewrite agree_equivI.
+      - pose (Ψ := (λ x : A, ✓ (to_agree a ⋅ to_agree x) : uPred M)%I).
+        assert (NonExpansive Ψ) as ? by solve_proper.
+        rewrite (internal_eq_rewrite a b Ψ).
+        eapply bi.impl_elim; first reflexivity.
+        etrans; first apply bi.True_intro.
+        subst Ψ; simpl.
+        rewrite agree_idemp. apply to_agree_validI.
+    Qed.
+
+    Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
+    Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
+  End agree.
+
+  Section csum_ofe.
+    Context {A B : ofe}.
+    Implicit Types a : A.
+    Implicit Types b : B.
+
+    Lemma csum_equivI (x y : csum A B) :
+      x ≡ y ⊣⊢ match x, y with
+                          | Cinl a, Cinl a' => a ≡ a'
+                          | Cinr b, Cinr b' => b ≡ b'
+                          | CsumBot, CsumBot => True
+                          | _, _ => False
+                          end.
+    Proof.
+      uPred.unseal; do 2 split; first by destruct 1.
+        by destruct x, y; try destruct 1; try constructor.
+    Qed.
+  End csum_ofe.
+
+  Section csum_cmra.
+    Context {A B : cmra}.
+    Implicit Types a : A.
+    Implicit Types b : B.
+
+    Lemma csum_validI (x : csum A B) :
+      ✓ x ⊣⊢ match x with
+                        | Cinl a => ✓ a
+                        | Cinr b => ✓ b
+                        | CsumBot => False
+                        end.
+    Proof. uPred.unseal. by destruct x. Qed.
+  End csum_cmra.
+
+  Section view.
+    Context {A B} (rel : view_rel A B).
+    Implicit Types a : A.
+    Implicit Types ag : option (frac * agree A).
+    Implicit Types b : B.
+    Implicit Types x y : view rel.
+
+    Lemma view_both_dfrac_validI_1 (relI : uPred M) dq a b :
+      (∀ n (x : M), rel n a b → relI n x) →
+      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ relI.
+    Proof.
+      intros Hrel. uPred.unseal. split=> n x _ /=.
+      rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
+    Qed.
+    Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
+      (∀ n (x : M), relI n x → rel n a b) →
+      ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
+    Proof.
+      intros Hrel. uPred.unseal. split=> n x _ /=.
+      rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
+    Qed.
+    Lemma view_both_dfrac_validI (relI : uPred M) dq a b :
+      (∀ n (x : M), rel n a b ↔ relI n x) →
+      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+    Proof.
+      intros. apply (anti_symm _);
+        [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
+    Qed.
+
+    Lemma view_both_validI_1 (relI : uPred M) a b :
+      (∀ n (x : M), rel n a b → relI n x) →
+      ✓ (●V a ⋅ ◯V b : view rel) ⊢ relI.
+    Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
+    Lemma view_both_validI_2 (relI : uPred M) a b :
+      (∀ n (x : M), relI n x → rel n a b) →
+      relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
+    Proof.
+      intros. rewrite -view_both_dfrac_validI_2 //.
+      apply bi.and_intro; [|done]. by apply bi.pure_intro.
+    Qed.
+    Lemma view_both_validI (relI : uPred M) a b :
+      (∀ n (x : M), rel n a b ↔ relI n x) →
+      ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ relI.
+    Proof.
+      intros. apply (anti_symm _);
+        [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
+    Qed.
+
+    Lemma view_auth_dfrac_validI (relI : uPred M) dq a :
+      (∀ n (x : M), relI n x ↔ rel n a ε) →
+      ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+    Proof.
+      intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
+    Qed.
+    Lemma view_auth_validI (relI : uPred M) a :
+      (∀ n (x : M), relI n x ↔ rel n a ε) →
+      ✓ (●V a : view rel) ⊣⊢ relI.
+    Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
+
+    Lemma view_frag_validI (relI : uPred M) b :
+      (∀ n (x : M), relI n x ↔ ∃ a, rel n a b) →
+      ✓ (◯V b : view rel) ⊣⊢ relI.
+    Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
+  End view.
+
+  Section auth.
+    Context {A : ucmra}.
+    Implicit Types a b : A.
+    Implicit Types x y : auth A.
+
+    Lemma auth_auth_dfrac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
+    Proof.
+      apply view_auth_dfrac_validI=> n. uPred.unseal; split; [|by intros [??]].
+      split; [|done]. apply ucmra_unit_leastN.
+    Qed.
+    Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
+    Proof.
+      by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
+    Qed.
+
+    Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
+    Proof.
+      apply view_frag_validI=> n x.
+      rewrite auth_view_rel_exists. by uPred.unseal.
+    Qed.
+
+    Lemma auth_both_dfrac_validI dq a b :
+      ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+    Proof. apply view_both_dfrac_validI=> n. by uPred.unseal. Qed.
+    Lemma auth_both_validI a b :
+      ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+    Proof.
+      by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
+    Qed.
+
+  End auth.
+
+  Section excl_auth.
+    Context {A : ofe}.
+    Implicit Types a b : A.
+
+    Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
+    Proof.
+      rewrite auth_both_validI bi.and_elim_l.
+      apply bi.exist_elim=> -[[c|]|];
+        by rewrite option_equivI /= excl_equivI //= bi.False_elim.
+    Qed.
+  End excl_auth.
+
+  Section dfrac_agree.
+    Context {A : ofe}.
+    Implicit Types a b : A.
+
+    Lemma dfrac_agree_validI dq a : ✓ (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
+    Proof.
+      rewrite prod_validI /= uPred.discrete_valid. apply bi.entails_anti_sym.
+      - by rewrite bi.and_elim_l.
+      - apply bi.and_intro; first done. etrans; last apply to_agree_validI.
+        apply bi.True_intro.
+    Qed.
+
+    Lemma dfrac_agree_validI_2 dq1 dq2 a b :
+      ✓ (to_dfrac_agree dq1 a ⋅ to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 ⋅ dq2)⌝ ∧ (a ≡ b).
+    Proof.
+      rewrite prod_validI /= uPred.discrete_valid to_agree_op_validI //.
+    Qed.
+
+    Lemma frac_agree_validI q a : ✓ (to_frac_agree q a) ⊣⊢ ⌜(q ≤ 1)%Qp⌝.
+    Proof.
+      rewrite dfrac_agree_validI dfrac_valid_own //.
+    Qed.
+
+    Lemma frac_agree_validI_2 q1 q2 a b :
+      ✓ (to_frac_agree q1 a ⋅ to_frac_agree q2 b) ⊣⊢ ⌜(q1 + q2 ≤ 1)%Qp⌝ ∧ (a ≡ b).
+    Proof.
+      rewrite dfrac_agree_validI_2 dfrac_valid_own //.
+    Qed.
+  End dfrac_agree.
+
+  Section gmap_view.
+    Context {K : Type} `{Countable K} {V : ofe}.
+    Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
+
+    Lemma gmap_view_both_validI m k dq v :
+      ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
+      ✓ dq ∧ m !! k ≡ Some v.
+    Proof.
+      rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
+      intros n a. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
+    Qed.
+
+    Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
+      ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
+      ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
+    Proof.
+      rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
+      rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
+      rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
+    Qed.
+
+  End gmap_view.
 End upred.
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index d8574dee5..dbd09ef05 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -184,72 +184,72 @@ Proof. exact: bupd_plainly. Qed.
 Module uPred.
 
 Section restate.
-Context {M : ucmra}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-
-(* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
-Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-
-Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
-Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
-  uPred_primitive.cmra_valid_ne.
-
-(** Re-exporting primitive lemmas that are not in any interface *)
-Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
-Proof. exact: uPred_primitive.ownM_op. Qed.
-Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
-Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
-Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
-Proof. exact: uPred_primitive.ownM_unit. Qed.
-Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
-Proof. exact: uPred_primitive.later_ownM. Qed.
-Lemma bupd_ownM_updateP x (Φ : M → Prop) :
-  x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
-Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
-
-(** This is really just a special case of an entailment
-between two [siProp], but we do not have the infrastructure
-to express the more general case. This temporary proof rule will
-be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-  (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
-Proof. exact: uPred_primitive.internal_eq_entails. Qed.
-
-Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-Proof. exact: uPred_primitive.ownM_valid. Qed.
-Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
-Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
-Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
-Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
-Proof. exact: uPred_primitive.discrete_valid. Qed.
-
-(** This is really just a special case of an entailment
-between two [siProp], but we do not have the infrastructure
-to express the more general case. This temporary proof rule will
-be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmra} (a : A) (b : B) :
-  (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
-Proof. exact: uPred_primitive.valid_entails. Qed.
-
-(** Consistency/soundness statement *)
-Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
-Proof. apply pure_soundness. Qed.
-
-Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
-Proof. apply internal_eq_soundness. Qed.
-
-Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
-Proof. apply later_soundness. Qed.
-(** See [derived.v] for a similar soundness result for basic updates. *)
+  Context {M : ucmra}.
+  Implicit Types φ : Prop.
+  Implicit Types P Q : uPred M.
+  Implicit Types A : Type.
+
+  (* Force implicit argument M *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+  Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
+  Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
+    uPred_primitive.cmra_valid_ne.
+
+  (** Re-exporting primitive lemmas that are not in any interface *)
+  Lemma ownM_op (a1 a2 : M) :
+    uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
+  Proof. exact: uPred_primitive.ownM_op. Qed.
+  Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
+  Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
+  Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
+  Proof. exact: uPred_primitive.ownM_unit. Qed.
+  Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+  Proof. exact: uPred_primitive.later_ownM. Qed.
+  Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+    x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
+  Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
+
+  (** This is really just a special case of an entailment
+  between two [siProp], but we do not have the infrastructure
+  to express the more general case. This temporary proof rule will
+  be replaced by the proper one eventually. *)
+  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+    (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
+  Proof. exact: uPred_primitive.internal_eq_entails. Qed.
+
+  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+  Proof. exact: uPred_primitive.ownM_valid. Qed.
+  Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
+  Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
+  Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+  Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
+  Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
+  Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
+  Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+  Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
+  Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+  Proof. exact: uPred_primitive.discrete_valid. Qed.
+
+  (** This is really just a special case of an entailment
+  between two [siProp], but we do not have the infrastructure
+  to express the more general case. This temporary proof rule will
+  be replaced by the proper one eventually. *)
+  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
+    (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
+  Proof. exact: uPred_primitive.valid_entails. Qed.
+
+  (** Consistency/soundness statement *)
+  Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
+  Proof. apply pure_soundness. Qed.
+
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
+  Proof. apply internal_eq_soundness. Qed.
+
+  Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
+  Proof. apply later_soundness. Qed.
+  (** See [derived.v] for a similar soundness result for basic updates. *)
 End restate.
 
 
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index 8898726df..16e37a82a 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -9,125 +9,123 @@ Import bi.bi base_logic.bi.uPred.
 
 Module uPred.
 Section derived.
-Context {M : ucmra}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-
-(* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
-Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-
-(** Propers *)
-Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-Global Instance cmra_valid_proper {A : cmra} :
-  Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
-
-(** Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
-Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
-Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
-Proof.
-  rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
-    [by rewrite persistently_elim|].
-  by rewrite {1}persistently_ownM_core core_id_core.
-Qed.
-Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
-Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
-Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
-Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
-Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
-Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
-Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof.
-  rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
-    first by rewrite persistently_elim.
-  apply:persistently_cmra_valid_1.
-Qed.
-Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
-Proof.
-  intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
-  by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
-Qed.
-
-(** Timeless instances *)
-Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
-  Timeless (✓ a : uPred M)%I.
-Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
-Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
-Proof.
-  intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
-  rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
-  apply except_0_mono. rewrite internal_eq_sym.
-  apply (internal_eq_rewrite' b a (uPred_ownM) _);
-    auto using and_elim_l, and_elim_r.
-Qed.
-
-(** Plainness *)
-Global Instance cmra_valid_plain {A : cmra} (a : A) :
-  Plain (✓ a : uPred M)%I.
-Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
-
-(** Persistence *)
-Global Instance cmra_valid_persistent {A : cmra} (a : A) :
-  Persistent (✓ a : uPred M)%I.
-Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
-Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
-Proof.
-  intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
-Qed.
-
-(** For big ops *)
-Global Instance uPred_ownM_sep_homomorphism :
-  MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
-Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
-
-(** Soundness statement for our modalities: facts derived under modalities in
-the empty context also without the modalities.
-For basic updates, soundness only holds for plain propositions. *)
-Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
-Proof. rewrite bupd_plain. done. Qed.
-
-Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
-Proof. induction n; eauto using later_soundness. Qed.
-
-(** As pure demonstration, we also show that this holds for an arbitrary nesting
-of modalities. We have to do a bit of work to be able to state this theorem
-though. *)
-Inductive modality := MBUpd | MLater | MPersistently | MPlainly.
-Definition denote_modality (m : modality) : uPred M → uPred M :=
-  match m with
-  | MBUpd => bupd
-  | MLater => bi_later
-  | MPersistently => bi_persistently
-  | MPlainly => plainly
-  end.
-Definition denote_modalities (ms : list modality) : uPred M → uPred M :=
-  λ P, foldr denote_modality P ms.
-
-(** Now we can state and prove 'soundness under arbitrary modalities' for plain
-propositions. This is probably not a lemma you want to actually use. *)
-Corollary modal_soundness P `{!Plain P} (ms : list modality) :
-  (⊢ denote_modalities ms P) → ⊢ P.
-Proof.
-  intros H. apply (laterN_soundness _ (length ms)).
-  move: H. apply bi_emp_valid_mono.
-  induction ms as [|m ms IH]; first done; simpl.
-  destruct m; simpl; rewrite IH.
-  - rewrite -later_intro. apply bupd_plain. apply _.
-  - done.
-  - rewrite -later_intro persistently_elim. done.
-  - rewrite -later_intro plainly_elim. done.
-Qed.
-
-(** Consistency: one cannot deive [False] in the logic, not even under
-modalities. Again this is just for demonstration and probably not practically
-useful. *)
-Corollary consistency : ¬ ⊢@{uPredI M} False.
-Proof. intros H. by eapply pure_soundness. Qed.
-
+  Context {M : ucmra}.
+  Implicit Types φ : Prop.
+  Implicit Types P Q : uPred M.
+  Implicit Types A : Type.
+
+  (* Force implicit argument M *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
+  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+  (** Propers *)
+  Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
+  Global Instance cmra_valid_proper {A : cmra} :
+    Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
+
+  (** Own and valid derived *)
+  Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
+  Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
+  Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+  Proof.
+    rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
+      [by rewrite persistently_elim|].
+    by rewrite {1}persistently_ownM_core core_id_core.
+  Qed.
+  Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
+  Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
+  Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
+  Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
+  Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
+  Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
+  Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+  Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
+  Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+  Proof.
+    rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
+      first by rewrite persistently_elim.
+    apply:persistently_cmra_valid_1.
+  Qed.
+  Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
+  Proof.
+    intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
+    by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
+  Qed.
+
+  (** Timeless instances *)
+  Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
+    Timeless (✓ a : uPred M)%I.
+  Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
+  Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
+  Proof.
+    intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
+    rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
+    apply except_0_mono. rewrite internal_eq_sym.
+    apply (internal_eq_rewrite' b a (uPred_ownM) _);
+      auto using and_elim_l, and_elim_r.
+  Qed.
+
+  (** Plainness *)
+  Global Instance cmra_valid_plain {A : cmra} (a : A) :
+    Plain (✓ a : uPred M)%I.
+  Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
+
+  (** Persistence *)
+  Global Instance cmra_valid_persistent {A : cmra} (a : A) :
+    Persistent (✓ a : uPred M)%I.
+  Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
+  Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
+  Proof.
+    intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
+  Qed.
+
+  (** For big ops *)
+  Global Instance uPred_ownM_sep_homomorphism :
+    MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
+  Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
+
+  (** Soundness statement for our modalities: facts derived under modalities in
+  the empty context also without the modalities.
+  For basic updates, soundness only holds for plain propositions. *)
+  Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
+  Proof. rewrite bupd_plain. done. Qed.
+
+  Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
+  Proof. induction n; eauto using later_soundness. Qed.
+
+  (** As pure demonstration, we also show that this holds for an arbitrary nesting
+  of modalities. We have to do a bit of work to be able to state this theorem
+  though. *)
+  Inductive modality := MBUpd | MLater | MPersistently | MPlainly.
+  Definition denote_modality (m : modality) : uPred M → uPred M :=
+    match m with
+    | MBUpd => bupd
+    | MLater => bi_later
+    | MPersistently => bi_persistently
+    | MPlainly => plainly
+    end.
+  Definition denote_modalities (ms : list modality) : uPred M → uPred M :=
+    λ P, foldr denote_modality P ms.
+
+  (** Now we can state and prove 'soundness under arbitrary modalities' for plain
+  propositions. This is probably not a lemma you want to actually use. *)
+  Corollary modal_soundness P `{!Plain P} (ms : list modality) :
+    (⊢ denote_modalities ms P) → ⊢ P.
+  Proof.
+    intros H. apply (laterN_soundness _ (length ms)).
+    move: H. apply bi_emp_valid_mono.
+    induction ms as [|m ms IH]; first done; simpl.
+    destruct m; simpl; rewrite IH.
+    - rewrite -later_intro. apply bupd_plain. apply _.
+    - done.
+    - rewrite -later_intro persistently_elim. done.
+    - rewrite -later_intro plainly_elim. done.
+  Qed.
+
+  (** Consistency: one cannot deive [False] in the logic, not even under
+  modalities. Again this is just for demonstration and probably not practically
+  useful. *)
+  Corollary consistency : ¬ ⊢@{uPredI M} False.
+  Proof. intros H. by eapply pure_soundness. Qed.
 End derived.
-
 End uPred.
diff --git a/iris/base_logic/proofmode.v b/iris/base_logic/proofmode.v
index 6ababee40..731ec3005 100644
--- a/iris/base_logic/proofmode.v
+++ b/iris/base_logic/proofmode.v
@@ -2,44 +2,43 @@ From iris.algebra Require Import proofmode_classes.
 From iris.proofmode Require Import classes.
 From iris.base_logic Require Export derived.
 From iris.prelude Require Import options.
-
 Import base_logic.bi.uPred.
 
 (* Setup of the proof mode *)
 Section class_instances.
-Context {M : ucmra}.
-Implicit Types P Q R : uPred M.
+  Context {M : ucmra}.
+  Implicit Types P Q R : uPred M.
 
-Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
-  @IntoPure (uPredI M) (✓ a) (✓ a).
-Proof. by rewrite /IntoPure discrete_valid. Qed.
+  Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
+    @IntoPure (uPredI M) (✓ a) (✓ a).
+  Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
-  @FromPure (uPredI M) false (✓ a) (✓ a).
-Proof.
-  rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
-  rewrite -uPred.cmra_valid_intro //.
-Qed.
+  Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
+    @FromPure (uPredI M) false (✓ a) (✓ a).
+  Proof.
+    rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
+    rewrite -uPred.cmra_valid_intro //.
+  Qed.
 
-Global Instance from_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 →
-  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
-Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
-  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
-  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-  destruct H; by rewrite bi.persistent_and_sep.
-Qed.
+  Global Instance from_sep_ownM (a b1 b2 : M) :
+    IsOp a b1 b2 →
+    FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
+  Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
+    IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
+    FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof.
+    intros ? H. rewrite /FromAnd (is_op a) ownM_op.
+    destruct H; by rewrite bi.persistent_and_sep.
+  Qed.
 
-Global Instance into_and_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
-Qed.
+  Global Instance into_and_ownM p (a b1 b2 : M) :
+    IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof.
+    intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
+  Qed.
 
-Global Instance into_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
+  Global Instance into_sep_ownM (a b1 b2 : M) :
+    IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
 End class_instances.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 8fe8c536f..1c274a2a4 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -435,483 +435,483 @@ Ltac unseal :=
   rewrite !uPred_unseal /=.
 
 Section primitive.
-Context {M : ucmra}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-Local Arguments uPred_holds {_} !_ _ _ /.
-Local Hint Immediate uPred_in_entails : core.
-
-(** The notations below are implicitly local due to the section, so we do not
-mind the overlap with the general BI notations. *)
-Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
-Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
-Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
-Notation "(⊣⊢)" := (@uPred_equiv M) (only parsing) : stdpp_scope.
-
-Notation "'True'" := (uPred_pure True) : bi_scope.
-Notation "'False'" := (uPred_pure False) : bi_scope.
-Notation "'⌜' φ '⌝'" := (uPred_pure φ%type%stdpp) : bi_scope.
-Infix "∧" := uPred_and : bi_scope.
-Infix "∨" := uPred_or : bi_scope.
-Infix "→" := uPred_impl : bi_scope.
-Notation "∀ x .. y , P" :=
-  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope.
-Notation "∃ x .. y , P" :=
-  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope.
-Infix "∗" := uPred_sep : bi_scope.
-Infix "-∗" := uPred_wand : bi_scope.
-Notation "â–¡ P" := (uPred_persistently P) : bi_scope.
-Notation "â–  P" := (uPred_plainly P) : bi_scope.
-Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope.
-Notation "â–· P" := (uPred_later P) : bi_scope.
-Notation "|==> P" := (uPred_bupd P) : bi_scope.
-
-(** Entailment *)
-Lemma entails_po : PreOrder (⊢).
-Proof.
-  split.
-  - by intros P; split=> x i.
-  - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
-Qed.
-Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢).
-Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_entails P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
-Proof.
-  split.
-  - intros HPQ; split; split=> x i; apply HPQ.
-  - intros [??]. exact: entails_anti_sym.
-Qed.
-Lemma entails_lim (cP cQ : chain (uPredO M)) :
-  (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
-Proof.
-  intros Hlim; split=> n m ? HP.
-  eapply uPred_holds_ne, Hlim, HP; rewrite ?conv_compl; eauto.
-Qed.
+  Context {M : ucmra}.
+  Implicit Types φ : Prop.
+  Implicit Types P Q : uPred M.
+  Implicit Types A : Type.
+  Local Arguments uPred_holds {_} !_ _ _ /.
+  Local Hint Immediate uPred_in_entails : core.
+
+  (** The notations below are implicitly local due to the section, so we do not
+  mind the overlap with the general BI notations. *)
+  Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
+  Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
+  Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
+  Notation "(⊣⊢)" := (@uPred_equiv M) (only parsing) : stdpp_scope.
+
+  Notation "'True'" := (uPred_pure True) : bi_scope.
+  Notation "'False'" := (uPred_pure False) : bi_scope.
+  Notation "'⌜' φ '⌝'" := (uPred_pure φ%type%stdpp) : bi_scope.
+  Infix "∧" := uPred_and : bi_scope.
+  Infix "∨" := uPred_or : bi_scope.
+  Infix "→" := uPred_impl : bi_scope.
+  Notation "∀ x .. y , P" :=
+    (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope.
+  Notation "∃ x .. y , P" :=
+    (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope.
+  Infix "∗" := uPred_sep : bi_scope.
+  Infix "-∗" := uPred_wand : bi_scope.
+  Notation "â–¡ P" := (uPred_persistently P) : bi_scope.
+  Notation "â–  P" := (uPred_plainly P) : bi_scope.
+  Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope.
+  Notation "â–· P" := (uPred_later P) : bi_scope.
+  Notation "|==> P" := (uPred_bupd P) : bi_scope.
+
+  (** Entailment *)
+  Lemma entails_po : PreOrder (⊢).
+  Proof.
+    split.
+    - by intros P; split=> x i.
+    - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
+  Qed.
+  Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢).
+  Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
+  Lemma equiv_entails P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+  Proof.
+    split.
+    - intros HPQ; split; split=> x i; apply HPQ.
+    - intros [??]. exact: entails_anti_sym.
+  Qed.
+  Lemma entails_lim (cP cQ : chain (uPredO M)) :
+    (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
+  Proof.
+    intros Hlim; split=> n m ? HP.
+    eapply uPred_holds_ne, Hlim, HP; rewrite ?conv_compl; eauto.
+  Qed.
 
-(** Non-expansiveness and setoid morphisms *)
-Lemma pure_ne n : Proper (iff ==> dist n) (@uPred_pure M).
-Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|m] ?; try apply Hφ. Qed.
+  (** Non-expansiveness and setoid morphisms *)
+  Lemma pure_ne n : Proper (iff ==> dist n) (@uPred_pure M).
+  Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|m] ?; try apply Hφ. Qed.
 
-Lemma and_ne : NonExpansive2 (@uPred_and M).
-Proof.
-  intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
-  split; (intros [??]; split; [by apply HP|by apply HQ]).
-Qed.
+  Lemma and_ne : NonExpansive2 (@uPred_and M).
+  Proof.
+    intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
+    split; (intros [??]; split; [by apply HP|by apply HQ]).
+  Qed.
 
-Lemma or_ne : NonExpansive2 (@uPred_or M).
-Proof.
-  intros n P P' HP Q Q' HQ; split=> x n' ??.
-  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
-Qed.
+  Lemma or_ne : NonExpansive2 (@uPred_or M).
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> x n' ??.
+    unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
+  Qed.
 
-Lemma impl_ne :
-  NonExpansive2 (@uPred_impl M).
-Proof.
-  intros n P P' HP Q Q' HQ; split=> x n' ??.
-  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
-Qed.
+  Lemma impl_ne :
+    NonExpansive2 (@uPred_impl M).
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> x n' ??.
+    unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
+  Qed.
 
-Lemma sep_ne : NonExpansive2 (@uPred_sep M).
-Proof.
-  intros n P P' HP Q Q' HQ; split=> n' x ??.
-  unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
-    exists x1, x2; split_and!; try (apply HP || apply HQ);
-    eauto using cmra_validN_op_l, cmra_validN_op_r.
-Qed.
+  Lemma sep_ne : NonExpansive2 (@uPred_sep M).
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> n' x ??.
+    unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
+      exists x1, x2; split_and!; try (apply HP || apply HQ);
+      eauto using cmra_validN_op_l, cmra_validN_op_r.
+  Qed.
 
-Lemma wand_ne :
-  NonExpansive2 (@uPred_wand M).
-Proof.
-  intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
-    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
-Qed.
+  Lemma wand_ne :
+    NonExpansive2 (@uPred_wand M).
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
+      apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
+  Qed.
 
-Lemma internal_eq_ne (A : ofe) :
-  NonExpansive2 (@uPred_internal_eq M A).
-Proof.
-  intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
-  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
-  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
-Qed.
+  Lemma internal_eq_ne (A : ofe) :
+    NonExpansive2 (@uPred_internal_eq M A).
+  Proof.
+    intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
+    - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
+    - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
+  Qed.
 
-Lemma forall_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
-Proof.
-  by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
-Qed.
+  Lemma forall_ne A n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
+  Proof.
+    by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
+  Qed.
 
-Lemma exist_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
-Proof.
-  intros Ψ1 Ψ2 HΨ.
-  unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
-Qed.
+  Lemma exist_ne A n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
+  Proof.
+    intros Ψ1 Ψ2 HΨ.
+    unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
+  Qed.
 
-Lemma later_contractive : Contractive (@uPred_later M).
-Proof.
-  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia.
-  apply HPQ; eauto using cmra_validN_S.
-Qed.
+  Lemma later_contractive : Contractive (@uPred_later M).
+  Proof.
+    unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia.
+    apply HPQ; eauto using cmra_validN_S.
+  Qed.
 
-Lemma plainly_ne : NonExpansive (@uPred_plainly M).
-Proof.
-  intros n P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using ucmra_unit_validN.
-Qed.
+  Lemma plainly_ne : NonExpansive (@uPred_plainly M).
+  Proof.
+    intros n P1 P2 HP.
+    unseal; split=> n' x; split; apply HP; eauto using ucmra_unit_validN.
+  Qed.
 
-Lemma persistently_ne : NonExpansive (@uPred_persistently M).
-Proof.
-  intros n P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
-Qed.
+  Lemma persistently_ne : NonExpansive (@uPred_persistently M).
+  Proof.
+    intros n P1 P2 HP.
+    unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
+  Qed.
 
-Lemma ownM_ne : NonExpansive (@uPred_ownM M).
-Proof.
-  intros n a b Ha.
-  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
-Qed.
+  Lemma ownM_ne : NonExpansive (@uPred_ownM M).
+  Proof.
+    intros n a b Ha.
+    unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
+  Qed.
 
-Lemma cmra_valid_ne {A : cmra} :
-  NonExpansive (@uPred_cmra_valid M A).
-Proof.
-  intros n a b Ha; unseal; split=> n' x ? /=.
-  by rewrite (dist_le _ _ _ _ Ha); last lia.
-Qed.
+  Lemma cmra_valid_ne {A : cmra} :
+    NonExpansive (@uPred_cmra_valid M A).
+  Proof.
+    intros n a b Ha; unseal; split=> n' x ? /=.
+    by rewrite (dist_le _ _ _ _ Ha); last lia.
+  Qed.
 
-Lemma bupd_ne : NonExpansive (@uPred_bupd M).
-Proof.
-  intros n P Q HPQ.
-  unseal; split=> n' x; split; intros HP k yf ??;
-    destruct (HP k yf) as (x'&?&?); auto;
-    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
-Qed.
+  Lemma bupd_ne : NonExpansive (@uPred_bupd M).
+  Proof.
+    intros n P Q HPQ.
+    unseal; split=> n' x; split; intros HP k yf ??;
+      destruct (HP k yf) as (x'&?&?); auto;
+      exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
+  Qed.
 
-(** Introduction and elimination rules *)
-Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.
-Proof. by intros ?; unseal; split. Qed.
-Lemma pure_elim' φ P : (φ → True ⊢ P) → ⌜φ⌝ ⊢ P.
-Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed.
-Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ x : A, ⌜φ x⌝) ⊢ ⌜∀ x : A, φ x⌝.
-Proof. by unseal. Qed.
-
-Lemma and_elim_l P Q : P ∧ Q ⊢ P.
-Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
-Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
-Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
-
-Lemma or_intro_l P Q : P ⊢ P ∨ Q.
-Proof. unseal; split=> n x ??; left; auto. Qed.
-Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
-Proof. unseal; split=> n x ??; right; auto. Qed.
-Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
-Proof.
-  intros HP HQ; unseal; split=> n x ? [?|?].
-  - by apply HP.
-  - by apply HQ.
-Qed.
+  (** Introduction and elimination rules *)
+  Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.
+  Proof. by intros ?; unseal; split. Qed.
+  Lemma pure_elim' φ P : (φ → True ⊢ P) → ⌜φ⌝ ⊢ P.
+  Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed.
+  Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ x : A, ⌜φ x⌝) ⊢ ⌜∀ x : A, φ x⌝.
+  Proof. by unseal. Qed.
+
+  Lemma and_elim_l P Q : P ∧ Q ⊢ P.
+  Proof. by unseal; split=> n x ? [??]. Qed.
+  Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
+  Proof. by unseal; split=> n x ? [??]. Qed.
+  Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
+  Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
+
+  Lemma or_intro_l P Q : P ⊢ P ∨ Q.
+  Proof. unseal; split=> n x ??; left; auto. Qed.
+  Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
+  Proof. unseal; split=> n x ??; right; auto. Qed.
+  Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
+  Proof.
+    intros HP HQ; unseal; split=> n x ? [?|?].
+    - by apply HP.
+    - by apply HQ.
+  Qed.
 
-Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
-Proof.
-  unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
-    naive_solver eauto using uPred_mono, cmra_included_includedN.
-Qed.
-Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
-Proof. unseal; intros HP ; split=> n x ? [??]; apply HP with n x; auto. Qed.
+  Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
+  Proof.
+    unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
+      naive_solver eauto using uPred_mono, cmra_included_includedN.
+  Qed.
+  Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
+  Proof. unseal; intros HP ; split=> n x ? [??]; apply HP with n x; auto. Qed.
 
-Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
-Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
-Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. unseal; split=> n x ? HP; apply HP. Qed.
+  Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
+  Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
+  Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
+  Proof. unseal; split=> n x ? HP; apply HP. Qed.
 
-Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
-Proof. unseal; split=> n x ??; by exists a. Qed.
-Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
-Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
+  Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
+  Proof. unseal; split=> n x ??; by exists a. Qed.
+  Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
+  Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
 
-(** BI connectives *)
-Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
-Proof.
-  intros HQ HQ'; unseal.
-  split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
-    eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
-Qed.
-Lemma True_sep_1 P : P ⊢ True ∗ P.
-Proof.
-  unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
-Qed.
-Lemma True_sep_2 P : True ∗ P ⊢ P.
-Proof.
-  unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
-    eauto using uPred_mono, cmra_includedN_r.
-Qed.
-Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P.
-Proof.
-  unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op).
-Qed.
-Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R).
-Proof.
-  unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
-  exists y1, (y2 â‹… x2); split_and?; auto.
-  + by rewrite (assoc op) -Hy -Hx.
-  + by exists y2, x2.
-Qed.
-Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
-Proof.
-  unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
-  exists x, x'; split_and?; auto.
-  eapply uPred_mono with n x; eauto using cmra_validN_op_l.
-Qed.
-Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
-Proof.
-  unseal =>HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
-  eapply HPQR; eauto using cmra_validN_op_l.
-Qed.
+  (** BI connectives *)
+  Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
+  Proof.
+    intros HQ HQ'; unseal.
+    split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
+      eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
+  Qed.
+  Lemma True_sep_1 P : P ⊢ True ∗ P.
+  Proof.
+    unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
+  Qed.
+  Lemma True_sep_2 P : True ∗ P ⊢ P.
+  Proof.
+    unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
+      eauto using uPred_mono, cmra_includedN_r.
+  Qed.
+  Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P.
+  Proof.
+    unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op).
+  Qed.
+  Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R).
+  Proof.
+    unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
+    exists y1, (y2 â‹… x2); split_and?; auto.
+    + by rewrite (assoc op) -Hy -Hx.
+    + by exists y2, x2.
+  Qed.
+  Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
+  Proof.
+    unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
+    exists x, x'; split_and?; auto.
+    eapply uPred_mono with n x; eauto using cmra_validN_op_l.
+  Qed.
+  Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
+  Proof.
+    unseal =>HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
+    eapply HPQR; eauto using cmra_validN_op_l.
+  Qed.
 
-(** Persistently *)
-Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
-Lemma persistently_elim P : □ P ⊢ P.
-Proof.
-  unseal; split=> n x ? /=.
-  eauto using uPred_mono, cmra_included_core, cmra_included_includedN.
-Qed.
-Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
-Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
+  (** Persistently *)
+  Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+  Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
+  Lemma persistently_elim P : □ P ⊢ P.
+  Proof.
+    unseal; split=> n x ? /=.
+    eauto using uPred_mono, cmra_included_core, cmra_included_includedN.
+  Qed.
+  Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
+  Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
-Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
-Proof. by unseal. Qed.
-Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
-Proof. by unseal. Qed.
+  Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+  Proof. by unseal. Qed.
+  Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
+  Proof. by unseal. Qed.
 
-Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ P ∗ Q.
-Proof.
-  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
-  by rewrite cmra_core_l.
-Qed.
+  Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ P ∗ Q.
+  Proof.
+    unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
+    by rewrite cmra_core_l.
+  Qed.
 
-(** Plainly *)
-Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
-Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
-Lemma plainly_elim_persistently P : ■ P ⊢ □ P.
-Proof. unseal; split; simpl; eauto using uPred_mono, ucmra_unit_leastN. Qed.
-Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
-Proof. unseal; split=> n x ?? //. Qed.
+  (** Plainly *)
+  Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
+  Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
+  Lemma plainly_elim_persistently P : ■ P ⊢ □ P.
+  Proof. unseal; split; simpl; eauto using uPred_mono, ucmra_unit_leastN. Qed.
+  Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
+  Proof. unseal; split=> n x ?? //. Qed.
 
-Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ■ Ψ a) ⊢ (■ ∀ a, Ψ a).
-Proof. by unseal. Qed.
-Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a).
-Proof. by unseal. Qed.
+  Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ■ Ψ a) ⊢ (■ ∀ a, Ψ a).
+  Proof. by unseal. Qed.
+  Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a).
+  Proof. by unseal. Qed.
 
-Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
-Proof.
-  unseal; split=> n x ? /=. setoid_rewrite (left_id ε op). split; naive_solver.
-Qed.
+  Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+  Proof.
+    unseal; split=> n x ? /=. setoid_rewrite (left_id ε op). split; naive_solver.
+  Qed.
 
-(* The following two laws are very similar, and indeed they hold not just for â–¡
-   and ■, but for any modality defined as `M P n x := ∀ y, R x y → P n y`. *)
-Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q).
-Proof.
-  unseal; split=> /= n x ? HPQ n' x' ????.
-  eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
-  apply (HPQ n' x); eauto using cmra_validN_le.
-Qed.
+  (* The following two laws are very similar, and indeed they hold not just for â–¡
+     and ■, but for any modality defined as `M P n x := ∀ y, R x y → P n y`. *)
+  Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q).
+  Proof.
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  Qed.
 
-Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
-Proof.
-  unseal; split=> /= n x ? HPQ n' x' ????.
-  eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
-  apply (HPQ n' x); eauto using cmra_validN_le.
-Qed.
+  Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
+  Proof.
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  Qed.
 
-(** Later *)
-Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
-Proof.
-  unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
-Qed.
-Lemma later_intro P : P ⊢ ▷ P.
-Proof.
-  unseal; split=> -[|n] /= x ? HP; first done.
-  apply uPred_mono with (S n) x; eauto using cmra_validN_S.
-Qed.
-Lemma later_forall_2 {A} (Φ : A → uPred M) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
-Proof. unseal; by split=> -[|n] x. Qed.
-Lemma later_exist_false {A} (Φ : A → uPred M) :
-  (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
-Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed.
-Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
-Proof.
-  unseal; split=> n x ?.
-  destruct n as [|n]; simpl.
-  { by exists x, (core x); rewrite cmra_core_r. }
-  intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
-    as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
-  exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
-Qed.
-Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
-Proof.
-  unseal; split=> n x ?.
-  destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
-  exists x1, x2; eauto using dist_S.
-Qed.
+  (** Later *)
+  Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
+  Proof.
+    unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
+  Qed.
+  Lemma later_intro P : P ⊢ ▷ P.
+  Proof.
+    unseal; split=> -[|n] /= x ? HP; first done.
+    apply uPred_mono with (S n) x; eauto using cmra_validN_S.
+  Qed.
+  Lemma later_forall_2 {A} (Φ : A → uPred M) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
+  Proof. unseal; by split=> -[|n] x. Qed.
+  Lemma later_exist_false {A} (Φ : A → uPred M) :
+    (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
+  Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed.
+  Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
+  Proof.
+    unseal; split=> n x ?.
+    destruct n as [|n]; simpl.
+    { by exists x, (core x); rewrite cmra_core_r. }
+    intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
+      as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
+    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
+  Qed.
+  Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
+  Proof.
+    unseal; split=> n x ?.
+    destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
+    exists x1, x2; eauto using dist_S.
+  Qed.
 
-Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
-Proof.
-  unseal; split=> -[|n] x ? /= HP; [by left|right].
-  intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
-Qed.
+  Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
+  Proof.
+    unseal; split=> -[|n] x ? /= HP; [by left|right].
+    intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
+  Qed.
 
-Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
-Proof. by unseal. Qed.
-Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
-Proof. by unseal. Qed.
-Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ ▷ P.
-Proof. by unseal. Qed.
-Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
-Proof. by unseal. Qed.
-
-(** Internal equality *)
-Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
-Proof. unseal; by split=> n x ??; simpl. Qed.
-Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → uPred M) :
-  NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
-
-Lemma fun_ext {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
-  (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
-Proof. by unseal. Qed.
-Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
-  proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
-Proof. by unseal. Qed.
-
-Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-Proof. by unseal. Qed.
-Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-Proof. by unseal. Qed.
-
-Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
-Proof.
-  unseal=> ?. split=> n x ?. by apply (discrete_iff n).
-Qed.
+  Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
+  Proof. by unseal. Qed.
+  Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
+  Proof. by unseal. Qed.
+  Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ ▷ P.
+  Proof. by unseal. Qed.
+  Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
+  Proof. by unseal. Qed.
+
+  (** Internal equality *)
+  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
+  Proof. unseal; by split=> n x ??; simpl. Qed.
+  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → uPred M) :
+    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+  Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
+
+  Lemma fun_ext {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
+    (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
+  Proof. by unseal. Qed.
+  Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
+    proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
+  Proof. by unseal. Qed.
+
+  Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+  Proof. by unseal. Qed.
+  Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+  Proof. by unseal. Qed.
+
+  Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
+  Proof.
+    unseal=> ?. split=> n x ?. by apply (discrete_iff n).
+  Qed.
 
-(** This is really just a special case of an entailment
-between two [siProp], but we do not have the infrastructure
-to express the more general case. This temporary proof rule will
-be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-  (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
-Proof. unseal=>Hsi. split=>n x ?. apply Hsi. Qed.
+  (** This is really just a special case of an entailment
+  between two [siProp], but we do not have the infrastructure
+  to express the more general case. This temporary proof rule will
+  be replaced by the proper one eventually. *)
+  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+    (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
+  Proof. unseal=>Hsi. split=>n x ?. apply Hsi. Qed.
 
-(** Basic update modality *)
-Lemma bupd_intro P : P ⊢ |==> P.
-Proof.
-  unseal. split=> n x ? HP k yf ?; exists x; split; first done.
-  apply uPred_mono with n x; eauto using cmra_validN_op_l.
-Qed.
-Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ⊢ |==> Q.
-Proof.
-  unseal. intros HPQ; split=> n x ? HP k yf ??.
-  destruct (HP k yf) as (x'&?&?); eauto.
-  exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
-Qed.
-Lemma bupd_trans P : (|==> |==> P) ⊢ |==> P.
-Proof. unseal; split; naive_solver. Qed.
-Lemma bupd_frame_r P R : (|==> P) ∗ R ⊢ |==> P ∗ R.
-Proof.
-  unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
-  destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
-  { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
-  exists (x' â‹… x2); split; first by rewrite -assoc.
-  exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Lemma bupd_plainly P : (|==> ■ P) ⊢ P.
-Proof.
-  unseal; split => n x Hnx /= Hng.
-  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
-  eapply uPred_mono; eauto using ucmra_unit_leastN.
-Qed.
+  (** Basic update modality *)
+  Lemma bupd_intro P : P ⊢ |==> P.
+  Proof.
+    unseal. split=> n x ? HP k yf ?; exists x; split; first done.
+    apply uPred_mono with n x; eauto using cmra_validN_op_l.
+  Qed.
+  Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ⊢ |==> Q.
+  Proof.
+    unseal. intros HPQ; split=> n x ? HP k yf ??.
+    destruct (HP k yf) as (x'&?&?); eauto.
+    exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
+  Qed.
+  Lemma bupd_trans P : (|==> |==> P) ⊢ |==> P.
+  Proof. unseal; split; naive_solver. Qed.
+  Lemma bupd_frame_r P R : (|==> P) ∗ R ⊢ |==> P ∗ R.
+  Proof.
+    unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
+    destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
+    { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
+    exists (x' â‹… x2); split; first by rewrite -assoc.
+    exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
+  Qed.
+  Lemma bupd_plainly P : (|==> ■ P) ⊢ P.
+  Proof.
+    unseal; split => n x Hnx /= Hng.
+    destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
+    eapply uPred_mono; eauto using ucmra_unit_leastN.
+  Qed.
 
-(** Own *)
-Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
-Proof.
-  unseal; split=> n x ?; split.
-  - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
-    split.
-    + by exists (core a1); rewrite cmra_core_r.
-    + by exists z.
-  - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
-    by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-      -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
-Qed.
-Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
-Proof.
-  split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
-Qed.
-Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
-Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
-Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
-Proof.
-  unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
-  destruct Hax as [y ?].
-  destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
-  exists a'. rewrite Hx. eauto using cmra_includedN_l.
-Qed.
+  (** Own *)
+  Lemma ownM_op (a1 a2 : M) :
+    uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
+  Proof.
+    unseal; split=> n x ?; split.
+    - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
+      split.
+      + by exists (core a1); rewrite cmra_core_r.
+      + by exists z.
+    - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
+      by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
+        -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
+  Qed.
+  Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
+  Proof.
+    split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
+  Qed.
+  Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
+  Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
+  Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+  Proof.
+    unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
+    destruct Hax as [y ?].
+    destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
+    exists a'. rewrite Hx. eauto using cmra_includedN_l.
+  Qed.
 
-Lemma bupd_ownM_updateP x (Φ : M → Prop) :
-  x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
-Proof.
-  unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
-  destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
-  { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
-  exists (y â‹… x3); split; first by rewrite -assoc.
-  exists y; eauto using cmra_includedN_l.
-Qed.
+  Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+    x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
+  Proof.
+    unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
+    destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
+    { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
+    exists (y â‹… x3); split; first by rewrite -assoc.
+    exists y; eauto using cmra_includedN_l.
+  Qed.
 
-(** Valid *)
-Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-Proof.
-  unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
-Qed.
-Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
-Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
-Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
-Proof. by unseal. Qed.
-Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
-
-Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
-Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-
-(** This is really just a special case of an entailment
-between two [siProp], but we do not have the infrastructure
-to express the more general case. This temporary proof rule will
-be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmra} (a : A) (b : B) :
-  (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
-Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
-
-(** Consistency/soundness statement *)
-(** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
-instance of [siProp] soundness in the future. *)
-Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
-Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
-
-Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
-Proof.
-  unseal=> -[H]. apply equiv_dist=> n.
-  by apply (H n ε); eauto using ucmra_unit_validN.
-Qed.
+  (** Valid *)
+  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+  Proof.
+    unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
+  Qed.
+  Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
+  Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
+  Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+  Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
+  Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
+  Proof. by unseal. Qed.
+  Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+  Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
+
+  Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+  Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
+
+  (** This is really just a special case of an entailment
+  between two [siProp], but we do not have the infrastructure
+  to express the more general case. This temporary proof rule will
+  be replaced by the proper one eventually. *)
+  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
+    (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
+  Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
+
+  (** Consistency/soundness statement *)
+  (** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
+  instance of [siProp] soundness in the future. *)
+  Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
+  Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
+
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+  Proof.
+    unseal=> -[H]. apply equiv_dist=> n.
+    by apply (H n ε); eauto using ucmra_unit_validN.
+  Qed.
 
-Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
-Proof.
-  unseal=> -[HP]; split=> n x Hx _.
-  apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
-  by apply (HP (S n)); eauto using ucmra_unit_validN.
-Qed.
+  Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
+  Proof.
+    unseal=> -[HP]; split=> n x Hx _.
+    apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
+    by apply (HP (S n)); eauto using ucmra_unit_validN.
+  Qed.
 End primitive.
 End uPred_primitive.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 8a6b499b0..16a80ebe1 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -130,188 +130,188 @@ Local Definition siProp_unseal :=
 Ltac unseal := rewrite !siProp_unseal /=.
 
 Section primitive.
-Local Arguments siProp_holds !_ _ /.
-
-(** The notations below are implicitly local due to the section, so we do not
-mind the overlap with the general BI notations. *)
-Notation "P ⊢ Q" := (siProp_entails P Q).
-Notation "'True'" := (siProp_pure True) : bi_scope.
-Notation "'False'" := (siProp_pure False) : bi_scope.
-Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : bi_scope.
-Infix "∧" := siProp_and : bi_scope.
-Infix "∨" := siProp_or : bi_scope.
-Infix "→" := siProp_impl : bi_scope.
-Notation "∀ x .. y , P" :=
-  (siProp_forall (λ x, .. (siProp_forall (λ y, P%I)) ..)) : bi_scope.
-Notation "∃ x .. y , P" :=
-  (siProp_exist (λ x, .. (siProp_exist (λ y, P%I)) ..)) : bi_scope.
-Notation "x ≡ y" := (siProp_internal_eq x y) : bi_scope.
-Notation "â–· P" := (siProp_later P) : bi_scope.
-
-(** Below there follow the primitive laws for [siProp]. There are no derived laws
-in this file. *)
-
-(** Entailment *)
-Lemma entails_po : PreOrder siProp_entails.
-Proof.
-  split.
-  - intros P; by split=> i.
-  - intros P Q Q' HP HQ; split=> i ?; by apply HQ, HP.
-Qed.
-Lemma entails_anti_symm : AntiSymm (≡) siProp_entails.
-Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
-Proof.
-  split.
-  - intros HPQ; split; split=> i; apply HPQ.
-  - intros [??]. by apply entails_anti_symm.
-Qed.
-
-(** Non-expansiveness and setoid morphisms *)
-Lemma pure_ne n : Proper (iff ==> dist n) siProp_pure.
-Proof. intros φ1 φ2 Hφ. by unseal. Qed.
-Lemma and_ne : NonExpansive2 siProp_and.
-Proof.
-  intros n P P' HP Q Q' HQ; unseal; split=> n' ?.
-  split; (intros [??]; split; [by apply HP|by apply HQ]).
-Qed.
-Lemma or_ne : NonExpansive2 siProp_or.
-Proof.
-  intros n P P' HP Q Q' HQ; split=> n' ?.
-  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
-Qed.
-Lemma impl_ne : NonExpansive2 siProp_impl.
-Proof.
-  intros n P P' HP Q Q' HQ; split=> n' ?.
-  unseal; split; intros HPQ n'' ??; apply HQ, HPQ, HP; auto with lia.
-Qed.
-Lemma forall_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_forall A).
-Proof.
-   by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
-Qed.
-Lemma exist_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_exist A).
-Proof.
-  intros Ψ1 Ψ2 HΨ.
-  unseal; split=> n' ?; split; intros [a ?]; exists a; by apply HΨ.
-Qed.
-Lemma later_contractive : Contractive siProp_later.
-Proof.
-  unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
-  apply HPQ; lia.
-Qed.
-Lemma internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
-Proof.
-  intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
-  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
-  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
-Qed.
-
-(** Introduction and elimination rules *)
-Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
-Proof. intros ?. unseal; by split. Qed.
-Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
-Proof. unseal=> HP; split=> n ?. by apply HP. Qed.
-Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝.
-Proof. by unseal. Qed.
-
-Lemma and_elim_l P Q : P ∧ Q ⊢ P.
-Proof. unseal; by split=> n [??]. Qed.
-Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
-Proof. unseal; by split=> n [??]. Qed.
-Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
-Proof.
-  intros HQ HR; unseal; split=> n ?.
-  split.
-  - by apply HQ.
-  - by apply HR.
-Qed.
-
-Lemma or_intro_l P Q : P ⊢ P ∨ Q.
-Proof. unseal; split=> n ?; left; auto. Qed.
-Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
-Proof. unseal; split=> n ?; right; auto. Qed.
-Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
-Proof.
-  intros HP HQ. unseal; split=> n [?|?].
-  - by apply HP.
-  - by apply HQ.
-Qed.
-
-Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
-Proof.
-  unseal=> HQ; split=> n ? n' ??.
-  apply HQ; naive_solver eauto using siProp_closed.
-Qed.
-Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
-Proof. unseal=> HP; split=> n [??]. apply HP with n; auto. Qed.
-
-Lemma forall_intro {A} P (Ψ : A → siProp) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
-Proof. unseal; intros HPΨ; split=> n ? a; by apply HPΨ. Qed.
-Lemma forall_elim {A} {Ψ : A → siProp} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. unseal; split=> n HP; apply HP. Qed.
-
-Lemma exist_intro {A} {Ψ : A → siProp} a : Ψ a ⊢ ∃ a, Ψ a.
-Proof. unseal; split=> n ?; by exists a. Qed.
-Lemma exist_elim {A} (Φ : A → siProp) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
-Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.
-
-(** Equality *)
-Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
-Proof. unseal; by split=> n ? /=. Qed.
-Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → siProp) :
-  NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-Proof.
-  intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
-Qed.
-
-Lemma fun_ext {A} {B : A → ofe} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
-Proof. by unseal. Qed.
-Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
-Proof. by unseal. Qed.
-Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
-Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
-
-Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
-Proof.
-  unseal; split=> n /= HPQ. split=> n' ?.
-  move: HPQ=> [] /(_ n') ? /(_ n'). naive_solver.
-Qed.
-
-(** Later *)
-Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-Proof. by unseal. Qed.
-Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-Proof. by unseal. Qed.
-
-Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
-Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
-Lemma later_intro P : P ⊢ ▷ P.
-Proof. unseal; split=> -[|n] /= HP; eauto using siProp_closed. Qed.
-
-Lemma later_forall_2 {A} (Φ : A → siProp) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
-Proof. unseal; by split=> -[|n]. Qed.
-Lemma later_exist_false {A} (Φ : A → siProp) :
-  (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
-Proof. unseal; split=> -[|[|n]] /=; eauto. Qed.
-Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
-Proof.
-  unseal; split=> -[|n] /= HP; [by left|right].
-  intros [|n'] ?; eauto using siProp_closed with lia.
-Qed.
-
-(** Consistency/soundness statement *)
-Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
-Proof. unseal=> -[H]. by apply (H 0). Qed.
-
-Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
-Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.
-
-Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
-Proof.
-  unseal=> -[HP]; split=> n _. apply siProp_closed with n; last done.
-  by apply (HP (S n)).
-Qed.
+  Local Arguments siProp_holds !_ _ /.
+
+  (** The notations below are implicitly local due to the section, so we do not
+  mind the overlap with the general BI notations. *)
+  Notation "P ⊢ Q" := (siProp_entails P Q).
+  Notation "'True'" := (siProp_pure True) : bi_scope.
+  Notation "'False'" := (siProp_pure False) : bi_scope.
+  Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : bi_scope.
+  Infix "∧" := siProp_and : bi_scope.
+  Infix "∨" := siProp_or : bi_scope.
+  Infix "→" := siProp_impl : bi_scope.
+  Notation "∀ x .. y , P" :=
+    (siProp_forall (λ x, .. (siProp_forall (λ y, P%I)) ..)) : bi_scope.
+  Notation "∃ x .. y , P" :=
+    (siProp_exist (λ x, .. (siProp_exist (λ y, P%I)) ..)) : bi_scope.
+  Notation "x ≡ y" := (siProp_internal_eq x y) : bi_scope.
+  Notation "â–· P" := (siProp_later P) : bi_scope.
+
+  (** Below there follow the primitive laws for [siProp]. There are no derived laws
+  in this file. *)
+
+  (** Entailment *)
+  Lemma entails_po : PreOrder siProp_entails.
+  Proof.
+    split.
+    - intros P; by split=> i.
+    - intros P Q Q' HP HQ; split=> i ?; by apply HQ, HP.
+  Qed.
+  Lemma entails_anti_symm : AntiSymm (≡) siProp_entails.
+  Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
+  Lemma equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+  Proof.
+    split.
+    - intros HPQ; split; split=> i; apply HPQ.
+    - intros [??]. by apply entails_anti_symm.
+  Qed.
+
+  (** Non-expansiveness and setoid morphisms *)
+  Lemma pure_ne n : Proper (iff ==> dist n) siProp_pure.
+  Proof. intros φ1 φ2 Hφ. by unseal. Qed.
+  Lemma and_ne : NonExpansive2 siProp_and.
+  Proof.
+    intros n P P' HP Q Q' HQ; unseal; split=> n' ?.
+    split; (intros [??]; split; [by apply HP|by apply HQ]).
+  Qed.
+  Lemma or_ne : NonExpansive2 siProp_or.
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> n' ?.
+    unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
+  Qed.
+  Lemma impl_ne : NonExpansive2 siProp_impl.
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> n' ?.
+    unseal; split; intros HPQ n'' ??; apply HQ, HPQ, HP; auto with lia.
+  Qed.
+  Lemma forall_ne A n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_forall A).
+  Proof.
+     by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
+  Qed.
+  Lemma exist_ne A n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_exist A).
+  Proof.
+    intros Ψ1 Ψ2 HΨ.
+    unseal; split=> n' ?; split; intros [a ?]; exists a; by apply HΨ.
+  Qed.
+  Lemma later_contractive : Contractive siProp_later.
+  Proof.
+    unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
+    apply HPQ; lia.
+  Qed.
+  Lemma internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
+  Proof.
+    intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
+    - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
+    - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
+  Qed.
+
+  (** Introduction and elimination rules *)
+  Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
+  Proof. intros ?. unseal; by split. Qed.
+  Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
+  Proof. unseal=> HP; split=> n ?. by apply HP. Qed.
+  Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝.
+  Proof. by unseal. Qed.
+
+  Lemma and_elim_l P Q : P ∧ Q ⊢ P.
+  Proof. unseal; by split=> n [??]. Qed.
+  Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
+  Proof. unseal; by split=> n [??]. Qed.
+  Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
+  Proof.
+    intros HQ HR; unseal; split=> n ?.
+    split.
+    - by apply HQ.
+    - by apply HR.
+  Qed.
+
+  Lemma or_intro_l P Q : P ⊢ P ∨ Q.
+  Proof. unseal; split=> n ?; left; auto. Qed.
+  Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
+  Proof. unseal; split=> n ?; right; auto. Qed.
+  Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
+  Proof.
+    intros HP HQ. unseal; split=> n [?|?].
+    - by apply HP.
+    - by apply HQ.
+  Qed.
+
+  Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
+  Proof.
+    unseal=> HQ; split=> n ? n' ??.
+    apply HQ; naive_solver eauto using siProp_closed.
+  Qed.
+  Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
+  Proof. unseal=> HP; split=> n [??]. apply HP with n; auto. Qed.
+
+  Lemma forall_intro {A} P (Ψ : A → siProp) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
+  Proof. unseal; intros HPΨ; split=> n ? a; by apply HPΨ. Qed.
+  Lemma forall_elim {A} {Ψ : A → siProp} a : (∀ a, Ψ a) ⊢ Ψ a.
+  Proof. unseal; split=> n HP; apply HP. Qed.
+
+  Lemma exist_intro {A} {Ψ : A → siProp} a : Ψ a ⊢ ∃ a, Ψ a.
+  Proof. unseal; split=> n ?; by exists a. Qed.
+  Lemma exist_elim {A} (Φ : A → siProp) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
+  Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.
+
+  (** Equality *)
+  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
+  Proof. unseal; by split=> n ? /=. Qed.
+  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → siProp) :
+    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+  Proof.
+    intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
+  Qed.
+
+  Lemma fun_ext {A} {B : A → ofe} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
+  Proof. by unseal. Qed.
+  Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
+  Proof. by unseal. Qed.
+  Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
+  Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
+
+  Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+  Proof.
+    unseal; split=> n /= HPQ. split=> n' ?.
+    move: HPQ=> [] /(_ n') ? /(_ n'). naive_solver.
+  Qed.
+
+  (** Later *)
+  Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+  Proof. by unseal. Qed.
+  Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+  Proof. by unseal. Qed.
+
+  Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
+  Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
+  Lemma later_intro P : P ⊢ ▷ P.
+  Proof. unseal; split=> -[|n] /= HP; eauto using siProp_closed. Qed.
+
+  Lemma later_forall_2 {A} (Φ : A → siProp) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
+  Proof. unseal; by split=> -[|n]. Qed.
+  Lemma later_exist_false {A} (Φ : A → siProp) :
+    (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
+  Proof. unseal; split=> -[|[|n]] /=; eauto. Qed.
+  Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
+  Proof.
+    unseal; split=> -[|n] /= HP; [by left|right].
+    intros [|n'] ?; eauto using siProp_closed with lia.
+  Qed.
+
+  (** Consistency/soundness statement *)
+  Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
+  Proof. unseal=> -[H]. by apply (H 0). Qed.
+
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+  Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.
+
+  Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
+  Proof.
+    unseal=> -[HP]; split=> n _. apply siProp_closed with n; last done.
+    by apply (HP (S n)).
+  Qed.
 End primitive.
 End siProp_primitive.
-- 
GitLab