From 780f6b82266d8dd80f6471d805a2454a77b38dca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Nov 2015 16:51:21 +0100
Subject: [PATCH] Step-indexed order on CMRAs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Remove the order from RAs, it is now defined in terms of the â‹… operation.
* Define ownership using the step-indexed order.
* Remove the order also from DRAs and change STS accordingly. While doing
  that, I changed STS to no longer use decidable token sets, which removes the
  requirement of decidable equality on tokens.
---
 iris/agree.v          |  25 ++++---
 iris/auth.v           |  39 +++++------
 iris/cmra.v           | 147 ++++++++++++++++++++++++++++++------------
 iris/cmra_maps.v      |  86 +++++++++++++++---------
 iris/dra.v            |  64 +++++++++---------
 iris/excl.v           |  25 +++----
 iris/language.v       |  31 +++++++++
 iris/logic.v          |  30 ++++-----
 iris/ra.v             |  55 +++++++---------
 iris/sts.v            |  84 +++++++++++-------------
 prelude/collections.v |   4 ++
 11 files changed, 346 insertions(+), 244 deletions(-)
 create mode 100644 iris/language.v

diff --git a/iris/agree.v b/iris/agree.v
index 38aaf15f0..2525dff1f 100644
--- a/iris/agree.v
+++ b/iris/agree.v
@@ -57,7 +57,6 @@ Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Global Instance agree_unit : Unit (agree A) := id.
 Global Instance agree_minus : Minus (agree A) := λ x y, x.
-Global Instance agree_included : Included (agree A) := λ x y, y ≡ x ⋅ y.
 Instance: Commutative (≡) (@op (agree A) _).
 Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
 Definition agree_idempotent (x : agree A) : x ⋅ x ≡ x.
@@ -80,6 +79,11 @@ Proof.
     repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
     by cofe_subst; rewrite !agree_idempotent.
 Qed.
+Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ={n}= x ⋅ y.
+Proof.
+  split; [|by intros ?; exists y].
+  by intros [z Hz]; rewrite Hz, (associative _), agree_idempotent.
+Qed.
 Global Instance agree_cmra : CMRA (agree A).
 Proof.
   split; try (apply _ || done).
@@ -87,23 +91,20 @@ Proof.
     rewrite <-(proj2 Hxy n'), (Hx n') by eauto using agree_valid_le.
     by apply dist_le with n; try apply Hxy.
   * by intros n x1 x2 Hx y1 y2 Hy.
-  * by intros x y1 y2 Hy ?; do 2 red; rewrite <-Hy.
   * intros x; split; [apply agree_valid_0|].
     by intros n'; rewrite Nat.le_0_r; intros ->.
   * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
     rewrite (Hx n') by auto; symmetry; apply dist_le with n; try apply Hx; auto.
   * intros x; apply agree_idempotent.
-  * intros x y; change (x ⋅ y ≡ x ⋅ (x ⋅ y)).
-    by rewrite (associative _), agree_idempotent.
   * by intros x y n [(?&?&?) ?].
-  * by intros x y; do 2 red; rewrite (associative _), agree_idempotent.
+  * by intros x y n; rewrite agree_includedN.
 Qed.
 Lemma agree_op_inv (x y1 y2 : agree A) n :
   validN n x → x ={n}= y1 ⋅ y2 → y1 ={n}= y2.
 Proof. by intros [??] Hxy; apply Hxy. Qed.
 Global Instance agree_extend : CMRAExtend (agree A).
 Proof.
-  intros x y1 y2 n ? Hx; exists (x,x); simpl; split.
+  intros n x y1 y2 ? Hx; exists (x,x); simpl; split.
   * by rewrite agree_idempotent.
   * by rewrite Hx, (agree_op_inv x y1 y2), agree_idempotent by done.
 Qed.
@@ -131,15 +132,13 @@ Section agree_map.
   Global Instance agree_map_ne n : Proper (dist n ==> dist n) agree_map.
   Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
   Global Instance agree_map_proper: Proper ((≡)==>(≡)) agree_map := ne_proper _.
-  Global Instance agree_map_preserving : CMRAPreserving agree_map.
+  Global Instance agree_map_monotone : CMRAMonotone agree_map.
   Proof.
     split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
-    intros x y; unfold included, agree_included; intros Hy; rewrite Hy.
-    split; [split|done].
-    * by intros (?&?&Hxy); repeat (intro || split);
-        try apply Hxy; try apply Hf; eauto using @agree_valid_le.
-    * by intros (?&(?&?&Hxy)&_); repeat split;
-        try apply Hxy; eauto using agree_valid_le.
+    intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
+    split; [split; simpl; try tauto|done].
+    by intros (?&?&Hxy); repeat split; intros;
+       try apply Hxy; try apply Hf; eauto using @agree_valid_le.
   Qed.
 End agree_map.
 Lemma agree_map_id `{Cofe A} (x : agree A) : agree_map id x = x.
diff --git a/iris/auth.v b/iris/auth.v
index d204f361f..23cfd6d98 100644
--- a/iris/auth.v
+++ b/iris/auth.v
@@ -1,27 +1,30 @@
 Require Export iris.excl.
 Local Arguments disjoint _ _ !_ !_ /.
-Local Arguments included _ _ !_ !_ /.
 
-Record auth (A : Type) : Type := Auth { authorative : excl A ; own : A }.
+Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
 Arguments Auth {_} _ _.
-Arguments authorative {_} _.
+Arguments authoritative {_} _.
 Arguments own {_} _.
 Notation "∘ x" := (Auth ExclUnit x) (at level 20).
 Notation "∙ x" := (Auth (Excl x) ∅) (at level 20).
 
 Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
-Instance auth_valid `{Valid A, Included A} : Valid (auth A) := λ x,
-  valid (authorative x) ∧ excl_above (own x) (authorative x).
+Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
+  valid (authoritative x) ∧ excl_above (own x) (authoritative x).
 Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
-  authorative x ≡ authorative y ∧ own x ≡ own y.
+  authoritative x ≡ authoritative y ∧ own x ≡ own y.
 Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
-  Auth (unit (authorative x)) (unit (own x)).
+  Auth (unit (authoritative x)) (unit (own x)).
 Instance auth_op `{Op A} : Op (auth A) := λ x y,
-  Auth (authorative x â‹… authorative y) (own x â‹… own y).
+  Auth (authoritative x â‹… authoritative y) (own x â‹… own y).
 Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
-  Auth (authorative x ⩪ authorative y) (own x ⩪ own y).
-Instance auth_included `{Equiv A, Included A} : Included (auth A) := λ x y,
-  authorative x ≼ authorative y ∧ own x ≼ own y.
+  Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y).
+Lemma auth_included `{Equiv A, Op A} (x y : auth A) :
+  x ≼ y ↔ authoritative x ≼ authoritative y ∧ own x ≼ own y.
+Proof.
+  split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
+  intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
+Qed.
 
 Instance auth_ra `{RA A} : RA (auth A).
 Proof.
@@ -35,19 +38,19 @@ Proof.
   * by intros y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
   * by intros x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
       split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
-  * by intros x y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
   * by split; simpl; rewrite (associative _).
   * by split; simpl; rewrite (commutative _).
   * by split; simpl; rewrite ?(ra_unit_l _).
   * by split; simpl; rewrite ?(ra_unit_idempotent _).
-  * split; simpl; auto using ra_unit_weaken.
-  * intros ?? [??]; split; [by apply ra_valid_op_l with (authorative y)|].
+  * intros ??; rewrite! auth_included; intros [??].
+    by split; simpl; apply ra_unit_preserving.
+  * intros ?? [??]; split; [by apply ra_valid_op_l with (authoritative y)|].
     by apply excl_above_weaken with (own x â‹… own y)
