diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 98857b9cb159b0bed8ba9e04a39b19393d3aeea8..34fba7aef020814d4962c814d86c4a8402456d6b 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 d8574dee580d05bd10bb247ccc3641b6e9f70b5d..dbd09ef0551e4825d9ee441420865004d9f90558 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 8898726df74117e98cc7f6e30777aba63b389592..16e37a82a08884d689c6d8f0acdc65f1237d084e 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 6ababee40451a8dfb897129fa155d593a995ca23..731ec300570a2219ab3613718d587d0cf606ff5d 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 8fe8c536f01f18157b74cfdaeb8052261a725ba5..1c274a2a498678b910753c1c539aab3c1da07198 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 8a6b499b0da8d27836225d94d3f4ebee6d21b78b..16a80ebe14815da45480d0fd9492a741ec58f4d1 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.