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..c473c83b6c5f5f868a789d489536841fff1810d2 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];
@@ -222,9 +222,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 cca312c3a475b5260037f1a87e24523d5b2cdb37..10eefcfc936939d519dfcb4a229c39e4ef5328c4 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -84,3 +84,6 @@ Section gset.
       rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
   Qed.
 End gset.
+
+Arguments gset_disjR _ {_ _}.
+Arguments gset_disjUR _ {_ _}.
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 be93b5991b0ac932cf9de389c7f0b72b56e57277..a8fe0398abf3342910385840c277f2de42a4863b 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.
@@ -1038,7 +1038,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.
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/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/proofmode/classes.v b/proofmode/classes.v
index b84436e8ef4529a1b40bdb29c11142facd3c44af..50fdd54b659a0806122fbc5ef6221b167a0e6fb1 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -301,10 +301,6 @@ Global Arguments from_exist {_} _ _ {_}.
 Global Instance from_exist_exist {A} (Φ: A → uPred M): FromExist (∃ a, Φ a) Φ.
 Proof. done. Qed.
 
-Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
-  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
-Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
-
 Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
   into_exist : P ⊢ ∃ x, Φ x.
 Global Arguments into_exist {_} _ _ {_}.
@@ -316,4 +312,7 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
 Global Instance into_exist_always {A} P (Φ : A → uPred M) :
   IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
+
+Class TimelessElim (Q : uPred M) :=
+  timeless_elim `{!TimelessP P} : ▷ P ★ (P -★ Q) ⊢ Q.
 End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 311a4d0ce2b143ed8934463438206045f17d5245..36f52d72a7ec20f72712fb6ad7cd31d7a0b472fe 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -375,6 +375,16 @@ Proof.
   by rewrite right_id always_and_sep_l' wand_elim_r HQ.
 Qed.
 
+Lemma tac_timeless Δ Δ' i p P Q :
+  TimelessElim Q →
+  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
+  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q.
+Proof.
+  intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
+  by rewrite always_if_later right_id HQ timeless_elim.
+Qed.
+
 (** * Always *)
 Lemma tac_always_intro Δ Q : envs_persistent Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
 Proof. intros. by apply: always_intro. Qed.
@@ -719,6 +729,10 @@ Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
 Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
 
 (** * Existential *)
+Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
+  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
+Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
+
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoExist P Φ →
   (∀ a, ∃ Δ',
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index e919ea13ed79a7e39039e44bd2c0b6a4d6ae6c57..df3203323e96350820f988dab219d639f553fec6 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -30,6 +30,12 @@ Global Instance into_wand_pvs E1 E2 R P Q :
   IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
 Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
+Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
+Proof.
+  intros P ?. rewrite (pvs_timeless E1 P) pvs_frame_r.
+  by rewrite wand_elim_r pvs_trans; last set_solver.
+Qed.
+
 Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
     (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
   is_fsa : P ⊣⊢ fsa E Φ;
@@ -48,6 +54,12 @@ Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
 Proof.
   intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
 Qed.
+Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
+  IsFSA Q E fsa fsaV Φ → TimelessElim Q.
+Proof.
+  intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
+  by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
+Qed.
 
 Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → (Δ ⊢ Q) → Δ ⊢ |={E1,E2}=> Q.
 Proof. intros -> ->. apply pvs_intro. Qed.
@@ -74,26 +86,6 @@ Proof.
   intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
   eapply tac_pvs_elim; set_solver.
 Qed.
-
-Lemma tac_pvs_timeless Δ Δ' E1 E2 i p P Q :
-  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
-  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
-  (Δ' ={E1,E2}=> Q) → Δ ={E1,E2}=> Q.
-Proof.
-  intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
-  rewrite always_if_later (pvs_timeless E1 (â–¡?_ P)%I) pvs_frame_r.
-  by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
-Qed.
-
-Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
-  IsFSA Q E fsa fsaV Φ →
-  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
-  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
-  (Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
-Proof.
-  intros ????. rewrite (is_fsa Q) -fsa_pvs_fsa.
-  eauto using tac_pvs_timeless.
-Qed.
 End pvs.
 
 Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
@@ -161,26 +153,5 @@ Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
   iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
-Tactic Notation "iTimeless" constr(H) :=
-  match goal with
-  | |- _ ⊢ |={_,_}=> _ =>
-     eapply tac_pvs_timeless with _ H _ _;
-       [env_cbv; reflexivity || fail "iTimeless:" H "not found"
-       |let P := match goal with |- TimelessP ?P => P end in
-        apply _ || fail "iTimeless: " P "not timeless"
-       |env_cbv; reflexivity|simpl]
-  | |- _ =>
-     eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
-       [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
-        apply _ || fail "iTimeless: " P "not a pvs"
-       |env_cbv; reflexivity || fail "iTimeless:" H "not found"
-       |let P := match goal with |- TimelessP ?P => P end in
-        apply _ || fail "iTimeless: " P "not timeless"
-       |env_cbv; reflexivity|simpl]
-  end.
-
-Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
-  iTimeless H; iDestruct H as Hs.
-
 Hint Extern 2 (of_envs _ ⊢ _) =>
   match goal with |- _ ⊢ (|={_}=> _)%I => iPvsIntro end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 8e6a504daeeecd6610e9e955fc0f37e0fa613d72..3901386c43ad909a114baeac44a5608ad5a6b1fd 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -501,6 +501,15 @@ Tactic Notation "iNext":=
     |let P := match goal with |- FromLater ?P _ => P end in
      apply _ || fail "iNext:" P "does not contain laters"|].
 
+Tactic Notation "iTimeless" constr(H) :=
+  eapply tac_timeless with _ H _ _;
+    [let Q := match goal with |- TimelessElim ?Q => Q end in
+     apply _ || fail "iTimeless: cannot eliminate later in goal" Q
+    |env_cbv; reflexivity || fail "iTimeless:" H "not found"
+    |let P := match goal with |- TimelessP ?P => P end in
+     apply _ || fail "iTimeless: " P "not timeless"
+    |env_cbv; reflexivity|].
+
 (** * Introduction tactic *)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
   [ (* (∀ _, _) *) apply tac_forall_intro; intros x