diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000000000000000000000000000000000000..3853fde1690ea8e268ab7956ecda3c129f0d6197
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,20 @@
+In this changelog, we document "large-ish" changes to Iris that affect even the
+way the logic is used on paper.  We also mention some significant changes in the
+Coq development, but not every API-breaking change is listed.  Changes marked
+[#] still need to be ported to the Iris Documentation LaTeX file.
+
+## Iris 2.0
+
+This version accompanies the final ICFP paper.
+
+* [# algebra] Make the core of an RA or CMRA a partial function.
+* [heap_lang] No longer use dependent types for expressions.  Instead, values
+  carry a proof of closedness.  Substitution, closedness and value-ness proofs
+  are performed by computation after reflecting into a term langauge that knows
+  about values and closed expressions.
+* [program_logic/language] The language does not define its own "atomic"
+  predicate.  Instead, atomicity is defined as reducing in one step to a value.
+
+## Iris 2.0-rc1
+
+This is the Coq development and Iris Documentation as submitted to ICFP.
diff --git a/algebra/auth.v b/algebra/auth.v
index f9cfc7c35542adb66bc5b586e7ed0d4b5253ada6..d9fa09e152742fe889072b811e75fc6ffa7f44da 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -127,7 +127,7 @@ Proof.
   - by split; simpl; rewrite ?cmra_core_l.
   - by split; simpl; rewrite ?cmra_core_idemp.
   - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply cmra_core_preserving.
+    by split; simpl; apply cmra_core_mono.
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
    intros n [[[a1|]|] b1] [[[a2|]|] b2];
@@ -183,8 +183,7 @@ Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
 
 Lemma auth_update a af b :
-  a ~l~> b @ Some af →
-  ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
+  a ~l~> b @ Some af → ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
 Proof.
   intros [Hab Hab']; apply cmra_total_update.
   move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
@@ -192,6 +191,11 @@ Proof.
   exists bf2. rewrite -assoc.
   apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
 Qed.
+Lemma auth_update_no_frame a b : a ~l~> b @ Some ∅ → ● a ⋅ ◯ a ~~> ● b ⋅ ◯ b.
+Proof.
+  intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
+  by apply auth_update.
+Qed.
 End cmra.
 
 Arguments authR : clear implicits.
@@ -222,9 +226,9 @@ Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
 Proof.
   split; try apply _.
   - intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
-      naive_solver eauto using includedN_preserving, validN_preserving.
+      naive_solver eauto using cmra_monotoneN, validN_preserving.
   - by intros [x a] [y b]; rewrite !auth_included /=;
-      intros [??]; split; simpl; apply: included_preserving.
+      intros [??]; split; simpl; apply: cmra_monotone.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
   CofeMor (auth_map f).
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 177c51ec9f91ba22b84a3484fb0f3f00afe5f0ef..a388fc743e13b18b44abb721d60e912c754d373b 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -48,7 +48,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
   mixin_cmra_comm : Comm (≡) (⋅);
   mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
   mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
-  mixin_cmra_pcore_preserving x y cx :
+  mixin_cmra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
   mixin_cmra_extend n x y1 y2 :
@@ -113,9 +113,9 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.
   Lemma cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx.
   Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.
-  Lemma cmra_pcore_preserving x y cx :
+  Lemma cmra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
-  Proof. apply (mixin_cmra_pcore_preserving _ (cmra_mixin A)). Qed.
+  Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
   Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
   Lemma cmra_extend n x y1 y2 :
@@ -217,10 +217,10 @@ Class CMRADiscrete (A : cmraT) := {
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
   validN_preserving n x : ✓{n} x → ✓{n} f x;
-  included_preserving x y : x ≼ y → f x ≼ f y
+  cmra_monotone x y : x ≼ y → f x ≼ f y
 }.
 Arguments validN_preserving {_ _} _ {_} _ _ _.
-Arguments included_preserving {_ _} _ {_} _ _ _.
+Arguments cmra_monotone {_ _} _ {_} _ _ _.
 
 (** * Properties **)
 Section cmra.
@@ -364,18 +364,18 @@ Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
 Lemma cmra_included_r x y : y ≼ x ⋅ y.
 Proof. rewrite (comm op); apply cmra_included_l. Qed.
 
-Lemma cmra_pcore_preserving' x y cx :
+Lemma cmra_pcore_mono' x y cx :
   x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
 Proof.
   intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
-  destruct (cmra_pcore_preserving x y cx') as (cy&->&?); auto.
+  destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
   exists cy; by rewrite Hcx.
 Qed.
-Lemma cmra_pcore_preservingN' n x y cx :
+Lemma cmra_pcore_monoN' n x y cx :
   x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
 Proof.
   intros [z Hy] (cx'&?&Hcx)%dist_Some_inv_r'.
-  destruct (cmra_pcore_preserving x (x â‹… z) cx')
+  destruct (cmra_pcore_mono x (x â‹… z) cx')
     as (cy&Hxy&?); auto using cmra_included_l.
   assert (pcore y ≡{n}≡ Some cy) as (cy'&?&Hcy')%dist_Some_inv_r'.
   { by rewrite Hy Hxy. }
@@ -384,14 +384,14 @@ Proof.
 Qed.
 Lemma cmra_included_pcore x cx : pcore x = Some cx → cx ≼ x.
 Proof. exists x. by rewrite cmra_pcore_l. Qed.
-Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
+Lemma cmra_monoN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
 Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
-Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
+Lemma cmra_mono_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
 Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
-Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
-Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
-Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
-Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
+Lemma cmra_monoN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
+Proof. by intros; rewrite -!(comm _ z); apply cmra_monoN_l. Qed.
+Lemma cmra_mono_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
+Proof. by intros; rewrite -!(comm _ z); apply cmra_mono_l. Qed.
 
 Lemma cmra_included_dist_l n x1 x2 x1' :
   x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2.
@@ -412,10 +412,10 @@ Section total_core.
   Proof.
     destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_idemp.
   Qed.
-  Lemma cmra_core_preserving x y : x ≼ y → core x ≼ core y.
+  Lemma cmra_core_mono x y : x ≼ y → core x ≼ core y.
   Proof.
     intros; destruct (cmra_total x) as [cx Hcx].
-    destruct (cmra_pcore_preserving x y cx) as (cy&Hcy&?); auto.
+    destruct (cmra_pcore_mono x y cx) as (cy&Hcy&?); auto.
     by rewrite /core /= Hcx Hcy.
   Qed.
 
@@ -461,10 +461,10 @@ Section total_core.
   Proof.
     split; [|apply _]. by intros x; exists (core x); rewrite cmra_core_r.
   Qed.
-  Lemma cmra_core_preservingN n x y : x ≼{n} y → core x ≼{n} core y.
+  Lemma cmra_core_monoN n x y : x ≼{n} y → core x ≼{n} core y.
   Proof.
     intros [z ->].
-    apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
+    apply cmra_included_includedN, cmra_core_mono, cmra_included_l.
   Qed.
 End total_core.
 
@@ -519,7 +519,7 @@ Section ucmra.
 
   Global Instance cmra_unit_total : CMRATotal A.
   Proof.
-    intros x. destruct (cmra_pcore_preserving' ∅ x ∅) as (cx&->&?);
+    intros x. destruct (cmra_pcore_mono' ∅ x ∅) as (cx&->&?);
       eauto using ucmra_unit_least, (persistent ∅).
   Qed.
 End ucmra.
@@ -538,7 +538,7 @@ Section cmra_total.
   Context (op_comm : Comm (≡) (@op A _)).
   Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
   Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
-  Context (core_preserving : ∀ x y : A, x ≼ y → core x ≼ core y).
+  Context (core_mono : ∀ x y : A, x ≼ y → core x ≼ core y).
   Context (validN_op_l : ∀ n (x y : A), ✓{n} (x ⋅ y) → ✓{n} x).
   Context (extend : ∀ n (x y1 y2 : A),
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
@@ -551,7 +551,7 @@ Section cmra_total.
     - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
     - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
       case (total cx)=>[ccx ->]; by constructor.
-    - intros x y cx Hxy%core_preserving Hx. move: Hxy.
+    - intros x y cx Hxy%core_mono Hx. move: Hxy.
       rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
   Qed.
 End cmra_total.
@@ -565,16 +565,16 @@ Proof.
   split.
   - apply _. 
   - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
-  - move=> x y Hxy /=. by apply included_preserving, included_preserving.
+  - move=> x y Hxy /=. by apply cmra_monotone, cmra_monotone.
 Qed.
 
 Section cmra_monotone.
   Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}.
   Global Instance cmra_monotone_proper : Proper ((≡) ==> (≡)) f := ne_proper _.
-  Lemma includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y.
+  Lemma cmra_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
   Proof.
     intros [z ->].
-    apply cmra_included_includedN, (included_preserving f), cmra_included_l.
+    apply cmra_included_includedN, (cmra_monotone f), cmra_included_l.
   Qed.
   Lemma valid_preserving x : ✓ x → ✓ f x.
   Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
@@ -677,7 +677,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
   ra_comm : Comm (≡) (⋅);
   ra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
   ra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
-  ra_pcore_preserving x y cx :
+  ra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
   ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x
 }.
@@ -715,7 +715,7 @@ Section ra_total.
   Context (op_comm : Comm (≡) (@op A _)).
   Context (core_l : ∀ x : A, core x ⋅ x ≡ x).
   Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
-  Context (core_preserving : ∀ x y : A, x ≼ y → core x ≼ core y).
+  Context (core_mono : ∀ x y : A, x ≼ y → core x ≼ core y).
   Context (valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x).
   Lemma ra_total_mixin : RAMixin A.
   Proof.
@@ -725,7 +725,7 @@ Section ra_total.
     - intros x cx Hcx. move: (core_l x). by rewrite /core /= Hcx.
     - intros x cx Hcx. move: (core_idemp x). rewrite /core /= Hcx /=.
       case (total cx)=>[ccx ->]; by constructor.
-    - intros x y cx Hxy%core_preserving Hx. move: Hxy.
+    - intros x y cx Hxy%core_mono Hx. move: Hxy.
       rewrite /core /= Hx /=. case (total y)=> [cy ->]; eauto.
   Qed.
 End ra_total.
@@ -878,8 +878,8 @@ Section prod.
     - intros x y; rewrite prod_pcore_Some prod_pcore_Some'.
       naive_solver eauto using cmra_pcore_idemp.
     - intros x y cx; rewrite prod_included prod_pcore_Some=> -[??] [??].
-      destruct (cmra_pcore_preserving (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
-      destruct (cmra_pcore_preserving (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
+      destruct (cmra_pcore_mono (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
+      destruct (cmra_pcore_mono (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
       exists (z1,z2). by rewrite prod_included prod_pcore_Some.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
     - intros n x y1 y2 [??] [??]; simpl in *.
@@ -942,7 +942,7 @@ Proof.
   split; first apply _.
   - by intros n x [??]; split; simpl; apply validN_preserving.
   - intros x y; rewrite !prod_included=> -[??] /=.
-    by split; apply included_preserving.
+    by split; apply cmra_monotone.
 Qed.
 
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
@@ -1043,7 +1043,7 @@ Section option.
     - intros mx my; setoid_rewrite option_included.
       intros [->|(x&y&->&->&[?|?])]; simpl; eauto.
       + destruct (pcore x) as [cx|] eqn:?; eauto.
-        destruct (cmra_pcore_preserving x y cx) as (?&?&?); eauto 10.
+        destruct (cmra_pcore_mono x y cx) as (?&?&?); eauto 10.
       + destruct (pcore x) as [cx|] eqn:?; eauto.
         destruct (cmra_pcore_proper x y cx) as (?&?&?); eauto 10.
     - intros n [x|] [y|]; rewrite /validN /option_validN /=;
@@ -1102,7 +1102,7 @@ Proof.
   split; first apply _.
   - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
   - intros mx my; rewrite !option_included.
-    intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @included_preserving.
+    intros [->|(x&y&->&->&[?|Hxy])]; simpl; eauto 10 using @cmra_monotone.
     right; exists (f x), (f y). by rewrite {4}Hxy; eauto.
 Qed.
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
diff --git a/algebra/csum.v b/algebra/csum.v
index 341aa6bede821e124e433cfb4cded175515827fc..a1d053517d42620852e5384082054203d5233705 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -202,10 +202,10 @@ Proof.
   - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
     + exists CsumBot. rewrite csum_included; eauto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
-      destruct (cmra_pcore_preserving a a' ca) as (ca'&->&?); auto.
+      destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
       exists (Cinl ca'). rewrite csum_included; eauto 10.
     + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
-      destruct (cmra_pcore_preserving b b' cb) as (cb'&->&?); auto.
+      destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
       exists (Cinr cb'). rewrite csum_included; eauto 10.
   - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
   - intros n [a|b|] y1 y2 Hx Hx'.
@@ -330,7 +330,7 @@ Proof.
   - intros n [a|b|]; simpl; auto using validN_preserving.
   - intros x y; rewrite !csum_included.
     intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
-    eauto 10 using included_preserving.
+    eauto 10 using cmra_monotone.
 Qed.
 
 Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
diff --git a/algebra/dra.v b/algebra/dra.v
index ce053438cce74bb4699c754957398e8a0d03cd2a..059729ff008246b40701209fa586afc270d88133 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -20,7 +20,7 @@ Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
   mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
   mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_preserving x y : 
+  mixin_dra_core_mono x y : 
     ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
 }.
 Structure draT := DRAT {
@@ -78,9 +78,9 @@ Section dra_mixin.
   Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
   Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
   Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_preserving x y : 
+  Lemma dra_core_mono x y : 
     ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
-  Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
+  Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
 End dra_mixin.
 
 Record validity (A : draT) := Validity {
@@ -166,7 +166,7 @@ Proof.
       naive_solver eauto using dra_core_l, dra_core_disjoint_l.
   - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
   - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
-    destruct (dra_core_preserving x z) as (z'&Hz').
+    destruct (dra_core_mono x z) as (z'&Hz').
     unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
     { intros (?&?&?); apply Hz'; tauto. }
     + tauto.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 2b074fb799fa5ba4958fd06021ee1314ade1ba68..c0e59099a938be9bfa46d84683d27cbc8e32a458 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -134,7 +134,7 @@ Proof.
   - intros m i. by rewrite lookup_op lookup_core cmra_core_l.
   - intros m i. by rewrite !lookup_core cmra_core_idemp.
   - intros m1 m2; rewrite !lookup_included=> Hm i.
-    rewrite !lookup_core. by apply cmra_core_preserving.
+    rewrite !lookup_core. by apply cmra_core_mono.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
   - intros n m m1 m2 Hm Hm12.
@@ -399,7 +399,7 @@ Proof.
   split; try apply _.
   - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
   - intros m1 m2; rewrite !lookup_included=> Hm i.
-    by rewrite !lookup_fmap; apply: included_preserving.
+    by rewrite !lookup_fmap; apply: cmra_monotone.
 Qed.
 Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
   gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B).
diff --git a/algebra/gset.v b/algebra/gset.v
index 10eefcfc936939d519dfcb4a229c39e4ef5328c4..c60bd02cd2eb8cd673f0a4ef89341ecfc098ddd9 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -57,7 +57,7 @@ Section gset.
   Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Arguments op _ _ _ _ : simpl never.
 
-  Lemma updateP_alloc_strong (Q : gset_disj K → Prop) (I : gset K) X :
+  Lemma gset_alloc_updateP_strong (Q : gset_disj K → Prop) (I : gset K) X :
     (∀ i, i ∉ X → i ∉ I → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
   Proof.
     intros HQ; apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
@@ -66,16 +66,16 @@ Section gset.
     - apply HQ; set_solver by eauto.
     - apply gset_disj_valid_op. set_solver by eauto.
   Qed.
-  Lemma updateP_alloc (Q : gset_disj K → Prop) X :
+  Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X :
     (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
-  Proof. move=>??. eapply updateP_alloc_strong with (I:=∅); by eauto. Qed.
-  Lemma updateP_alloc_strong' (I : gset K) X :
+  Proof. move=>??. eapply gset_alloc_updateP_strong with (I:=∅); by eauto. Qed.
+  Lemma gset_alloc_updateP_strong' (I : gset K) X :
     GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ I ∧ i ∉ X.
-  Proof. eauto using updateP_alloc_strong. Qed.
-  Lemma updateP_alloc' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
-  Proof. eauto using updateP_alloc. Qed.
+  Proof. eauto using gset_alloc_updateP_strong. Qed.
+  Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
+  Proof. eauto using gset_alloc_updateP. Qed.
 
-  Lemma alloc_singleton_local_update X i Xf :
+  Lemma gset_alloc_local_update X i Xf :
     i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
   Proof.
     intros ??; apply local_update_total; split; simpl.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 06fc17e017ffb67521709121085b8c17e22ad9dd..312017cea454555ce4d2e965ba03bdc6a7e4e26d 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -114,7 +114,7 @@ Section iprod_cmra.
     - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
     - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
     - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
-      by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
+      by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
     - intros n f f1 f2 Hf Hf12.
       set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
@@ -282,7 +282,7 @@ Proof.
   split; first apply _.
   - intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg.
   - intros g1 g2; rewrite !iprod_included_spec=> Hf x.
-    rewrite /iprod_map; apply (included_preserving _), Hf.
+    rewrite /iprod_map; apply (cmra_monotone _), Hf.
 Qed.
 
 Definition iprodC_map `{Finite A} {B1 B2 : A → cofeT}
diff --git a/algebra/list.v b/algebra/list.v
index b4f0803a3bcfe32fd932cdd73a79bb9b71114976..3ab4d27c259f3b75a130ae1163f0814ff01d522b 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -187,7 +187,7 @@ Section cmra.
     - intros l; rewrite list_equiv_lookup=> i.
       by rewrite !list_lookup_core cmra_core_idemp.
     - intros l1 l2; rewrite !list_lookup_included=> Hl i.
-      rewrite !list_lookup_core. by apply cmra_core_preserving.
+      rewrite !list_lookup_core. by apply cmra_core_mono.
     - intros n l1 l2. rewrite !list_lookup_validN.
       setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
     - intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
@@ -374,7 +374,7 @@ Proof.
   - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
     by apply (validN_preserving (fmap f : option A → option B)).
   - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
-    by apply (included_preserving (fmap f : option A → option B)).
+    by apply (cmra_monotone (fmap f : option A → option B)).
 Qed.
 
 Program Definition listURF (F : urFunctor) : urFunctor := {|
diff --git a/algebra/upred.v b/algebra/upred.v
index 752d5de942cc604d1c8e84d613287793964dd7e1..60eeaac81330c0bbf329019fe8acc16fd1b926fe 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -68,7 +68,7 @@ Qed.
 Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
   `{!CMRAMonotone f} (P : uPred M1) :
   uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. naive_solver eauto using uPred_mono, includedN_preserving. Qed.
+Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
 Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed.
 
 Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
@@ -212,7 +212,7 @@ Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
 Next Obligation.
   intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
   apply uPred_mono with (x1 â‹… x3);
-    eauto using cmra_validN_includedN, cmra_preservingN_r, cmra_includedN_le.
+    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
 Qed.
 Next Obligation. naive_solver. Qed.
 Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
@@ -223,7 +223,7 @@ Definition uPred_wand_eq :
 Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Next Obligation.
-  intros M; naive_solver eauto using uPred_mono, @cmra_core_preservingN.
+  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
 Qed.
 Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
 Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
@@ -324,6 +324,13 @@ Arguments uPred_always_if _ !_ _/.
 Notation "â–¡? p P" := (uPred_always_if p P)
   (at level 20, p at level 0, P at level 20, format "â–¡? p  P").
 
+Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
+  Nat.iter n uPred_later P.
+Instance: Params (@uPred_laterN) 2.
+Notation "â–·^ n P" := (uPred_laterN n P)
+  (at level 20, n at level 9, right associativity,
+   format "â–·^ n  P") : uPred_scope.
+
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False).
 Arguments timelessP {_} _ {_}.
 
@@ -454,7 +461,7 @@ Proof.
   intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
   apply (HPQ n'); eauto using cmra_validN_S.
 Qed.
-Global Instance later_proper :
+Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
 Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
 Proof.
@@ -485,10 +492,6 @@ Proof.
     exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
 Qed.
 Global Instance rvs_proper : Proper ((≡) ==> (≡)) (@uPred_rvs M) := ne_proper _.
-Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
-Proof. unfold uPred_iff; solve_proper. Qed.
-Global Instance iff_proper :
-  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.
 
 (** Introduction and elimination rules *)
 Lemma pure_intro φ P : φ → P ⊢ ■ φ.
@@ -548,6 +551,11 @@ Proof.
 Qed.
 
 (* Derived logical stuff *)
+Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
+Proof. unfold uPred_iff; solve_proper. Qed.
+Global Instance iff_proper :
+  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.
+
 Lemma False_elim P : False ⊢ P.
 Proof. by apply (pure_elim False). Qed.
 Lemma True_intro P : P ⊢ True.
@@ -968,7 +976,10 @@ Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ★ P.
 Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ★ □ Q.
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
+Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
 
+(* Conditional always *)
 Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
 Proof. solve_proper. Qed.
 Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
@@ -1029,6 +1040,9 @@ Proof.
 Qed.
 
 (* Later derived *)
+Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
+Proof. by intros ->. Qed.
+Hint Resolve later_mono later_proper.
 Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M).
 Proof. intros P Q; apply later_mono. Qed.
 Global Instance later_flip_mono' :
@@ -1037,18 +1051,69 @@ Proof. intros P Q; apply later_mono. Qed.
 Lemma later_True : ▷ True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
 Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q.
-Proof.
-  apply impl_intro_l; rewrite -later_and.
-  apply later_mono, impl_elim with P; auto.
-Qed.
+Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed.
 Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
   ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
 Proof. apply: anti_symm; eauto using later_exist_2, later_exist_1. Qed.
 Lemma later_wand P Q : ▷ (P -★ Q) ⊢ ▷ P -★ ▷ Q.
-Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
+Proof. apply wand_intro_r;rewrite -later_sep; eauto using wand_elim_l. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
+(* n-times later *)
+Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m).
+Proof. induction m; simpl. by intros ???. solve_proper. Qed.
+Global Instance laterN_proper m :
+  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_laterN M m) := ne_proper _.
+
+Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
+Proof. done. Qed.
+Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
+Proof. induction n; simpl; auto. Qed.
+Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
+Proof. induction n1; simpl; auto. Qed.
+Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
+Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
+
+Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
+Proof. induction n; simpl; auto. Qed.
+Lemma laterN_intro n P : P ⊢ ▷^n P.
+Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
+Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed.
+Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed.
+Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
+Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
+Lemma laterN_exist_1 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ (▷^n ∃ a, Φ a).
+Proof. induction n as [|n IH]; simpl; rewrite ?later_exist_1; auto. Qed.
+Lemma laterN_exist_2 `{Inhabited A} n (Φ : A → uPred M) :
+  (▷^n ∃ a, Φ a) ⊢ ∃ a, ▷^n Φ a.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_exist_2; auto. Qed.
+Lemma laterN_sep n P Q : ▷^n (P ★ Q) ⊣⊢ ▷^n P ★ ▷^n Q.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed.
+
+Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@uPred_laterN M n).
+Proof. intros P Q; apply laterN_mono. Qed.
+Global Instance laterN_flip_mono' n :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_laterN M n).
+Proof. intros P Q; apply laterN_mono. Qed.
+Lemma laterN_True n : ▷^n True ⊣⊢ True.
+Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed.
+Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q.
+Proof.
+  apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono.
+Qed.
+Lemma laterN_exist n `{Inhabited A} (Φ : A → uPred M) :
+  ▷^n (∃ a, Φ a) ⊣⊢ (∃ a, ▷^n Φ a).
+Proof. apply: anti_symm; eauto using laterN_exist_2, laterN_exist_1. Qed.
+Lemma laterN_wand n P Q : ▷^n (P -★ Q) ⊢ ▷^n P -★ ▷^n Q.
+Proof.
+  apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono.
+Qed.
+Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
+Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
+
 (* Own *)
 Lemma ownM_op (a1 a2 : M) :
   uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ★ uPred_ownM a2.
@@ -1063,7 +1128,7 @@ Qed.
 Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
   split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
-  rewrite -(persistent_core a). by apply cmra_core_preservingN.
+  rewrite -(persistent_core a). by apply cmra_core_monoN.
 Qed.
 Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
 Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
@@ -1280,6 +1345,8 @@ Global Instance valid_persistent {A : cmraT} (a : A) :
 Proof. by intros; rewrite /PersistentP always_valid. Qed.
 Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
 Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
+Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P).
+Proof. induction n; apply _. Qed.
 Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
 Proof. intros. by rewrite /PersistentP always_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
diff --git a/docs/algebra.tex b/docs/algebra.tex
index e6fd00b9e673228b5da8c05ee650e48657cfadd7..c22f0baa7a314ce5dd47baf87a313cb3484f29a8 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -64,57 +64,70 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th
 
 \begin{defn}
   A \emph{resource algebra} (RA) is a tuple \\
-  $(\monoid, \mval \subseteq \monoid, \mcore{-}:
-  \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying
+  $(\monoid, \mval \subseteq \monoid, \mcore{{-}}:
+  \monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:
   \begin{align*}
     \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\
     \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{ra-comm} \\
-    \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
-    \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
-    \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
+    \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
+    \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
+    \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
     \All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
     \text{where}\qquad %\qquad\\
-    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
+    \maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\
+    \melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
   \end{align*}
 \end{defn}
 \noindent
 RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences:
 \begin{enumerate}
-\item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset of \emph{valid} elements that is compatible with the operation (\ruleref{ra-valid-op}).
-\item Instead of a single unit that is an identity to every element, there is a function $\mcore{-}$ assigning to every element $\melt$ its \emph{(duplicable) core} $\mcore\melt$, as demanded by \ruleref{ra-core-id}. \\
-  We further demand that $\mcore{-}$ is idempotent (\ruleref{ra-core-idem}) and monotone (\ruleref{ra-core-mono}) with respect to the usual \emph{extension order}, which is defined similar to PCMs (\ruleref{ra-incl}).
+\item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset $\mval$ of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
 
-  This idea of a core is closely related to the concept of \emph{multi-unit separation algebras}~\cite{Dockins+:aplas09}, with the key difference that the core is a \emph{function} defining a \emph{canonical} ``unit'' $\mcore\melt$ for every element~$\melt$.
+This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, CMRAs, in the next subsection.
+
+\item Instead of a single unit that is an identity to every element, we allow
+for an arbitrary number of units, via a function $\mcore{{-}}$ assigning to an element $\melt$ its \emph{(duplicable) core} $\mcore\melt$, as demanded by \ruleref{ra-core-id}.
+  We further demand that $\mcore{{-}}$ is idempotent (\ruleref{ra-core-idem}) and monotone (\ruleref{ra-core-mono}) with respect to the \emph{extension order}, defined similarly to that for PCMs (\ruleref{ra-incl}).
+
+  Notice that the domain of the core is $\maybe\monoid$, a set that adds a dummy element $\mnocore$ to $\monoid$.
+%  (This corresponds to the option type.)
+  Thus, the core can be \emph{partial}: not all elements need to have a unit.
+  We use the metavariable $\maybe\melt$ to indicate elements of  $\maybe\monoid$.
+  We also lift the composition $(\mtimes)$ to $\maybe\monoid$.
+  Partial cores help us to build interesting composite RAs from smaller primitives.
+
+Notice also that the core of an RA is a strict generalization of the unit that any PCM must provide, since $\mcore{{-}}$ can always be picked as a constant function.
 \end{enumerate}
 
 
 \begin{defn}
   It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
-  \[ \All \melt_\f. \melt \mtimes \melt_\f \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval \]
+  \[ \All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \maybe{\melt_\f} \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval \]
 
   We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
 \end{defn}
-The assertion $\melt \mupd \meltsB$ says that every element $\melt_\f$ compatible with $\melt$ (we also call such elements \emph{frames}), must also be compatible with some $\meltB \in \meltsB$.
+The assertion $\melt \mupd \meltsB$ says that every element $\maybe{\melt_\f}$ compatible with $\melt$ (we also call such elements \emph{frames}), must also be compatible with some $\meltB \in \meltsB$.
+Notice that $\maybe{\melt_\f}$ could be $\mnocore$, so the frame-preserving update can also be applied to elements that have \emph{no} frame.
 Intuitively, this means that whatever assumptions the rest of the program is making about the state of $\gname$, if these assumptions are compatible with $\melt$, then updating to $\meltB$ will not invalidate any of these assumptions.
 Since Iris ensures that the global ghost state is valid, this means that we can soundly update the ghost state from $\melt$ to a non-deterministically picked $\meltB \in \meltsB$.
 
 \subsection{CMRA}
 
 \begin{defn}
-  A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \nfn \monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying
+  A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
   \begin{align*}
     \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
-    \All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\
+    \All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\
     \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
     \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
-    \All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
-    \All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
-    \All \melt, \meltB.& \melt \mincl \meltB \Ra \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\
+    \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
+    \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
+    \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\
     \All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\
     \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$\melt \in \mval_n \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
     &\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{cmra-extend} \\
     \text{where}\qquad\qquad\\
-    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl}\\
+    \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\
     \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}
   \end{align*}
 \end{defn}
@@ -143,12 +156,10 @@ The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the foll
 \end{tikzpicture}\end{center}
 where the $n$-equivalence at the bottom is meant to apply to the pairs of elements, \ie we demand $\melt_1 \nequiv{n} \meltB_1$ and $\melt_2 \nequiv{n} \meltB_2$.
 In other words, extension carries the decomposition of $\meltB$ into $\meltB_1$ and $\meltB_2$ over the $n$-equivalence of $\melt$ and $\meltB$, and yields a corresponding decomposition of $\melt$ into $\melt_1$ and $\melt_2$.
-This operation is needed to prove that $\later$ commutes with existential quantification and separating conjunction:
+This operation is needed to prove that $\later$ commutes with separating conjunction:
 \begin{mathpar}
-  \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop}
-  \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}
+  \axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}
 \end{mathpar}
-(This assumes that the type $\type$ is non-empty.)
 
 \begin{defn}
   An element $\munit$ of a CMRA $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
@@ -157,12 +168,17 @@ This operation is needed to prove that $\later$ commutes with existential quanti
   \item $\munit$ is a left-identity of the operation: \\
     $\All \melt \in M. \munit \mtimes \melt = \melt$
   \item $\munit$ is a discrete COFE element
+  \item $\munit$ is its own core: \\ $\mcore\munit = \munit$
   \end{enumerate}
 \end{defn}
 
+\begin{lem}\label{lem:cmra-unit-total-core}
+  If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$.
+\end{lem}
+
 \begin{defn}
   It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
-  \[ \All n, \melt_\f. \melt \mtimes \melt_\f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval_n \]
+  \[ \All n, \maybe{\melt_\f}. \melt \mtimes \maybe{\melt_\f} \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval_n \]
 
   We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
 \end{defn}
@@ -193,7 +209,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
 \begin{defn}
   The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows.
 \end{defn}
-Note that $\CMRAs$ is a subcategory of $\COFEs$.
+Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
 
 
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 03e331a135ecd68c13ec52e3e1e2f0010b340c68..cf4114d7b525dea873d4bb0b180db09f46df1f42 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -59,6 +59,35 @@ Frame-preserving updates on the $M_i$ lift to the product:
   {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
 \end{mathpar}
 
+\subsection{Sum}
+\label{sec:summ}
+
+The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as:
+\begin{align*}
+  \monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \bot \\
+  \mval_n \eqdef{}& \setComp{\cinl(\melt_1)\!}{\!\melt_1 \in \mval'_n}
+    \cup \setComp{\cinr(\melt_2)\!}{\!\melt_2 \in \mval''_n}  \\
+  \cinl(\melt_1) \mtimes \cinl(\meltB_1) \eqdef{}& \cinl(\melt_1 \mtimes \meltB_1)  \\
+%  \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
+%  \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \\
+  \mcore{\cinl(\melt_1)} \eqdef{}& \begin{cases}\mnocore & \text{if $\mcore{\melt_1} = \mnocore$} \\ \cinl({\mcore{\melt_1}}) & \text{otherwise} \end{cases}
+\end{align*}
+The composition and core for $\cinr$ are defined symmetrically.
+The remaining cases of the composition and core are all $\bot$.
+Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.
+
+We obtain the following frame-preserving updates, as well as their symmetric counterparts:
+\begin{mathpar}
+  \inferH{sum-update}
+  {\melt \mupd_{M_1} \meltsB}
+  {\cinl(\melt) \mupd \setComp{ \cinl(\meltB)}{\meltB \in \meltsB}}
+
+  \inferH{sum-swap}
+  {\All \melt_\f, n. \melt \mtimes \melt_\f \notin \mval'_n \and \meltB \in \mval''}
+  {\cinl(\melt) \mupd \cinr(\meltB)}
+\end{mathpar}
+Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}.
+
 \subsection{Finite partial function}
 \label{sec:fpfnm}
 
@@ -118,59 +147,17 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
   \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y}
 \end{mathpar}
 
-\subsection{One-shot}
-
-The purpose of the one-shot CMRA is to lazily initialize the state of a ghost location.
-Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
-\begin{align*}
-  \oneshotm(\monoid) \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\
-  \mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n}
-\\%\end{align*}
-%\begin{align*}
-  \osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\
-  \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
-  \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt)
-\end{align*}%
-Notice that $\oneshotm(\monoid)$ is a disjoint sum with the four constructors (injections) $\ospending$, $\osshot$, $\munit$ and $\bot$.
-The remaining cases of composition go to $\bot$.
-\begin{align*}
-  \mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\
-  \mcore{\munit} \eqdef{}& \munit &  \mcore{\bot} \eqdef{}& \bot
-\end{align*}
-The step-indexed equivalence is inductively defined as follows:
-\begin{mathpar}
-  \axiom{\ospending \nequiv{n} \ospending}
-
-  \infer{\melt \nequiv{n} \meltB}{\osshot(\melt) \nequiv{n} \osshot(\meltB)}
-
-  \axiom{\munit \nequiv{n} \munit}
-
-  \axiom{\bot \nequiv{n} \bot}
-\end{mathpar}
-$\oneshotm(-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
-
-We obtain the following frame-preserving updates:
-\begin{mathpar}
-  \inferH{oneshot-shoot}
-  {\melt \in \mval}
-  {\ospending \mupd \osshot(\melt)}
-
-  \inferH{oneshot-update}
-  {\melt \mupd \meltsB}
-  {\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}}
-\end{mathpar}
 
 \subsection{Exclusive CMRA}
 
 Given a cofe $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
 \begin{align*}
-  \exm(\cofe) \eqdef{}& \exinj(\cofe) + \munit + \bot \\
-  \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot} \\
-  \munit \mtimes \exinj(x) \eqdef{}& \exinj(x) \mtimes \munit \eqdef \exinj(x)
+  \exm(\cofe) \eqdef{}& \exinj(\cofe) + \bot \\
+  \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot}
 \end{align*}
-The remaining cases of composition go to $\bot$.
+All cases of composition go to $\bot$.
 \begin{align*}
-  \mcore{\exinj(x)} \eqdef{}& \munit & \mcore{\munit} \eqdef{}& \munit &
+  \mcore{\exinj(x)} \eqdef{}& \mnocore &
   \mcore{\bot} \eqdef{}& \bot
 \end{align*}
 The step-indexed equivalence is inductively defined as follows:
diff --git a/docs/iris.sty b/docs/iris.sty
index fe64b4e90ac11fe9a53c47a4269b948610819e75..c95c30e234666529908eb1cfc76aa0555699ecb4 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -35,7 +35,7 @@
 \newcommand{\upclose}{\mathord{\uparrow}}
 \newcommand{\ALT}{\ |\ }
 
-\newcommand{\spac}{\,} % a space
+\newcommand{\spac}{\:} % a space
 
 \def\All #1.{\forall #1.\spac}%
 \def\Exists #1.{\exists #1.\spac}%
@@ -56,6 +56,8 @@
 \newcommand{\eqdef}{\triangleq}
 \newcommand{\bnfdef}{\vcentcolon\vcentcolon=}
 
+\newcommand{\maybe}[1]{#1^?}
+
 \newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
 \newcommand*\set[1]{\left\{#1\right\}}
 \newcommand*\record[1]{\left\{\spac#1\spac\right\}}
@@ -67,6 +69,7 @@
   \end{array}
 }
 
+\newcommand{\op}{\textrm{op}}
 \newcommand{\dom}{\mathrm{dom}}
 \newcommand{\cod}{\mathrm{cod}}
 \newcommand{\chain}{\mathrm{chain}}
@@ -112,8 +115,6 @@
 
 
 %% Some commonly used identifiers
-\newcommand{\op}{\textrm{op}}
-
 \newcommand{\SProp}{\textdom{SProp}}
 \newcommand{\UPred}{\textdom{UPred}}
 \newcommand{\mProp}{\textdom{Prop}} % meta-level prop
@@ -144,10 +145,9 @@
 
 \newcommand{\f}{\mathrm{f}} % for "frame"
 
-\newcommand{\mcar}[1]{|#1|}
-\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
 \newcommand{\munit}{\varepsilon}
-\newcommand{\mcore}[1]{\llparenthesis#1\rrparenthesis}
+\newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
+\newcommand{\mnocore}\top
 \newcommand{\mtimes}{\mathbin{\cdot}}
 
 \newcommand{\mupd}{\rightsquigarrow}
@@ -328,6 +328,9 @@
 % STANDARD DERIVED CONSTRUCTIONS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\newcommand{\unittt}{()}
+\newcommand{\unit}{1}
+
 % Agreement
 \newcommand{\agm}{\ensuremath{\textmon{Ag}}}
 \newcommand{\aginj}{\textlog{ag}}
@@ -347,6 +350,11 @@
 \newcommand{\AuthInv}{\textsf{AuthInv}}
 \newcommand{\Auth}{\textsf{Auth}}
 
+% Sum
+\newcommand{\csumm}{\mathrel{+_{\!\bot}}}
+\newcommand{\cinl}{\textsf{inl}}
+\newcommand{\cinr}{\textsf{inr}}
+
 % One-Shot
 \newcommand{\oneshotm}{\ensuremath{\textmon{OneShot}}}
 \newcommand{\ospending}{\textlog{pending}}
diff --git a/docs/logic.tex b/docs/logic.tex
index 24a8ca03a3b930e2aa59ea06e32d44bfc309a6bb..94b627f16a121040314d985cb3ea23dab7e99a6e 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -10,18 +10,6 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
   A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_\f$ is forked off.
 \item All values are stuck:
 \[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
-\item There is a predicate defining \emph{atomic} expressions satisfying
-\let\oldcr\cr
-\begin{mathpar}
-  {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and
-  {{
-    \begin{inbox}
-\All\expr_1, \state_1, \expr_2, \state_2, \expr_\f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
-    \end{inbox}
-}}
-\end{mathpar}
-In other words, atomic expression \emph{reduce in one step to a value}.
-It does not matter whether they fork off an arbitrary expression.
 \end{itemize}
 
 \begin{defn}
@@ -29,6 +17,11 @@ It does not matter whether they fork off an arbitrary expression.
   \[ \Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
 \end{defn}
 
+\begin{defn}
+  An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:
+  \[ \All\state_1, \expr_2, \state_2, \expr_\f. \expr, \state_1 \step \expr_2, \state_2, \expr_\f \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
+\end{defn}
+
 \begin{defn}[Context]
   A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
   \begin{enumerate}[itemsep=0pt]
@@ -68,8 +61,8 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
 
 To instantiate Iris, you need to define the following parameters:
 \begin{itemize}
-\item A language $\Lang$
-\item A locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit
+\item A language $\Lang$, and
+\item a locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(A)$ is a total function.)
 \end{itemize}
 
 \noindent
@@ -141,7 +134,7 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
 Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
 We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
 If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
-\ralf{$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.}
+%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
 
 Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
 This is a \emph{meta-level} assertion about propositions, defined as follows:
diff --git a/docs/model.tex b/docs/model.tex
index d8595b6bae293ca094ea2efda9123c55edea95df..f6ce778183b83d9714185250e1a298940cf0736e 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -46,14 +46,13 @@ We introduce an additional logical connective $\ownM\melt$, which will later be
 
 For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.
 
-
 \subsection{Iris model}
 
 \paragraph{Semantic domain of assertions.}
 The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$.
 We start by defining the functor that assembles the CMRAs we need to the global resource CMRA:
 \begin{align*}
-  \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
+  \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
 \end{align*}
 Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
 $\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
@@ -87,7 +86,7 @@ We only have to define the interpretation of the missing connectives, the most i
   \wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t]
     \rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land 
     \dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\
-    \All\iname \in \mask, \prop. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
+    \All\iname \in \mask, \prop \in \iProp. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
   \end{inbox}\\
 	\wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))}
 \end{align*}
@@ -95,7 +94,7 @@ We only have to define the interpretation of the missing connectives, the most i
 \typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
 \begin{align*}
 	\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
-            \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
+            \All \rs_\f, k, \mask_\f, \state.& 0 < k \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
             \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
           \end{aligned}}
 \end{align*}
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 361b83a3a61a055095cf72f16f8c079a77a0a698..e84f90afecc010c45cfba8082db4859028aaaebc 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -82,7 +82,7 @@ Tactic Notation "wp_seq" := wp_let.
 Tactic Notation "wp_op" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
+    lazymatch eval hnf in e' with
     | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
     | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
     | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
diff --git a/prelude/collections.v b/prelude/collections.v
index 98a1a93efdedf40c5b600def194349f32dd64c92..7762ce91a3398701a4cb186635d3d664a4afa9f2 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -645,6 +645,11 @@ Section collection.
       intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
       destruct (decide (x ∈ X)); intuition.
     Qed.
+    Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ⊥ Z.
+    Proof.
+      split; [|set_solver].
+      exists (Y ∖ X); split; [auto using union_difference|set_solver].
+    Qed.
     Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅.
     Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. set_solver. Qed.
     Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y.
@@ -657,6 +662,8 @@ Section collection.
     Proof. unfold_leibniz. apply non_empty_difference. Qed.
     Lemma empty_difference_subseteq_L X Y : X ∖ Y = ∅ → X ⊆ Y.
     Proof. unfold_leibniz. apply empty_difference_subseteq. Qed.
+    Lemma subseteq_disjoint_union_L X Y : X ⊆ Y ↔ ∃ Z, Y = X ∪ Z ∧ X ⊥ Z.
+    Proof. unfold_leibniz. apply subseteq_disjoint_union. Qed.
   End dec.
 End collection.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 841d143d93ffbab854e8b55c522b43bc63640b59..ba098d733e1732ceb6d86d93e095ec1e612d2850 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -103,14 +103,14 @@ Section auth.
     iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
     iInv N as (a') "[Hγ Hφ]".
     iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid _ with "#Hγ") as "Hvalid".
+    iDestruct (own_valid with "#Hγ") as "Hvalid".
     iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
     iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
     rewrite ->(left_id _ _) in Ha'; setoid_subst.
     iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
     { iApply "HΨ"; by iSplit. }
     iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
-    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
+    iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
     iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
     iNext. iExists (b â‹… af). by iFrame.
   Qed.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index fd10371492499454744d6af34fbdfb640ebd2684..793b69c51a7c49d081b691da5ac2ab3ee86c2a81 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -15,11 +15,11 @@ Section box_defs.
 
   Definition slice_name := gname.
 
-  Definition box_own_auth (γ : slice_name)
-    (a : auth (option (excl bool))) : iProp := own γ (a, ∅).
+  Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool)))
+    := own γ (a, (∅:option (agree (later (iPrePropG Λ Σ))))).
 
   Definition box_own_prop (γ : slice_name) (P : iProp) : iProp :=
-    own γ (∅:auth _, Some (to_agree (Next (iProp_unfold P)))).
+    own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
 
   Definition slice_inv (γ : slice_name) (P : iProp) : iProp :=
     (∃ b, box_own_auth γ (● Excl' b) ★ box_own_prop γ P ★ if b then P else True)%I.
@@ -70,8 +70,7 @@ Proof.
   rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
   iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
   iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
-  rewrite -{1}(right_id ∅ _ (Excl' b2)) -{1}(right_id ∅ _ (Excl' b3)).
-  by apply auth_update, option_local_update, exclusive_local_update.
+  by apply auth_update_no_frame, option_local_update, exclusive_local_update.
 Qed.
 
 Lemma box_own_agree γ Q1 Q2 :
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index e227bd5ade1f622f7aedd927538dfe060f95ccb3..92c4adc27d02c2e6a0f15e21c96fc69cf59ee700 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -18,13 +18,14 @@ Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
 
 (** * Properties of own *)
-Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
+Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Λ Σ A _ γ).
 Proof. rewrite !own_eq. solve_proper. Qed.
-Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (own γ) := ne_proper _.
+Global Instance own_proper γ :
+  Proper ((≡) ==> (⊣⊢)) (@own Λ Σ A _ γ) := ne_proper _.
 
 Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
 Proof. by rewrite !own_eq /own_def -ownG_op to_globalF_op. Qed.
-Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (own γ).
+Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (@own Λ Σ A _ γ).
 Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
 Proof.
@@ -81,11 +82,17 @@ Proof.
 Qed.
 End global.
 
+Arguments own_valid {_ _ _} [_] _ _.
+Arguments own_valid_l {_ _ _} [_] _ _.
+Arguments own_valid_r {_ _ _} [_] _ _.
+Arguments own_updateP {_ _ _} [_] _ _ _ _ _.
+Arguments own_update {_ _ _} [_] _ _ _ _ _.
+
 Section global_empty.
 Context `{i : inG Λ Σ (A:ucmraT)}.
 Implicit Types a : A.
 
-Lemma own_empty γ E : True ={E}=> own γ ∅.
+Lemma own_empty γ E : True ={E}=> own γ (∅:A).
 Proof.
   rewrite ownG_empty !own_eq /own_def.
   apply pvs_ownG_update, iprod_singleton_update_empty.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 6d534c266cdbfe4c294b128aca05a682e9e1db9d..48403855e61fd192d625c7e54af8377c8c4c33c5 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -28,6 +28,7 @@ Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
   inG_prf : A = projT2 Σ inG_id (iPreProp Λ (globalF Σ))
 }.
 Arguments inG_id {_ _ _} _.
+Hint Mode inG - - + : typeclass_instances.
 
 Definition to_globalF `{i : inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
   iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
@@ -39,17 +40,18 @@ Section to_globalF.
 Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
 
-Global Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
+Global Instance to_globalF_ne γ n :
+  Proper (dist n ==> dist n) (@to_globalF Λ Σ A _ γ).
 Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
 Lemma to_globalF_op γ a1 a2 :
   to_globalF γ (a1 ⋅ a2) ≡ to_globalF γ a1 ⋅ to_globalF γ a2.
 Proof.
   by rewrite /to_globalF iprod_op_singleton op_singleton cmra_transport_op.
 Qed.
-Global Instance to_globalF_timeless γ m: Timeless m → Timeless (to_globalF γ m).
+Global Instance to_globalF_timeless γ a : Timeless a → Timeless (to_globalF γ a).
 Proof. rewrite /to_globalF; apply _. Qed.
-Global Instance to_globalF_persistent γ m :
-  Persistent m → Persistent (to_globalF γ m).
+Global Instance to_globalF_persistent γ a :
+  Persistent a → Persistent (to_globalF γ a).
 Proof. rewrite /to_globalF; apply _. Qed.
 End to_globalF.
 
diff --git a/program_logic/resources.v b/program_logic/resources.v
index b12df6173c90aab79155eb1b6bc57f8bd210b5a0..1590ee7374bdb68b0b5ddd2fb16d1b7f7b28f680 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -109,7 +109,7 @@ Proof.
   - by intros ?; constructor; rewrite /= cmra_core_l.
   - by intros ?; constructor; rewrite /= cmra_core_idemp.
   - intros r1 r2; rewrite !res_included.
-    by intros (?&?&?); split_and!; apply cmra_core_preserving.
+    by intros (?&?&?); split_and!; apply cmra_core_mono.
   - intros n r1 r2 (?&?&?);
       split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
   - intros n r r1 r2 (?&?&?) [???]; simpl in *.
@@ -212,7 +212,7 @@ Proof.
   split; first apply _.
   - intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
   - by intros r1 r2; rewrite !res_included;
-      intros (?&?&?); split_and!; simpl; try apply: included_preserving.
+      intros (?&?&?); split_and!; simpl; try apply: cmra_monotone.
 Qed.
 Definition resC_map {Λ} {A A' : cofeT} {M M' : ucmraT}
     (f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 44b6be39033067723c81cc8dae6a93b89a2109d8..97f37f828f7bf005268b7053cab3a29b267f0cb1 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -5,9 +5,14 @@ From iris.heap_lang Require Import notation par proofmode.
 From iris.proofmode Require Import invariants.
 Import uPred.
 
+Definition one_shotR (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
+  csumR (exclR unitC) (agreeR $ laterC $ F (iPrePropG Λ Σ)).
+Definition Pending {Λ Σ F} : one_shotR Λ Σ F := Cinl (Excl ()).
+Definition Shot {Λ Σ} {F : cFunctor} (x : F (iPropG Λ Σ)) : one_shotR Λ Σ F :=
+  Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
+
 Class oneShotG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
-  one_shot_inG :>
-    inG Λ Σ (csumR (exclR unitC) (agreeR $ laterC $ F (iPrePropG Λ Σ))).
+  one_shot_inG :> inG Λ Σ (one_shotR Λ Σ F).
 Definition oneShotGF (F : cFunctor) : gFunctor :=
   GFunctor (csumRF (exclRF unitC) (agreeRF (â–¶ F))).
 Instance inGF_oneShotG  `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
@@ -19,15 +24,13 @@ Definition client eM eW1 eW2 : expr :=
 Global Opaque client.
 
 Section proof.
-Context (G : cFunctor).
-Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ G}.
+Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ F}.
 Context (N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
-Local Notation X := (G iProp).
+Local Notation X := (F iProp).
 
 Definition barrier_res γ (Φ : X → iProp) : iProp :=
-  (∃ x, own γ (Cinr $ to_agree $
-               Next (cFunctor_map G (iProp_fold, iProp_unfold) x)) ★ Φ x)%I.
+  (∃ x, own γ (Shot x) ★ Φ x)%I.
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp) `{!Closed [] e} :
   recv N l (barrier_res γ Φ) ★ (∀ x, {{ Φ x }} e {{ _, Ψ x }})
@@ -57,7 +60,7 @@ Proof.
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
     rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
-    rewrite (ne_proper (cFunctor_map G) (cid, cid) (_ â—Ž _, _ â—Ž _)); last first.
+    rewrite (ne_proper (cFunctor_map F) (cid, cid) (_ â—Ž _, _ â—Ž _)); last first.
     { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
     rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
   iNext. iRewrite -"Hxx" in "Hx'".
@@ -73,7 +76,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
   ⊢ WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
   iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
-  iPvs (own_alloc (Cinl (Excl ()))) as (γ) "Hγ". done.
+  iPvs (own_alloc (Pending : one_shotR heap_lang Σ F)) as (γ) "Hγ". done.
   wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
   iFrame "Hh". iIntros (l) "[Hr Hs]".
   set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
@@ -81,8 +84,8 @@ Proof.
   iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
   - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
-    iPvs (own_update _ _ (Cinr (to_agree _)) with "Hγ") as "Hx".
-    by apply cmra_update_exclusive.
+    iPvs (own_update with "Hγ") as "Hx".
+    { by apply (cmra_update_exclusive (Shot x)). }
     iApply signal_spec; iFrame "Hs"; iSplit; last done.
     iExists x; auto.
   - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 1539f49e861fae71004d2152eb51f45be76acb42..66479873d92a06b8be0450c81d1574cb3d08357e 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -20,22 +20,21 @@ Definition one_shot_example : val := λ: <>,
     end)).
 Global Opaque one_shot_example.
 
-Class one_shotG Σ :=
-  one_shot_inG :> inG heap_lang Σ (csumR (exclR unitC)(dec_agreeR Z)).
-Definition one_shotGF : gFunctorList :=
-  [GFunctor (constRF (csumR (exclR unitC)(dec_agreeR Z)))].
+Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
+Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
+Definition Shot (n : Z) : one_shotR := (Cinr (DecAgree n) : one_shotR).
+
+Class one_shotG Σ := one_shot_inG :> inG heap_lang Σ one_shotR.
+Definition one_shotGF : gFunctorList := [GFunctor (constRF one_shotR)].
 Instance inGF_one_shotG Σ : inGFs heap_lang Σ one_shotGF → one_shotG Σ.
 Proof. intros [? _]; apply: inGF_inG. Qed.
 
-Notation Pending := (Cinl (Excl ())).
-
 Section proof.
 Context `{!heapG Σ, !one_shotG Σ} (N : namespace) (HN : heapN ⊥ N).
 Local Notation iProp := (iPropG heap_lang Σ).
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
-  (l ↦ NONEV ★ own γ Pending ∨
-  ∃ n : Z, l ↦ SOMEV #n ★ own γ (Cinr (DecAgree n)))%I.
+  (l ↦ NONEV ★ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ★ own γ (Shot n))%I.
 
 Lemma wp_one_shot (Φ : val → iProp) :
   heap_ctx ★ (∀ f1 f2 : val,
@@ -53,18 +52,18 @@ Proof.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + wp_cas_suc. iSplitL; [|by iLeft].
       iPvs (own_update with "Hγ") as "Hγ".
-      { by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
+      { by apply cmra_update_exclusive with (y:=Shot n). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
     + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
   - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
     iAssert (∃ v, l ↦ v ★ ((v = NONEV ★ own γ Pending) ∨
-       ∃ n : Z, v = SOMEV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv".
+       ∃ n : Z, v = SOMEV #n ★ own γ (Shot n)))%I with "[-]" as "Hv".
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
       + iExists NONEV. iFrame. eauto.
       + iExists (SOMEV #m). iFrame. eauto. }
     iDestruct "Hv" as (v) "[Hl Hv]". wp_load; iPvsIntro.
     iAssert (one_shot_inv γ l ★ (v = NONEV ∨ ∃ n : Z,
-      v = SOMEV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "[$ #Hv]".
+      v = SOMEV #n ★ own γ (Shot n)))%I with "[-]" as "[$ #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
@@ -73,7 +72,7 @@ Proof.
     { by wp_match. }
     wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as (m') "[Hl Hγ]".
-    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
+    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
     wp_load; iPvsIntro.
     iCombine "Hγ" "Hγ'" as "Hγ".
     iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.