-      (authorative x â‹… authorative y); try apply ra_included_l.
-  * split; simpl; apply ra_included_l.
-  * by intros ?? [??]; split; simpl; apply ra_op_minus.
+      (authoritative x â‹… authoritative y); try apply ra_included_l.
+  * by intros ??; rewrite auth_included;
+      intros [??]; split; simpl; apply ra_op_minus.
 Qed.
 Instance auth_ra_empty `{RA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
 Proof. split. done. by intros x; constructor; simpl; rewrite (left_id _ _). Qed.
 Lemma auth_frag_op `{RA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b.
-Proof. done. Qed.
+Proof. done. Qed.
\ No newline at end of file
diff --git a/iris/cmra.v b/iris/cmra.v
index e4c5589ae..7b3a9d8b8 100644
--- a/iris/cmra.v
+++ b/iris/cmra.v
@@ -3,15 +3,18 @@ Require Export iris.ra iris.cofe.
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
 
-Class CMRA A `{Equiv A, Compl A,
-    Unit A, Op A, Valid A, ValidN A, Included A, Minus A} : Prop := {
+Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅ z.
+Notation "x ≼{ n } y" := (includedN n x y)
+  (at level 70, format "x  ≼{ n }  y") : C_scope.
+Instance: Params (@includedN) 4.
+
+Class CMRA A `{Equiv A, Compl A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
   (* setoids *)
   cmra_cofe :> Cofe A;
   cmra_op_ne n x :> Proper (dist n ==> dist n) (op x);
   cmra_unit_ne n :> Proper (dist n ==> dist n) unit;
   cmra_valid_ne n :> Proper (dist n ==> impl) (validN n);
   cmra_minus_ne n :> Proper (dist n ==> dist n ==> dist n) minus;
-  cmra_included_proper x : Proper ((≡) ==> impl) (included x);
   (* valid *)
   cmra_valid_0 x : validN 0 x;
   cmra_valid_S n x : validN (S n) x → validN n x;
@@ -21,18 +24,17 @@ Class CMRA A `{Equiv A, Compl A,
   cmra_commutative : Commutative (≡) (⋅);
   cmra_unit_l x : unit x ⋅ x ≡ x;
   cmra_unit_idempotent x : unit (unit x) ≡ unit x;
-  cmra_unit_weaken x y : unit x ≼ unit (x ⋅ y);
+  cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y;
   cmra_valid_op_l n x y : validN n (x ⋅ y) → validN n x;
-  cmra_included_l x y : x ≼ x ⋅ y;
-  cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+  cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y
 }.
 Class CMRAExtend A `{Equiv A, Dist A, Op A, ValidN A} :=
-  cmra_extend_op x y1 y2 n :
+  cmra_extend_op n x y1 y2 :
     validN n x → x ={n}= y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z ={n}= (y1,y2) }.
 
-Class CMRAPreserving
-    `{Included A, ValidN A, Included B, ValidN B} (f : A → B) := {
-  included_preserving x y : x ≼ y → f x ≼ f y;
+Class CMRAMonotone
+    `{Dist A, Op A, ValidN A, Dist B, Op B, ValidN B} (f : A → B) := {
+  includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
   validN_preserving n x : validN n x → validN n (f x)
 }.
 
@@ -46,12 +48,11 @@ Structure cmraT := CMRAT {
   cmra_op : Op cmra_car;
   cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
-  cmra_included : Included cmra_car;
   cmra_minus : Minus cmra_car;
   cmra_cmra : CMRA cmra_car;
   cmra_extend : CMRAExtend cmra_car
 }.
-Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _ _}.
+Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _}.
 Arguments cmra_car _ : simpl never.
 Arguments cmra_equiv _ _ _ : simpl never.
 Arguments cmra_dist _ _ _ _ : simpl never.
@@ -60,12 +61,11 @@ Arguments cmra_unit _ _ : simpl never.
 Arguments cmra_op _ _ _ : simpl never.
 Arguments cmra_valid _ _ : simpl never.
 Arguments cmra_validN _ _ _ : simpl never.
-Arguments cmra_included _ _ _ : simpl never.
 Arguments cmra_minus _ _ _ : simpl never.
 Arguments cmra_cmra _ : simpl never.
 Add Printing Constructor cmraT.
 Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op
-  cmra_valid cmra_validN cmra_included cmra_minus cmra_cmra cmra_extend.
+  cmra_valid cmra_validN cmra_minus cmra_cmra cmra_extend.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A.
 Canonical Structure cmra_cofeC.
 
@@ -73,6 +73,13 @@ Section cmra.
 Context `{cmra : CMRA A}.
 Implicit Types x y z : A.
 
+Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y.
+Proof.
+  split; [by intros [z Hz] n; exists z; rewrite Hz|].
+  intros Hxy; exists (y ⩪ x); apply equiv_dist; intros n.
+  symmetry; apply cmra_op_minus, Hxy.
+Qed.
+
 Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (validN n).
 Proof. by split; apply cmra_valid_ne. Qed.
 Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (validN n).
@@ -82,16 +89,15 @@ Proof.
   split; try by (destruct cmra;
     eauto using ne_proper, ne_proper_2 with typeclass_instances).
   * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite <-Hx.
+  * intros x y; rewrite !cmra_included_includedN.
+    eauto using cmra_unit_preserving.
   * intros x y; rewrite !cmra_valid_validN; intros ? n.
     by apply cmra_valid_op_l with y.
+  * intros x y [z Hz]; apply equiv_dist; intros n.
+    by apply cmra_op_minus; exists z; rewrite Hz.
 Qed.
 Lemma cmra_valid_op_r x y n : validN n (x ⋅ y) → validN n y.
 Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed.
-Lemma cmra_valid_included x y n : validN n y → x ≼ y → validN n x.
-Proof.
-  rewrite ra_included_spec; intros Hvalid [z Hy]; rewrite Hy in Hvalid.
-  eauto using cmra_valid_op_l.
-Qed.
 Lemma cmra_valid_le x n n' : validN n x → n' ≤ n → validN n' x.
 Proof. induction 2; eauto using cmra_valid_S. Qed.
 Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (â‹…).
@@ -101,24 +107,66 @@ Proof.
 Qed.
 Lemma cmra_unit_valid x n : validN n x → validN n (unit x).
 Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
-Lemma cmra_included_dist_l x1 x2 x1' n :
-  x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
-Proof.
-  rewrite ra_included_spec; intros [z Hx2] Hx1; exists (x1' â‹… z); split.
-  apply ra_included_l. by rewrite Hx1, Hx2.
-Qed.
 Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
   validN 1 (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
 Proof.
   intros ??? z Hz.
-  destruct (cmra_extend_op z x1 x2 1) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
+  destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
   { by rewrite <-?Hz. }
   by rewrite Hz', (timeless x1 y1), (timeless x2 y2).
 Qed.
+
+(** * Included *)
+Global Instance cmra_included_ne n :
+  Proper (dist n ==> dist n ==> iff) (includedN n).
+Proof.
+  intros x x' Hx y y' Hy; unfold includedN.
+  by setoid_rewrite Hx; setoid_rewrite Hy.
+Qed.
+Global Instance cmra_included_proper:Proper ((≡) ==> (≡) ==> iff) (includedN n).
+Proof.
+  intros n x x' Hx y y' Hy; unfold includedN.
+  by setoid_rewrite Hx; setoid_rewrite Hy.
+Qed.
+Lemma cmra_included_0 x y : x ≼{0} y.
+Proof. by exists (unit x). Qed.
+Lemma cmra_included_S x y n : x ≼{S n} y → x ≼{n} y.
+Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
+
+Lemma cmra_included_l n x y : x ≼{n} x ⋅ y.
+Proof. by exists y. Qed.
+Lemma cmra_included_r n x y : y ≼{n} x ⋅ y.
+Proof. rewrite (commutative op); apply cmra_included_l. Qed.
+Global Instance cmra_included_ord n : PreOrder (includedN n).
+Proof.
+  split.
+  * by intros x; exists (unit x); rewrite ra_unit_r.
+  * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
+    by rewrite (associative _), <-Hy, <-Hz.
+Qed.
+Lemma cmra_valid_includedN x y n : validN n y → x ≼{n} y → validN n x.
+Proof. intros Hyv [z Hy]; rewrite Hy in Hyv; eauto using cmra_valid_op_l. Qed.
+Lemma cmra_valid_included x y n : validN n y → x ≼ y → validN n x.
+Proof. rewrite cmra_included_includedN; eauto using cmra_valid_includedN. Qed.
+Lemma cmra_included_dist_l x1 x2 x1' n :
+  x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
+Proof.
+  intros [z Hx2] Hx1; exists (x1' â‹… z); split; auto using ra_included_l.
+  by rewrite Hx1, Hx2.
+Qed.
 End cmra.
 
-Instance cmra_preserving_id `{CMRA A} : CMRAPreserving (@id A).
+Instance cmra_monotone_id `{CMRA A} : CMRAMonotone (@id A).
 Proof. by split. Qed.
+Instance cmra_monotone_ra_monotone `{CMRA A, CMRA B} (f : A → B) :
+  CMRAMonotone f → RAMonotone f.
+Proof.
+  split.
+  * intros x y; rewrite !cmra_included_includedN.
+    by intros ? n; apply includedN_preserving.
+  * intros x; rewrite !cmra_valid_validN.
+    by intros ? n; apply validN_preserving.
+Qed.
 
 (* Also via [cmra_cofe; cofe_equivalence] *)
 Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
@@ -139,15 +187,18 @@ Section discrete.
     * by intros [|n]; try apply ra_minus_proper.
     * by intros [|n].
     * intros x; split; intros Hvalid. by intros [|n]. apply (Hvalid 1).
+    * by intros [|n]; try apply ra_unit_preserving.
     * by intros [|n]; try apply ra_valid_op_l.
+    * by intros [|n] x y; try apply ra_op_minus.
   Qed.
   Instance discrete_extend : CMRAExtend A.
   Proof.
-    intros x y1 y2 [|n] ??; [|by exists (y1,y2)].
+    intros [|n] x y1 y2 ??; [|by exists (y1,y2)].
     by exists (x,unit x); simpl; rewrite ra_unit_r.
   Qed.
-  Definition discreteC : cmraT := CMRAT A.
+  Definition discreteRA : cmraT := CMRAT A.
 End discrete.
+Arguments discreteRA _ {_ _ _ _ _ _}.
 
 (** Product *)
 Instance prod_op `{Op A, Op B} : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
@@ -158,11 +209,20 @@ Instance prod_valid `{Valid A, Valid B} : Valid (A * B) := λ x,
   valid (x.1) ∧ valid (x.2).
 Instance prod_validN `{ValidN A, ValidN B} : ValidN (A * B) := λ n x,
   validN n (x.1) ∧ validN n (x.2).
-Instance prod_included `{Included A, Included B} : Included (A * B) :=
-  prod_relation (≼) (≼).
 Instance prod_minus `{Minus A, Minus B} : Minus (A * B) := λ x y,
   (x.1 ⩪ y.1, x.2 ⩪ y.2).
-
+Lemma prod_included `{Equiv A, Equiv B, Op A, Op B} (x y : A * B) :
+  x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
+Proof.
+  split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
+  intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
+Qed.
+Lemma prod_includedN `{Dist A, Dist B, Op A, Op B} (x y : A * B) n :
+  x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2.
+Proof.
+  split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
+  intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
+Qed.
 Instance prod_cmra `{CMRA A, CMRA B} : CMRA (A * B).
 Proof.
   split; try apply _.
@@ -171,7 +231,6 @@ Proof.
   * by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite <-?Hy1, <-?Hy2.
   * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
       split; simpl in *; rewrite ?Hx1, ?Hx2, ?Hy1, ?Hy2.
-  * by intros x y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite <-?Hy1, <-?Hy2.
   * split; apply cmra_valid_0.
   * by intros n x [??]; split; apply cmra_valid_S.
   * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
@@ -180,10 +239,11 @@ Proof.
   * split; simpl; apply (commutative _).
   * split; simpl; apply ra_unit_l.
   * split; simpl; apply ra_unit_idempotent.
-  * split; apply ra_unit_weaken.
+  * intros n x y; rewrite !prod_includedN.
+    by intros [??]; split; apply cmra_unit_preserving.
   * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto.
-  * split; apply cmra_included_l.
-  * by intros x y [??]; split; apply cmra_op_minus.
+  * intros x y n; rewrite prod_includedN; intros [??].
+    by split; apply cmra_op_minus.
 Qed.
 Instance prod_ra_empty `{RAEmpty A, RAEmpty B} : RAEmpty (A * B).
 Proof.
@@ -191,18 +251,19 @@ Proof.
 Qed.
 Instance prod_cmra_extend `{CMRAExtend A, CMRAExtend B} : CMRAExtend (A * B).
 Proof.
-  intros x y1 y2 n [??] [??]; simpl in *.
-  destruct (cmra_extend_op (x.1) (y1.1) (y2.1) n) as (z1&?&?&?); auto.
-  destruct (cmra_extend_op (x.2) (y1.2) (y2.2) n) as (z2&?&?&?); auto.
+  intros n x y1 y2 [??] [??]; simpl in *.
+  destruct (cmra_extend_op n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
+  destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
   by exists ((z1.1,z2.1),(z1.2,z2.2)).
 Qed.
 Canonical Structure prodRA (A B : cmraT) : cmraT := CMRAT (A * B).
-Instance prod_map_cmra_preserving `{CMRA A, CMRA A', CMRA B, CMRA B'}
-  (f : A → A') (g : B → B') `{!CMRAPreserving f, !CMRAPreserving g} :
-  CMRAPreserving (prod_map f g).
+Instance prod_map_cmra_monotone `{CMRA A, CMRA A', CMRA B, CMRA B'}
+  (f : A → A') (g : B → B') `{!CMRAMonotone f, !CMRAMonotone g} :
+  CMRAMonotone (prod_map f g).
 Proof.
   split.
-  * by intros x1 x2 [??]; split; simpl; apply included_preserving.
+  * intros n x1 x2; rewrite !prod_includedN; intros [??]; simpl.
+    by split; apply includedN_preserving.
   * by intros n x [??]; split; simpl; apply validN_preserving.
 Qed.
 Definition prodRA_map {A A' B B' : cmraT}
diff --git a/iris/cmra_maps.v b/iris/cmra_maps.v
index 68591bece..d4a20f725 100644
--- a/iris/cmra_maps.v
+++ b/iris/cmra_maps.v
@@ -3,18 +3,28 @@ Require Import prelude.pmap prelude.nmap prelude.zmap.
 Require Import prelude.stringmap prelude.natmap.
 
 (** option *)
-Instance option_valid `{Valid A} : Valid (option A) := λ x,
-  match x with Some x => valid x | None => True end.
-Instance option_validN `{ValidN A} : ValidN (option A) := λ n x,
-  match x with Some x => validN n x | None => True end.
+Instance option_valid `{Valid A} : Valid (option A) := λ mx,
+  match mx with Some x => valid x | None => True end.
+Instance option_validN `{ValidN A} : ValidN (option A) := λ n mx,
+  match mx with Some x => validN n x | None => True end.
 Instance option_unit `{Unit A} : Unit (option A) := fmap unit.
 Instance option_op `{Op A} : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_minus `{Minus A} : Minus (option A) :=
   difference_with (λ x y, Some (x ⩪ y)).
-Inductive option_included `{Included A} : Included (option A) :=
-  | Some_included x y : x ≼ y → Some x ≼ Some y
-  | None_included x : None ≼ x.
-Existing Instance option_included.
+Lemma option_includedN `{CMRA A} n mx my :
+  mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
+Proof.
+  split.
+  * intros [mz Hmz]; destruct n as [|n]; [by left|right].
+    destruct mx as [x|]; [right|by left].
+    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
+    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto.
+    + by exists z.
+    + by cofe_subst.
+  * intros [->|[->|(x&y&->&->&z&Hz)]];
+      try (by exists my; destruct my; constructor).
+    by exists (Some z); constructor.
+Qed.
 Instance option_cmra `{CMRA A} : CMRA (option A).
 Proof.
   split.
@@ -27,8 +37,6 @@ Proof.
      eapply (_ : Proper (dist _ ==> impl) (validN _)); eauto.
   * by destruct 1; inversion_clear 1; constructor;
       repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
-  * intros [x|]; destruct 1; inversion_clear 1; constructor;
-      eapply (_ : Proper (equiv ==> impl) (included _)); eauto.
   * intros [x|]; unfold validN, option_validN; auto using cmra_valid_0.
   * intros n [x|]; unfold validN, option_validN; auto using cmra_valid_S.
   * by intros [x|]; unfold valid, validN, option_validN, option_valid;
@@ -37,19 +45,21 @@ Proof.
   * intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto.
   * by intros [x|]; constructor; rewrite cmra_unit_l.
   * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
-  * intros [x|] [y|]; constructor; auto using cmra_unit_weaken.
+  * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
+    do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preserving.
   * intros n [x|] [y|]; unfold validN, option_validN; simpl;
       eauto using cmra_valid_op_l.
-  * intros [x|] [y|]; constructor; auto using cmra_included_l.
-  * destruct 1 as [|[]]; constructor; eauto using cmra_op_minus.
+  * intros n mx my; rewrite option_includedN.
+    intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
+    by constructor; apply cmra_op_minus.
 Qed.
 Instance option_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (option A).
 Proof.
-  intros mx my1 my2 n; destruct (decide (n = 0)) as [->|].
+  intros n mx my1 my2; destruct (decide (n = 0)) as [->|].
   { by exists (mx, None); repeat constructor; destruct mx; constructor. }
   destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
     try (by exfalso; inversion Hx'; auto).
-  * destruct (cmra_extend_op x y1 y2 n) as ([z1 z2]&?&?&?); auto.
+  * destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
     { by inversion_clear Hx'. }
     by exists (Some z1, Some z2); repeat constructor.
   * by exists (Some x,None); inversion Hx'; repeat constructor.
@@ -57,10 +67,11 @@ Proof.
   * exists (None,None); repeat constructor.
 Qed.
 Instance option_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A → B)
-  `{!CMRAPreserving f} : CMRAPreserving (fmap f : option A → option B).
+  `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B).
 Proof.
   split.
-  * by destruct 1 as [|[?|]]; constructor; apply included_preserving.
+  * intros n mx my; rewrite !option_includedN.
+    intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
   * by intros n [x|] ?;
       unfold validN, option_validN; simpl; try apply validN_preserving.
 Qed.
@@ -74,14 +85,28 @@ Section map.
   Instance map_valid `{Valid A} : Valid (M A) := λ m, ∀ i, valid (m !! i).
   Instance map_validN `{ValidN A} : ValidN (M A) := λ n m, ∀ i, validN n (m!!i).
   Instance map_minus `{Minus A} : Minus (M A) := merge minus.
-  Instance map_included `{Included A} : Included (M A) := λ m1 m2,
-    ∀ i, m1 !! i ≼ m2 !! i.
   Lemma lookup_op `{Op A} m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
   Proof. by apply lookup_merge. Qed.
   Lemma lookup_minus `{Minus A} m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
   Proof. by apply lookup_merge. Qed.
   Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i).
   Proof. by apply lookup_fmap. Qed.
+  Lemma map_included_spec `{CMRA A} (m1 m2 : M A) :
+    m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
+  Proof.
+    split.
+    * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
+    * intros Hm; exists (m2 ⩪ m1); intros i.
+      by rewrite lookup_op, lookup_minus, ra_op_minus.
+  Qed.
+  Lemma map_includedN_spec `{CMRA A} (m1 m2 : M A) n :
+    m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
+  Proof.
+    split.
+    * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
+    * intros Hm; exists (m2 ⩪ m1); intros i.
+      by rewrite lookup_op, lookup_minus, cmra_op_minus.
+  Qed.
   Instance map_cmra `{CMRA A} : CMRA (M A).
   Proof.
     split.
@@ -91,7 +116,6 @@ Section map.
     * by intros n m1 m2 Hm ? i; rewrite <-(Hm i).
     * intros n m1 m1' Hm1 m2 m2' Hm2 i.
       by rewrite !lookup_minus, (Hm1 i), (Hm2 i).
-    * by intros m1 m2 m2' Hm2 ? i; rewrite <-(Hm2 i).
     * intros m i; apply cmra_valid_0.
     * intros n m Hm i; apply cmra_valid_S, Hm.
     * intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
@@ -100,11 +124,12 @@ Section map.
     * by intros m1 m2 i; rewrite !lookup_op, (commutative _).
     * by intros m i; rewrite lookup_op, !lookup_unit, ra_unit_l.
     * by intros m i; rewrite !lookup_unit, ra_unit_idempotent.
-    * intros m1 m2 i; rewrite !lookup_unit, lookup_op; apply ra_unit_weaken.
+    * intros n x y; rewrite !map_includedN_spec; intros Hm i.
+      by rewrite !lookup_unit; apply cmra_unit_preserving.
     * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
       by rewrite <-lookup_op.
-    * intros m1 m2 i; rewrite lookup_op; apply ra_included_l.
-    * by intros m1 m2 Hm i; rewrite lookup_op, lookup_minus, ra_op_minus.
+    * intros x y n; rewrite map_includedN_spec; intros ? i.
+      by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
   Qed.
   Instance map_ra_empty `{RA A} : RAEmpty (M A).
   Proof.
@@ -114,10 +139,10 @@ Section map.
   Qed.
   Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (M A).
   Proof.
-    intros m m1 m2 n Hm Hm12.
+    intros n m m1 m2 Hm Hm12.
     assert (∀ i, m !! i ={n}= m1 !! i ⋅ m2 !! i) as Hm12'
       by (by intros i; rewrite <-lookup_op).
-    set (f i := cmra_extend_op (m !! i) (m1 !! i) (m2 !! i) n (Hm i) (Hm12' i)).
+    set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
     set (f_proj i := proj1_sig (f i)).
     exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
       repeat split; simpl; intros i; rewrite ?lookup_op, !lookup_imap.
@@ -131,11 +156,12 @@ Section map.
       by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
   Qed.
   Definition mapRA (A : cmraT) : cmraT := CMRAT (M A).
-  Global Instance map_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A → B)
-    `{!CMRAPreserving f} : CMRAPreserving (fmap f : M A → M B).
+  Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
+    `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A → M B).
   Proof.
     split.
-    * by intros m1 m2 Hm i; rewrite !lookup_fmap; apply included_preserving.
+    * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
+      by rewrite !lookup_fmap; apply includedN_preserving.
     * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
   Qed.
   Hint Resolve (map_fmap_ne (M:=M)) : typeclass_instances.
@@ -143,8 +169,8 @@ Section map.
     CofeMor (fmap f : mapRA A → mapRA B).
   Global Instance mapRA_map_ne {A B} n :
     Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n.
-  Global Instance mapRA_mapcmra_preserving {A B : cmraT} (f : A -n> B)
-    `{!CMRAPreserving f} : CMRAPreserving (mapRA_map f) := _.
+  Global Instance mapRA_mapcmra_monotone {A B : cmraT} (f : A -n> B)
+    `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
 End map.
 
 Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _.
diff --git a/iris/dra.v b/iris/dra.v
index b7f573f0c..aa3e707d8 100644
--- a/iris/dra.v
+++ b/iris/dra.v
@@ -30,14 +30,19 @@ Instance validity_valid_proper `{Equiv A} (P : A → Prop) :
 Proof. intros ?? [??]; naive_solver. Qed.
 
 Local Notation V := valid.
-Class DRA A `{Equiv A,Valid A,Unit A,Disjoint A,Op A,Included A, Minus A} := {
+
+Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
+  ∃ z, y ≡ x ⋅ z ∧ V z ∧ x ⊥ z.
+Instance: Params (@dra_included) 4.
+Local Infix "≼" := dra_included.
+
+Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
   (* setoids *)
   dra_equivalence :> Equivalence ((≡) : relation A);
   dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
   dra_unit_proper :> Proper ((≡) ==> (≡)) unit;
   dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
   dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
-  dra_included_proper :> Proper ((≡) ==> (≡) ==> impl) included;
   (* validity *)
   dra_op_valid x y : V x → V y → x ⊥ y → V (x ⋅ y);
   dra_unit_valid x : V x → V (unit x);
@@ -51,20 +56,21 @@ Class DRA A `{Equiv A,Valid A,Unit A,Disjoint A,Op A,Included A, Minus A} := {
   dra_unit_disjoint_l x : V x → unit x ⊥ x;
   dra_unit_l x : V x → unit x ⋅ x ≡ x;
   dra_unit_idempotent x : V x → unit (unit x) ≡ unit x;
-  dra_unit_weaken x y : V x → V y → x ⊥ y → unit x ≼ unit (x ⋅ y);
-  dra_included_l x y : V x → V y → x ⊥ y → x ≼ x ⋅ y;
-  dra_disjoint_difference x y : V x → V y → x ≼ y → x ⊥ y ⩪ x;
-  dra_op_difference x y : V x → V y → x ≼ y → x ⋅ y ⩪ x ≡ y
+  dra_unit_preserving x y : V x → V y → x ≼ y → unit x ≼ unit y;
+  dra_disjoint_minus x y : V x → V y → x ≼ y → x ⊥ y ⩪ x;
+  dra_op_minus x y : V x → V y → x ≼ y → x ⋅ y ⩪ x ≡ y
 }.
 
 Section dra.
 Context A `{DRA A}.
 Arguments valid _ _ !_ /.
+Hint Immediate dra_op_proper : typeclass_instances.
 
-Instance: Proper ((≡) ==> (≡) ==> impl) (⊥).
+Instance: Proper ((≡) ==> (≡) ==> iff) (⊥).
 Proof.
-  intros x1 x2 Hx y1 y2 Hy.
-  by rewrite Hy, (symmetry_iff (⊥) x1), (symmetry_iff (⊥) x2), Hx.
+  intros x1 x2 Hx y1 y2 Hy; split.
+  * by rewrite Hy, (symmetry_iff (⊥) x1), (symmetry_iff (⊥) x2), Hx.
+  * by rewrite <-Hy, (symmetry_iff (⊥) x2), (symmetry_iff (⊥) x1), <-Hx.
 Qed.
 Lemma dra_disjoint_rl x y z : V x → V y → V z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y.
 Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
@@ -78,10 +84,8 @@ Proof.
   intros; symmetry; rewrite dra_commutative by eauto using dra_disjoint_rl.
   apply dra_disjoint_move_l; auto; by rewrite dra_commutative.
 Qed.
-Hint Immediate dra_associative dra_commutative dra_unit_disjoint_l
-  dra_unit_l dra_unit_idempotent dra_unit_weaken dra_included_l
-  dra_op_difference dra_disjoint_difference dra_disjoint_rl
-  dra_disjoint_lr dra_disjoint_move_l dra_disjoint_move_r.
+Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
+Hint Unfold dra_included.
 
 Notation T := (validity (valid : A → Prop)).
 Program Instance validity_unit : Unit T := λ x,
@@ -91,8 +95,6 @@ Program Instance validity_op : Op T := λ x y,
   Validity (validity_car x â‹… validity_car y)
            (V x ∧ V y ∧ validity_car x ⊥ validity_car y) _.
 Next Obligation. by apply dra_op_valid; try apply validity_prf. Qed.
-Instance validity_included : Included T := λ x y,
-  V y → V x ∧ validity_car x ≼ validity_car y.
 Program Instance validity_minus : Minus T := λ x y,
   Validity (validity_car x ⩪ validity_car y)
            (V x ∧ V y ∧ validity_car y ≼ validity_car x) _.
@@ -108,21 +110,25 @@ Proof.
   * by intros ?? Heq ?; rewrite <-Heq.
   * intros x1 x2 [? Hx] y1 y2 [? Hy];
       split; simpl; [|by intros (?&?&?); rewrite Hx, Hy].
-    split; intros (?&?&?); split_ands'; try tauto.
-    + by rewrite <-Hx, <-Hy by done.
-    + by rewrite Hx, Hy by tauto.
-  * intros ??? [? Heq] Hle; split; [apply Hle; tauto|].
-    rewrite <-Heq by tauto; apply Hle; tauto.
-  * intros [x px ?] [y py ?] [z pz ?];
-      split; simpl; [naive_solver|intros; apply (associative _)].
-  * intros [x px ?] [y py ?]; split; naive_solver.
-  * intros [x px ?]; split; naive_solver.
-  * intros [x px ?]; split; naive_solver.
-  * intros [x px ?] [y py ?]; split; naive_solver.
+    split; intros (?&?&z&?&?); split_ands'; try tauto.
+    + exists z. by rewrite <-Hy, <-Hx.
+    + exists z. by rewrite Hx, Hy by tauto.
+  * intros [x px ?] [y py ?] [z pz ?]; split; simpl;
+      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
+      |intros; apply (associative _)].
+  * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative.
+  * intros [x px ?]; split;
+      naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
+  * intros [x px ?]; split; naive_solver eauto using dra_unit_idempotent.
+  * intros x y Hxy; exists (unit y ⩪ unit x).
+    destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
+    assert (py → unit x ≼ unit y)
+      by intuition eauto 10 using dra_unit_preserving.
+    constructor; [|symmetry]; simpl in *;
+      intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid.
   * by intros [x px ?] [y py ?] (?&?&?).
-  * intros [x px ?] [y py ?]; split; naive_solver.
-  * intros [x px ?] [y py ?];
-      unfold included, validity_included; split; naive_solver.
+  * intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
+      intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
 Qed.
 Definition dra_update (x y : T) :
   (∀ z, V x → V z → validity_car x ⊥ z → V y ∧ validity_car y ⊥ z) → x ⇝ y.
diff --git a/iris/excl.v b/iris/excl.v
index 698fc40a7..7f4edafd2 100644
--- a/iris/excl.v
+++ b/iris/excl.v
@@ -1,6 +1,5 @@
 Require Export iris.cmra.
 Local Arguments disjoint _ _ !_ !_ /.
-Local Arguments included _ _ !_ !_ /.
 
 Inductive excl (A : Type) :=
   | Excl : A → excl A
@@ -32,15 +31,6 @@ Instance excl_minus {A} : Minus (excl A) := λ x y,
   | Excl _, Excl _ => ExclUnit
   | _, _ => ExclBot
   end.
-Instance excl_included `{Equiv A} : Included (excl A) := λ x y,
-  match x, y with
-  | Excl x, Excl y => x ≡ y
-  | ExclUnit, _ => True
-  | _, ExclBot => True
-  | _, _ => False
-  end.
-Definition excl_above `{Included A} (x : A) (y : excl A) : Prop :=
-  match y with Excl y' => x ≼ y' | ExclUnit => True | ExclBot => False end.
 Instance excl_ra `{Equiv A, !Equivalence (@equiv A _)} : RA (excl A).
 Proof.
   split.
@@ -52,21 +42,23 @@ Proof.
   * constructor.
   * by destruct 1.
   * by do 2 destruct 1; constructor.
-  * by intros []; destruct 1; simpl; try (intros Hx; rewrite Hx).
   * by intros [?| |] [?| |] [?| |]; constructor.
   * by intros [?| |] [?| |]; constructor.
   * by intros [?| |]; constructor.
   * constructor.
+  * intros [?| |] [?| |]; exists ∅; constructor.
   * by intros [?| |] [?| |].
-  * by intros [?| |] [?| |].
-  * by intros [?| |] [?| |]; simpl; try constructor.
-  * by intros [?| |] [?| |] ?; try constructor.
+  * by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
 Qed.
 Instance excl_empty_ra `{Equiv A, !Equivalence (@equiv A _)} : RAEmpty (excl A).
 Proof. split. done. by intros []. Qed.
 Lemma excl_update {A} (x : A) y : valid y → Excl x ⇝ y.
 Proof. by destruct y; intros ? [?| |]. Qed.
 
+Definition excl_above `{Equiv A, Op A} (x : A) (y : excl A) : Prop :=
+  match y with Excl y' => x ≼ y' | ExclUnit => True | ExclBot => False end.
+Instance: Params (@excl_above) 3.
+
 Section excl_above.
   Context `{RA A}.
   Global Instance excl_above_proper : Proper ((≡) ==> (≡) ==> iff) excl_above.
@@ -74,7 +66,8 @@ Section excl_above.
   Lemma excl_above_weaken (a b : A) x y :
     excl_above b y → a ≼ b → x ≼ y → excl_above a x.
   Proof.
-    destruct x as [a'| |], y as [b'| |]; simpl; intros ??; try done.
-    by intros Hab; rewrite Hab; transitivity b.
+    destruct x as [a'| |], y as [b'| |];
+      intros ?? [[] Hz]; inversion_clear Hz; simpl in *; try done.
+    by setoid_subst; transitivity b.
   Qed.
 End excl_above.
diff --git a/iris/language.v b/iris/language.v
new file mode 100644
index 000000000..c9d26dc74
--- /dev/null
+++ b/iris/language.v
@@ -0,0 +1,31 @@
+Require Import prelude.prelude.
+
+Class language (E V S : Type) := Language {
+  to_expr : V → E;
+  of_expr : E → option V;
+  atomic : E → Prop;
+  prim_step : (E * S) → (E * S) → option E → Prop;
+  of_to_expr v : of_expr (to_expr v) = Some v;
+  to_of_expr e v : of_expr e = Some v → to_expr v = e;
+  values_stuck e σ s' ef : prim_step (e,σ) s' ef → of_expr e = None;
+  atomic_not_value e : atomic e → of_expr e = None;
+  atomic_step e1 σ1 e2 σ2 ef :
+    atomic e1 →
+    prim_step (e1,σ1) (e2,σ2) ef →
+    is_Some (of_expr e2)
+}.
+
+Section foo.
+  Context `{language E V St}.
+
+  Definition cfg : Type := (list E * St)%type.
+  Inductive step (ρ1 ρ2 : cfg) : Prop :=
+    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
+       ρ1 = (t1 ++ e1 :: t2, σ1) →
+       ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
+       prim_step (e1, σ1) (e2, σ2) ef →
+       step ρ1 ρ2.
+
+  Definition steps := rtc step.
+  Definition stepn := nsteps step.
+End foo.
\ No newline at end of file
diff --git a/iris/logic.v b/iris/logic.v
index d3165e625..0e1ff71a0 100644
--- a/iris/logic.v
+++ b/iris/logic.v
@@ -48,7 +48,7 @@ Canonical Structure uPredC (M : cmraT) : cofeT := CofeT (uPred M).
 
 (** functor *)
 Program Definition uPred_map {M1 M2 : cmraT} (f : M2 → M1)
-  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAPreserving f}
+  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f}
   (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
 Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
 Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed.
@@ -56,15 +56,15 @@ Next Obligation.
   naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
 Qed.
 Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 → M1)
-  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAPreserving f} :
+  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f} :
   Proper (dist n ==> dist n) (uPred_map f).
 Proof.
   by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
 Qed.
-Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAPreserving f} :
+Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
   uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
 Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
-    `{!CMRAPreserving f, !CMRAPreserving g} n :
+    `{!CMRAMonotone f, !CMRAMonotone g} n :
   f ={n}= g → uPredC_map f ={n}= uPredC_map g.
 Proof.
   by intros Hfg P y n' ??; simpl; rewrite (dist_le _ _ _ _(Hfg y)) by lia.
@@ -125,8 +125,7 @@ Next Obligation. by intros M P Q x; exists x, x. Qed.
 Next Obligation.
   intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ? Hvalid.
   assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
-  { rewrite ra_included_spec in Hxy; destruct Hxy as [z Hy].
-    exists (x2 â‹… z); split; eauto using ra_included_l.
+  { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using ra_included_l.
     apply dist_le with n1; auto. by rewrite (associative op), <-Hx, Hy. }
   rewrite Hy in Hvalid; exists x1, x2'; split_ands; auto.
   * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
@@ -165,11 +164,11 @@ Next Obligation.
 Qed.
 
 Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
-  {| uPred_holds n x := ∃ a', x ={n}= a ⋅ a' |}.
-Next Obligation. by intros M a x1 x2 n [a' Hx] ?; exists a'; rewrite <-Hx. Qed.
+  {| uPred_holds n x := a ≼{n} x |}.
+Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite <-Hx. Qed.
 Next Obligation. by intros M a x; exists x. Qed.
 Next Obligation.
-  intros M a x1 x n1 n2; rewrite ra_included_spec; intros [a' Hx1] [x2 Hx] ??.
+  intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
   exists (a' â‹… x2). by rewrite (associative op), <-(dist_le _ _ _ _ Hx1), Hx.
 Qed.
 Program Definition uPred_valid {M : cmraT} (a : M) : uPred M :=
@@ -571,7 +570,7 @@ Lemma uPred_later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
 Proof.
   intros x n ?; split.
   * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
-    destruct (cmra_extend_op x x1 x2 n)
+    destruct (cmra_extend_op n x x1 x2)
       as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
     exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
   * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
@@ -682,10 +681,9 @@ Proof.
 Qed.
 Lemma uPred_own_unit (a : M) : uPred_own (unit a) ≡ (□ uPred_own (unit a))%I.
 Proof.
-  intros x n; split; [intros [a' Hx]|by apply uPred_always_elim].
-  assert (∃ a'', unit (unit a ⋅ a') ≡ unit (unit a) ⋅ a'') as [a'' Ha]
-    by (rewrite <-ra_included_spec; auto using ra_unit_weaken).
-  by exists a''; rewrite Hx, Ha, ra_unit_idempotent.
+  intros x n; split; [intros [a' Hx]|by apply uPred_always_elim]. simpl.
+  rewrite <-(ra_unit_idempotent a), Hx.
+  apply cmra_unit_preserving, cmra_included_l.
 Qed.
 Lemma uPred_own_empty `{Empty M, !RAEmpty M} : True%I ⊆ uPred_own ∅.
 Proof. intros x [|n] ??; [done|]. by  exists x; rewrite (left_id _ _). Qed.
@@ -712,7 +710,7 @@ Global Instance uPred_sep_timeless P Q :
   TimelessP P → TimelessP Q → TimelessP (P ★ Q).
 Proof.
   intros ?? x [|n] Hvalid (x1&x2&Hx12&?&?); [done|].
-  destruct (cmra_extend_op x x1 x2 1) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *.
+  destruct (cmra_extend_op 1 x x1 x2) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *.
   rewrite Hx12 in Hvalid; exists y1, y2; split_ands; [by rewrite Hx| |].
   * apply timelessP; rewrite Hy1; eauto using cmra_valid_op_l.
   * apply timelessP; rewrite Hy2; eauto using cmra_valid_op_r.
@@ -738,7 +736,7 @@ Global Instance uPred_own_timeless (a : M) :
   Timeless a → TimelessP (uPred_own a).
 Proof.
   intros ? x n ? [a' ?].
-  destruct (cmra_extend_op x a a' 1) as ([b b']&Hx&Hb&Hb'); auto; simpl in *.
+  destruct (cmra_extend_op 1 x a a') as ([b b']&Hx&Hb&Hb'); auto; simpl in *.
   by exists b'; rewrite Hx, (timeless a b) by done.
 Qed.
 End logic.
diff --git a/iris/ra.v b/iris/ra.v
index a668bafe1..001ffdb81 100644
--- a/iris/ra.v
+++ b/iris/ra.v
@@ -11,32 +11,30 @@ Instance: Params (@op) 2.
 Infix "â‹…" := op (at level 50, left associativity) : C_scope.
 Notation "(â‹…)" := op (only parsing) : C_scope.
 
-Class Included (A : Type) := included : relation A.
-Instance: Params (@included) 2.
+Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : C_scope.
 Notation "(≼)" := included (only parsing) : C_scope.
 Hint Extern 0 (?x ≼ ?x) => reflexivity.
+Instance: Params (@included) 3.
 
 Class Minus (A : Type) := minus : A → A → A.
 Instance: Params (@minus) 2.
 Infix "⩪" := minus (at level 40) : C_scope.
 
-Class RA A `{Equiv A, Valid A, Unit A, Op A, Included A, Minus A} : Prop := {
+Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := {
   (* setoids *)
   ra_equivalence :> Equivalence ((≡) : relation A);
   ra_op_proper x :> Proper ((≡) ==> (≡)) (op x);
   ra_unit_proper :> Proper ((≡) ==> (≡)) unit;
   ra_valid_proper :> Proper ((≡) ==> impl) valid;
   ra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
-  ra_included_proper x :> Proper ((≡) ==> impl) (included x);
   (* monoid *)
   ra_associative :> Associative (≡) (⋅);
   ra_commutative :> Commutative (≡) (⋅);
   ra_unit_l x : unit x ⋅ x ≡ x;
   ra_unit_idempotent x : unit (unit x) ≡ unit x;
-  ra_unit_weaken x y : unit x ≼ unit (x ⋅ y);
+  ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
   ra_valid_op_l x y : valid (x ⋅ y) → valid x;
-  ra_included_l x y : x ≼ x ⋅ y;
   ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
 }.
 Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
@@ -44,6 +42,12 @@ Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
   ra_empty_l :> LeftId (≡) ∅ (⋅)
 }.
 
+Class RAMonotone
+    `{Equiv A, Op A, Valid A, Equiv B, Op B, Valid B} (f : A → B) := {
+  included_preserving x y : x ≼ y → f x ≼ f y;
+  valid_preserving x : valid x → valid (f x)
+}.
+
 (** Big ops *)
 Fixpoint big_op `{Op A, Empty A} (xs : list A) : A :=
   match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
@@ -87,38 +91,27 @@ Lemma ra_unit_unit x : unit x ⋅ unit x ≡ unit x.
 Proof. by rewrite <-(ra_unit_idempotent x) at 2; rewrite ra_unit_r. Qed.
 
 (** ** Order *)
-Lemma ra_included_spec x y : x ≼ y ↔ ∃ z, y ≡ x ⋅ z.
-Proof.
-  split; [by exists (y ⩪ x); rewrite ra_op_minus|].
-  intros [z Hz]; rewrite Hz; apply ra_included_l.
-Qed.
-Global Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> iff) (≼).
-Proof.
-  intros x1 x2 Hx y1 y2 Hy; rewrite !ra_included_spec.
-  by setoid_rewrite Hx; setoid_rewrite Hy.
-Qed.
+Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> impl) (≼).
+Proof. intros x1 x2 Hx y1 y2 Hy [z Hz]; exists z. by rewrite <-Hy, Hz, Hx. Qed.
+Global Instance ra_included_proper : Proper ((≡) ==> (≡) ==> iff) (≼).
+Proof. by split; apply ra_included_proper'. Qed.
+Lemma ra_included_l x y : x ≼ x ⋅ y.
+Proof. by exists y. Qed.
+Lemma ra_included_r x y : y ≼ x ⋅ y.
+Proof. rewrite (commutative op); apply ra_included_l. Qed.
 Global Instance: PreOrder included.
 Proof.
   split.
-  * by intros x; rewrite ra_included_spec; exists (unit x); rewrite ra_unit_r.
-  * intros x y z; rewrite ?ra_included_spec; intros [z1 Hy] [z2 Hz].
-    exists (z1 â‹… z2). by rewrite (associative _), <-Hy, <-Hz.
+  * by intros x; exists (unit x); rewrite ra_unit_r.
+  * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
+    by rewrite (associative _), <-Hy, <-Hz.
 Qed.
 Lemma ra_included_unit x : unit x ≼ x.
-Proof. by rewrite ra_included_spec; exists x; rewrite ra_unit_l. Qed.
-Lemma ra_included_r x y : y ≼ x ⋅ y.
-Proof. rewrite (commutative _); apply ra_included_l. Qed.
+Proof. by exists x; rewrite ra_unit_l. Qed.
 Lemma ra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
-Proof.
-  rewrite !ra_included_spec.
-  by intros (z1&Hz1); exists z1; rewrite Hz1, (associative (â‹…)).
-Qed.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1, (associative (â‹…)). Qed.
 Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
 Proof. by intros; rewrite <-!(commutative _ z); apply ra_preserving_l. Qed.
-Lemma ra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
-Proof.
-  rewrite ra_included_spec; intros [z Hy]; rewrite Hy; apply ra_unit_weaken.
-Qed.
 
 (** ** Properties of [(⇝)] relation *)
 Global Instance ra_update_preorder : PreOrder ra_update.
@@ -132,7 +125,7 @@ Proof. by intros x; rewrite (commutative op), (left_id _ _). Qed.
 Lemma ra_unit_empty x : unit ∅ ≡ ∅.
 Proof. by rewrite <-(ra_unit_l ∅) at 2; rewrite (right_id _ _). Qed.
 Lemma ra_empty_least x : ∅ ≼ x.
-Proof. by rewrite ra_included_spec; exists x; rewrite (left_id _ _). Qed.
+Proof. by exists x; rewrite (left_id _ _). Qed.
 
 (** * Big ops *)
 Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
diff --git a/iris/sts.v b/iris/sts.v
index 71dbcdfd6..ceee5ea16 100644
--- a/iris/sts.v
+++ b/iris/sts.v
@@ -1,34 +1,34 @@
 Require Export iris.ra.
-Require Import prelude.sets prelude.bsets iris.dra.
+Require Import prelude.sets iris.dra.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments unit _ _ !_ /.
 
 Module sts.
-Inductive t {A B} (R : relation A) (tok : A → bset B) :=
-  | auth : A → bset B → t R tok
-  | frag : set A → bset B → t R tok.
+Inductive t {A B} (R : relation A) (tok : A → set B) :=
+  | auth : A → set B → t R tok
+  | frag : set A → set B → t R tok.
 Arguments auth {_ _ _ _} _ _.
 Arguments frag {_ _ _ _} _ _.
 
 Section sts_core.
-Context {A B : Type} `{∀ x y : B, Decision (x = y)}.
-Context (R : relation A) (tok : A → bset B).
+Context {A B : Type} (R : relation A) (tok : A → set B).
+Infix "≼" := dra_included.
 
 Inductive sts_equiv : Equiv (t R tok) :=
   | auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
   | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
 Global Existing Instance sts_equiv.
-Inductive step : relation (A * bset B) :=
+Inductive step : relation (A * set B) :=
   | Step s1 s2 T1 T2 :
      R s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ → tok s1 ∪ T1 ≡ tok s2 ∪ T2 →
      step (s1,T1) (s2,T2).
 Hint Resolve Step.
-Inductive frame_step (T : bset B) (s1 s2 : A) : Prop :=
+Inductive frame_step (T : set B) (s1 s2 : A) : Prop :=
   | Frame_step T1 T2 :
      T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2.
 Hint Resolve Frame_step.
-Record closed (T : bset B) (S : set A) : Prop := Closed {
+Record closed (T : set B) (S : set A) : Prop := Closed {
   closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅;
   closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
 }.
@@ -37,8 +37,8 @@ Lemma closed_steps S T s1 s2 :
 Proof. induction 3; eauto using closed_step. Qed.
 Global Instance sts_valid : Valid (t R tok) := λ x,
   match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed T S' end.
-Definition up (T : bset B) (s : A) : set A := mkSet (rtc (frame_step T) s).
-Definition up_set (T : bset B) (S : set A) : set A := S ≫= up T.
+Definition up (T : set B) (s : A) : set A := mkSet (rtc (frame_step T) s).
+Definition up_set (T : set B) (S : set A) : set A := S ≫= up T.
 Global Instance sts_unit : Unit (t R tok) := λ x,
   match x with
   | frag S' _ => frag (up_set ∅ S') ∅ | auth s _ => frag (up ∅ s) ∅
@@ -55,12 +55,6 @@ Global Instance sts_op : Op (t R tok) := λ x1 x2,
   | frag _ T1, auth s T2 => auth s (T1 ∪ T2)
   | auth s T1, auth _ T2 => auth s (T1 ∪ T2) (* never happens *)
   end.
-Inductive sts_included : Included (t R tok) :=
-  | frag_frag_included S1 S2 T1 T2 S' :
-     T1 ⊆ T2 → S2 ≡ S1 ∩ S' → closed (T2 ∖ T1) S' → frag S1 T1 ≼ frag S2 T2
-  | frag_auth_included s S T1 T2 : s ∈ S → T1 ⊆ T2 → frag S T1 ≼ auth s T2
-  | auth_auth_included s T1 T2 : T1 ⊆ T2 → auth s T1 ≼ auth s T2.
-Global Existing Instance sts_included.
 Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
   match x1, x2 with
   | frag S1 T1, frag S2 T2 => frag (up_set (T1 ∖ T2) S1) (T1 ∖ T2)
@@ -69,10 +63,9 @@ Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
   | auth s T1, auth _ T2 => frag (up (T1 ∖ T2) s) (T1 ∖ T2)
   end.
 
-Hint Extern 5 (equiv (A:=set _) _ _) => esolve_elem_of : sts.
-Hint Extern 5 (equiv (A:=bset _) _ _) => esolve_elem_of : sts.
-Hint Extern 5 (_ ∈ _) => esolve_elem_of : sts.
-Hint Extern 5 (_ ⊆ _) => esolve_elem_of : sts.
+Hint Extern 10 (equiv (A:=set _) _ _) => esolve_elem_of : sts.
+Hint Extern 10 (_ ∈ _) => esolve_elem_of : sts.
+Hint Extern 10 (_ ⊆ _) => esolve_elem_of : sts.
 Instance: Equivalence ((≡) : relation (t R tok)).
 Proof.
   split.
@@ -112,7 +105,7 @@ Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof. by intros T1 T2 HT S1 S2 HS; unfold up_set; rewrite HS, HT. Qed.
 Lemma elem_of_up s T : s ∈ up T s.
 Proof. constructor. Qed.
-Lemma subseteq_up_set S T : S ⊆ up_set T S.
+Lemma suseteq_up_set S T : S ⊆ up_set T S.
 Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
 Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → closed T (up_set T S).
 Proof.
@@ -135,16 +128,10 @@ Lemma closed_up_empty s : closed ∅ (up ∅ s).
 Proof. eauto using closed_up with sts. Qed.
 Lemma up_closed S T : closed T S → up_set T S ≡ S.
 Proof.
-  intros; split; auto using subseteq_up_set; intros s.
+  intros; split; auto using suseteq_up_set; intros s.
   unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
   induction Hstep; eauto using closed_step.
 Qed.
-Lemma up_set_subseteq T1 T2 S1 S2 :
-  closed (T2 ∖ T1) S2 → up_set (T2 ∖ T1) (S1 ∩ S2) ⊆ S2.
-Proof.
-  intros ? s2; unfold up_set; rewrite elem_of_bind; intros (s1&?&?).
-  apply closed_steps with (T2 ∖ T1) s1; auto with sts.
-Qed.
 Global Instance sts_dra : DRA (t R tok).
 Proof.
   split.
@@ -153,13 +140,13 @@ Proof.
   * by destruct 1; constructor; setoid_subst.
   * by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
   * by do 2 destruct 1; constructor; setoid_subst.
-  * by do 2 destruct 1; inversion_clear 1; econstructor; setoid_subst.
   * assert (∀ T T' S s,
       closed T S → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
     { intros S T T' s [??]; esolve_elem_of. }
     destruct 3; simpl in *; auto using closed_op with sts.
   * intros []; simpl; eauto using closed_up, closed_up_set with sts.
-  * destruct 3; simpl in *; setoid_subst; eauto using closed_up with sts.
+  * intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
+      rewrite ?disjoint_union_difference; auto using closed_up with sts.
     eapply closed_up_set; eauto 2 using closed_disjoint with sts.
   * intros [] [] []; constructor; rewrite ?(associative _); auto with sts.
   * destruct 4; inversion_clear 1; constructor; auto with sts.
@@ -168,22 +155,24 @@ Proof.
   * destruct 3; constructor; auto with sts.
   * intros []; constructor; auto using elem_of_up with sts.
   * intros [|S T]; constructor; auto with sts.
-    assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts.
+    assert (S ⊆ up_set ∅ S); auto using suseteq_up_set with sts.
   * intros [s T|S T]; constructor; auto with sts.
     + by rewrite (up_closed (up _ _)) by auto using closed_up with sts.
     + by rewrite (up_closed (up_set _ _)) by auto using closed_up_set with sts.
-  * destruct 3 as [S1 S2| |]; simpl;
-      match goal with |- _ ≼ frag ?S _ => apply frag_frag_included with S end;
-      eauto using closed_up_empty, closed_up_set_empty;
-      unfold up_set; esolve_elem_of.
-  * destruct 3 as [S1 S2 T1 T2| |]; econstructor; eauto with sts.
-    by setoid_replace ((T1 ∪ T2) ∖ T1) with T2 by esolve_elem_of.
-  * destruct 3; constructor; eauto using elem_of_up with sts.
-  * destruct 3 as [S1 S2 T1 T2 S'| |]; constructor;
-      rewrite ?(commutative _ (_ ∖ _)), <-?union_difference; auto with sts.
-    assert (S2 ⊆ up_set (T2 ∖ T1) S2) by eauto using subseteq_up_set.
-    assert (up_set (T2 ∖ T1) (S1 ∩ S') ⊆ S') by eauto using up_set_subseteq.
-    esolve_elem_of.
+  * intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)).
+    destruct Hxz; inversion_clear Hy; simpl; split_ands;
+      auto using closed_up_set_empty, closed_up_empty;
+      constructor; unfold up_set; auto with sts.
+  * intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy;
+      constructor; eauto using elem_of_up; auto with sts.
+  * intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
+      inversion Hy; clear Hy; constructor; setoid_subst;
+      rewrite ?disjoint_union_difference by done; auto.
+    split; [|apply intersection_greatest; auto using suseteq_up_set with sts].
+    apply intersection_greatest; [auto with sts|].
+    intros s2; rewrite elem_of_intersection.
+    unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
+    apply closed_steps with T2 s1; auto with sts.
 Qed.
 Lemma step_closed s1 s2 T1 T2 S Tf :
   step (s1,T1) (s2,T2) → closed Tf S → s1 ∈ S → T1 ∩ Tf ≡ ∅ →
@@ -198,16 +187,15 @@ End sts.
 
 Section sts_ra.
 Context {A B : Type} `{∀ x y : B, Decision (x = y)}.
-Context (R : relation A) (tok : A → bset B).
+Context (R : relation A) (tok : A → set B).
 
 Definition sts := validity (valid : sts.t R tok → Prop).
 Global Instance sts_unit : Unit sts := validity_unit _.
 Global Instance sts_op : Op sts := validity_op _.
-Global Instance sts_included : Included sts := validity_included _.
 Global Instance sts_minus : Minus sts := validity_minus _.
 Global Instance sts_ra : RA sts := validity_ra _.
-Definition sts_auth (s : A) (T : bset B) : sts := to_validity (sts.auth s T).
-Definition sts_frag (S : set A) (T : bset B) : sts :=
+Definition sts_auth (s : A) (T : set B) : sts := to_validity (sts.auth s T).
+Definition sts_frag (S : set A) (T : set B) : sts :=
   to_validity (sts.frag S T).
 Lemma sts_update s1 s2 T1 T2 :
   sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ⇝ sts_auth s2 T2.
diff --git a/prelude/collections.v b/prelude/collections.v
index 619134db2..a0bbafe61 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -297,6 +297,8 @@ Section collection.
   Proof. esolve_elem_of. Qed.
   Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
   Proof. esolve_elem_of. Qed.
+  Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y.
+  Proof. esolve_elem_of. Qed.
 
   Section leibniz.
     Context `{!LeibnizEquiv C}.
@@ -315,6 +317,8 @@ Section collection.
     Lemma difference_intersection_distr_l_L X Y Z :
       (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z.
     Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
+    Lemma disjoint_union_difference_L X Y : X ∩ Y = ∅ → (X ∪ Y) ∖ X = Y.
+    Proof. unfold_leibniz. apply disjoint_union_difference. Qed.
   End leibniz.
 
   Section dec.
-- 
GitLab