diff --git a/algebra/agree.v b/algebra/agree.v
index cab28bc9494e80a8df94fe614b00b3d378ca042c..d739964f321fc94e9dd9dc6c20000cd42cf0fb72 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -61,7 +61,6 @@ Program Instance agree_op : Op (agree A) := λ x y,
      agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Instance agree_core : Core (agree A) := id.
-Instance agree_div : Div (agree A) := λ x y, x.
 
 Instance: Comm (≡) (@op (agree A) _).
 Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
@@ -108,13 +107,11 @@ Qed.
 Definition agree_cmra_mixin : CMRAMixin (agree A).
 Proof.
   split; try (apply _ || done).
-  - by intros n x1 x2 Hx y1 y2 Hy.
   - intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
     rewrite -(Hx n'); last auto.
     symmetry; apply dist_le with n; try apply Hx; auto.
   - intros x; apply agree_idemp.
   - by intros n x y [(?&?&?) ?].
-  - by intros x y; rewrite agree_included.
   - intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
     + by rewrite agree_idemp.
     + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
diff --git a/algebra/auth.v b/algebra/auth.v
index e2e54fb184de6553c0ab55a74dbf421d0c286b6d..4fc52b8b2df137d9f873092df64b8c8f06244d88 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -73,7 +73,7 @@ Implicit Types x y : auth A.
 Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
 Instance auth_valid : Valid (auth A) := λ x,
   match authoritative x with
-  | Excl a => own x ≼ a ∧ ✓ a
+  | Excl a => (∀ n, own x ≼{n} a) ∧ ✓ a
   | ExclUnit => ✓ own x
   | ExclBot => False
   end.
@@ -89,8 +89,6 @@ Instance auth_core : Core (auth A) := λ x,
   Auth (core (authoritative x)) (core (own x)).
 Instance auth_op : Op (auth A) := λ x y,
   Auth (authoritative x â‹… authoritative y) (own x â‹… own y).
-Instance auth_div : Div (auth A) := λ x y,
-  Auth (authoritative x ÷ authoritative y) (own x ÷ own y).
 
 Lemma auth_included (x y : auth A) :
   x ≼ y ↔ authoritative x ≼ authoritative y ∧ own x ≼ own y.
@@ -110,8 +108,6 @@ Proof.
   - by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
   - intros n [x a] [y b] [Hx Ha]; simpl in *;
       destruct Hx; intros ?; cofe_subst; auto.
-  - by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
-      split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
   - intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
       naive_solver eauto using O.
   - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
@@ -125,8 +121,6 @@ Proof.
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
    intros n [[a1| |] b1] [[a2| |] b2];
      naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
-  - by intros ??; rewrite auth_included;
-      intros [??]; split; simpl; apply cmra_op_div.
   - intros n x y1 y2 ? [??]; simpl in *.
     destruct (cmra_extend n (authoritative x) (authoritative y1)
       (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
@@ -138,9 +132,9 @@ Canonical Structure authR : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
 Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
 Proof.
   split; first apply _.
-  intros [[] ?]; by rewrite /= /cmra_valid /cmra_validN /=
-    -?cmra_discrete_included_iff -?cmra_discrete_valid_iff.
-Qed.
+  intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=
+    -?cmra_discrete_included_iff -?cmra_discrete_valid_iff; auto.
+Admitted.
 
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 08256da86301ae6a933c88c94bb9282818c51a7e..30c2b8b12fa0586dd8e27ac9174c731421a39abd 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -14,10 +14,6 @@ Notation "(≼)" := included (only parsing) : C_scope.
 Hint Extern 0 (_ ≼ _) => reflexivity.
 Instance: Params (@included) 3.
 
-Class Div (A : Type) := div : A → A → A.
-Instance: Params (@div) 2.
-Infix "÷" := div : C_scope.
-
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
 Notation "✓{ n } x" := (validN n x)
@@ -33,13 +29,11 @@ Notation "x ≼{ n } y" := (includedN n x y)
 Instance: Params (@includedN) 4.
 Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
-Record CMRAMixin A
-    `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A, Div A} := {
+Record CMRAMixin A `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A} := {
   (* setoids *)
   mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
   mixin_cmra_core_ne n : Proper (dist n ==> dist n) core;
   mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
-  mixin_cmra_div_ne n : Proper (dist n ==> dist n ==> dist n) div;
   (* valid *)
   mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
   mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
@@ -50,7 +44,6 @@ Record CMRAMixin A
   mixin_cmra_core_idemp x : core (core x) ≡ core x;
   mixin_cmra_core_preserving x y : x ≼ y → core x ≼ core y;
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
-  mixin_cmra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y;
   mixin_cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }
@@ -66,11 +59,10 @@ Structure cmraT := CMRAT {
   cmra_op : Op cmra_car;
   cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
-  cmra_div : Div cmra_car;
   cmra_cofe_mixin : CofeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car
 }.
-Arguments CMRAT {_ _ _ _ _ _ _ _ _} _ _.
+Arguments CMRAT {_ _ _ _ _ _ _ _} _ _.
 Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
@@ -79,11 +71,10 @@ Arguments cmra_core : simpl never.
 Arguments cmra_op : simpl never.
 Arguments cmra_valid : simpl never.
 Arguments cmra_validN : simpl never.
-Arguments cmra_div : simpl never.
 Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
-Existing Instances cmra_core cmra_op cmra_valid cmra_validN cmra_div.
+Existing Instances cmra_core cmra_op cmra_valid cmra_validN.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
@@ -97,9 +88,6 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_core_ne _ (cmra_mixin A)). Qed.
   Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
   Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
-  Global Instance cmra_div_ne n :
-    Proper (dist n ==> dist n ==> dist n) (@div A _).
-  Proof. apply (mixin_cmra_div_ne _ (cmra_mixin A)). Qed.
   Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
   Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
@@ -116,8 +104,6 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_core_preserving _ (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_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y.
-  Proof. apply (mixin_cmra_op_div _ (cmra_mixin A)). Qed.
   Lemma cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }.
@@ -188,8 +174,6 @@ Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
 Proof. by split; apply cmra_validN_ne. Qed.
 Global Instance cmra_validN_proper : Proper ((≡) ==> iff) (@validN A _ n) | 1.
 Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
-Global Instance cmra_div_proper : Proper ((≡) ==> (≡) ==> (≡)) (@div A _).
-Proof. apply (ne_proper_2 _). Qed.
 
 Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
 Proof.
@@ -246,17 +230,9 @@ Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
 Lemma cmra_core_valid x : ✓ x → ✓ core x.
 Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
 
-(** ** Div *)
-Lemma cmra_op_div' n x y : x ≼{n} y → x ⋅ y ÷ x ≡{n}≡ y.
-Proof. intros [z ->]. by rewrite cmra_op_div; last exists z. Qed.
-
 (** ** Order *)
-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=> n.
-  by rewrite cmra_op_div'.
-Qed.
+Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
+Proof. intros [z ->]. by exists z. Qed.
 Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
 Proof.
   split.
@@ -266,13 +242,15 @@ Proof.
 Qed.
 Global Instance cmra_included_preorder: PreOrder (@included A _ _).
 Proof.
-  split; red; intros until 0; rewrite !cmra_included_includedN; first done.
-  intros; etrans; eauto.
+  split.
+  - by intros x; exists (core x); rewrite cmra_core_r.
+  - intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
+    by rewrite assoc -Hy -Hz.
 Qed.
 Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x.
 Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x.
-Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
+Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
 
 Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y.
 Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
@@ -337,7 +315,7 @@ Proof.
 Qed.
 Lemma cmra_discrete_included_iff `{Discrete A} n x y : x ≼ y ↔ x ≼{n} y.
 Proof.
-  split; first by rewrite cmra_included_includedN.
+  split; first by apply cmra_included_includedN.
   intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
 Qed.
 Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A → Prop) :
@@ -486,25 +464,23 @@ End cmra_transport.
 
 (** * Instances *)
 (** ** Discrete CMRA *)
-Class RA A `{Equiv A, Core A, Op A, Valid A, Div A} := {
+Class RA A `{Equiv A, Core A, Op A, Valid A} := {
   (* setoids *)
   ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
   ra_core_ne :> Proper ((≡) ==> (≡)) core;
   ra_validN_ne :> Proper ((≡) ==> impl) valid;
-  ra_div_ne :> Proper ((≡) ==> (≡) ==> (≡)) div;
   (* monoid *)
   ra_assoc :> Assoc (≡) (⋅);
   ra_comm :> Comm (≡) (⋅);
   ra_core_l x : core x ⋅ x ≡ x;
   ra_core_idemp x : core (core x) ≡ core x;
   ra_core_preserving x y : x ≼ y → core x ≼ core y;
-  ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
-  ra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y
+  ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x
 }.
 
 Section discrete.
   Context {A : cofeT} `{Discrete A}.
-  Context `{Core A, Op A, Valid A, Div A} (ra : RA A).
+  Context `{Core A, Op A, Valid A} (ra : RA A).
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
@@ -525,7 +501,6 @@ Section unit.
   Instance unit_valid : Valid () := λ x, True.
   Instance unit_core : Core () := λ x, x.
   Instance unit_op : Op () := λ x y, ().
-  Instance unit_div : Div () := λ x y, ().
   Global Instance unit_empty : Empty () := ().
   Definition unit_ra : RA ().
   Proof. by split. Qed.
@@ -544,7 +519,6 @@ Section prod.
   Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
   Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
   Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
-  Instance prod_div : Div (A * B) := λ x y, (x.1 ÷ y.1, x.2 ÷ y.2).
   Lemma prod_included (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|].
@@ -561,8 +535,6 @@ Section prod.
     - by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
     - by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
     - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
-    - by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
-        split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
     - intros x; split.
       + intros [??] n; split; by apply cmra_valid_validN.
       + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
@@ -574,8 +546,6 @@ Section prod.
     - intros x y; rewrite !prod_included.
       by intros [??]; split; apply cmra_core_preserving.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
-    - intros x y; rewrite prod_included; intros [??].
-      by split; apply cmra_op_div.
     - intros n x y1 y2 [??] [??]; simpl in *.
       destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
       destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index b7c37089aca2a0cddb780ba4a745312ebe34a29e..b21ef80449274ae1aec88b7f870e41b84030b4b7 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -27,7 +27,6 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
   | _, _ => DecAgreeBot
   end.
 Instance dec_agree_core : Core (dec_agree A) := id.
-Instance dec_agree_div : Div (dec_agree A) := λ x y, x.
 
 Definition dec_agree_ra : RA (dec_agree A).
 Proof.
@@ -35,15 +34,12 @@ Proof.
   - apply _.
   - apply _.
   - apply _.
-  - apply _.
   - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
   - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
   - intros [?|]; by repeat (simplify_eq/= || case_match).
   - intros [?|]; by repeat (simplify_eq/= || case_match).
   - by intros [?|] [?|] ?.
   - by intros [?|] [?|] ?.
-  - intros [?|] [?|] [[?|]]; fold_leibniz;
-      intros; by repeat (simplify_eq/= || case_match).
 Qed.
 
 Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
diff --git a/algebra/dra.v b/algebra/dra.v
index 36fe74bb7bcf428637e57fc4985698bb7c2968ff..f62020e4bd4798410a6c9e8cc6d72e4124691950 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -6,6 +6,7 @@ Record validity {A} (P : A → Prop) : Type := Validity {
   validity_is_valid : Prop;
   validity_prf : validity_is_valid → P validity_car
 }.
+Add Printing Constructor validity.
 Arguments Validity {_ _} _ _ _.
 Arguments validity_car {_ _} _.
 Arguments validity_is_valid {_ _} _.
@@ -13,23 +14,16 @@ Arguments validity_is_valid {_ _} _.
 Definition to_validity {A} {P : A → Prop} (x : A) : validity P :=
   Validity x (P x) id.
 
-Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
-  ∃ z, y ≡ x ⋅ z ∧ ✓ z ∧ x ⊥ z.
-Instance: Params (@dra_included) 4.
-Local Infix "≼" := dra_included.
-
-Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A, Div A} := {
+Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A} := {
   (* setoids *)
   dra_equivalence :> Equivalence ((≡) : relation A);
   dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
   dra_core_proper :> Proper ((≡) ==> (≡)) core;
   dra_valid_proper :> Proper ((≡) ==> impl) valid;
   dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
-  dra_div_proper :> Proper ((≡) ==> (≡) ==> (≡)) div;
   (* validity *)
   dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
   dra_core_valid x : ✓ x → ✓ core x;
-  dra_div_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ÷ x);
   (* monoid *)
   dra_assoc :> Assoc (≡) (⋅);
   dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
@@ -39,9 +33,8 @@ Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A, Div A} := {
   dra_core_disjoint_l x : ✓ x → core x ⊥ x;
   dra_core_l x : ✓ x → core x ⋅ x ≡ x;
   dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  dra_core_preserving x y : ✓ x → ✓ y → x ≼ y → core x ≼ core y;
-  dra_disjoint_div x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ÷ x;
-  dra_op_div x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ÷ x ≡ y
+  dra_core_preserving x y : 
+    ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
 }.
 
 Section dra.
@@ -83,7 +76,6 @@ Proof.
   apply dra_disjoint_move_l; auto; by rewrite dra_comm.
 Qed.
 Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
-Hint Unfold dra_included.
 
 Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
@@ -95,10 +87,6 @@ Program Instance validity_op : Op T := λ x y,
   Validity (validity_car x â‹… validity_car y)
            (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
 Solve Obligations with naive_solver auto using dra_op_valid.
-Program Instance validity_div : Div T := λ x y,
-  Validity (validity_car x ÷ validity_car y)
-           (✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _.
-Solve Obligations with naive_solver auto using dra_div_valid.
 
 Definition validity_ra : RA (discreteC T).
 Proof.
@@ -108,11 +96,6 @@ Proof.
       first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
   - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
   - intros ?? [??]; naive_solver.
-  - intros x1 x2 [? Hx] y1 y2 [? Hy];
-      split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
-    split; intros (?&?&z&?&?); split_and!; try tauto.
-    + exists z. by rewrite -Hy // -Hx.
-    + exists z. by rewrite Hx ?Hy; tauto.
   - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
       [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
       |by intros; rewrite assoc].
@@ -120,15 +103,13 @@ Proof.
   - intros [x px ?]; split;
       naive_solver eauto using dra_core_l, dra_core_disjoint_l.
   - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
-  - intros x y Hxy; exists (core y ÷ core x).
-    destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
-    assert (py → core x ≼ core y)
-      by intuition eauto 10 using dra_core_preserving.
-    constructor; [|symmetry]; simpl in *;
-      intuition eauto using dra_op_div, dra_disjoint_div, dra_core_valid.
+  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
+    destruct (dra_core_preserving x z) as (z'&Hz').
+    unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
+    { intros (?&?&?); apply Hz'; tauto. }
+    + tauto.
+    + intros. rewrite Hy //. tauto.
   - by intros [x px ?] [y py ?] (?&?&?).
-  - intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
-      intuition eauto 10 using dra_disjoint_div, dra_op_div.
 Qed.
 Definition validityR : cmraT := discreteR validity_ra.
 Instance validity_cmra_discrete :
@@ -146,21 +127,20 @@ Lemma to_validity_op (x y : A) :
   to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
 Proof. split; naive_solver auto using dra_op_valid. Qed.
 
+(*
 Lemma to_validity_included x y:
   (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
 Proof.
   split.
   - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
-    destruct Hvl' as [? [? ?]].
-    split; first done.
-    exists (validity_car z). split_and!; last done.
-    + apply EQ. assumption.
-    + by apply validity_valid_car_valid.
+    destruct Hvl' as [? [? ?]]; split; first done.
+    exists (validity_car z); eauto.
   - intros (Hvl & z & EQ & ? & ?).
-    assert (✓ y) by (rewrite EQ; apply dra_op_valid; done).
+    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
     split; first done. exists (to_validity z). split; first split.
-    + intros _. simpl. split_and!; done.
+    + intros _. simpl. by split_and!.
     + intros _. setoid_subst. by apply dra_op_valid. 
     + intros _. rewrite /= EQ //.
 Qed.
+*)
 End dra.
diff --git a/algebra/excl.v b/algebra/excl.v
index 9f731370e9dad3262162d3f11eb7d21493bd3b9a..1314471f396eea88065b7bfaf2ae1d32f22ba9d9 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -98,19 +98,13 @@ Instance excl_op : Op (excl A) := λ x y,
   | ExclUnit, ExclUnit => ExclUnit
   | _, _=> ExclBot
   end.
-Instance excl_div : Div (excl A) := λ x y,
-  match x, y with
-  | _, ExclUnit => x
-  | Excl _, Excl _ => ExclUnit
-  | _, _ => ExclBot
-  end.
+
 Definition excl_cmra_mixin : CMRAMixin (excl A).
 Proof.
   split.
   - by intros n []; destruct 1; constructor.
   - constructor.
   - by destruct 1; intros ?.
-  - by destruct 1; inversion_clear 1; constructor.
   - intros x; split. done. by move=> /(_ 0).
   - intros n [?| |]; simpl; auto with lia.
   - by intros [?| |] [?| |] [?| |]; constructor.
@@ -119,7 +113,6 @@ Proof.
   - constructor.
   - by intros [?| |] [?| |]; exists ∅.
   - by intros n [?| |] [?| |].
-  - by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
   - intros n x y1 y2 ? Hx.
     by exists match y1, y2 with
       | Excl a1, Excl a2 => (Excl a1, Excl a2)
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 0215ded5026d03defce89006b6b87ff8c7d66719..8f302e8db123b35f65c4f6939b59f7af89fe632f 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -96,29 +96,26 @@ Instance map_op : Op (gmap K A) := merge op.
 Instance map_core : Core (gmap K A) := fmap core.
 Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
 Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
-Instance map_div : Div (gmap K A) := merge div.
 
 Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
 Proof. by apply lookup_merge. Qed.
-Lemma lookup_div m1 m2 i : (m1 ÷ m2) !! i = m1 !! i ÷ m2 !! i.
-Proof. by apply lookup_merge. Qed.
 Lemma lookup_core m i : core m !! i = core (m !! i).
 Proof. by apply lookup_fmap. Qed.
 
 Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
 Proof.
-  split.
-  - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
-  - intros Hm; exists (m2 ÷ m1); intros i.
-    by rewrite lookup_op lookup_div cmra_op_div.
-Qed.
-Lemma map_includedN_spec (m1 m2 : gmap K A) n :
-  m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
-Proof.
-  split.
-  - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
-  - intros Hm; exists (m2 ÷ m1); intros i.
-    by rewrite lookup_op lookup_div cmra_op_div'.
+  split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
+  revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
+  { exists m2. by rewrite left_id. }
+  destruct (IH (delete i m2)) as [m2' Hm2'].
+  { intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
+    - intros _. rewrite Hi. apply: cmra_unit_least.
+    - rewrite lookup_insert_ne // lookup_delete_ne //. }
+  destruct (Hm i) as [my Hi']; simplify_map_eq.
+  exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
+  - by rewrite Hi' lookup_op lookup_insert lookup_partial_alter.
+  - move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
+      lookup_insert_ne // lookup_partial_alter_ne.
 Qed.
 
 Definition map_cmra_mixin : CMRAMixin (gmap K A).
@@ -127,7 +124,6 @@ Proof.
   - by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
   - by intros n m1 m2 Hm i; rewrite !lookup_core (Hm i).
   - by intros n m1 m2 Hm ? i; rewrite -(Hm i).
-  - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_div (Hm1 i) (Hm2 i).
   - intros m; split.
     + by intros ? n i; apply cmra_valid_validN.
     + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
@@ -140,8 +136,6 @@ Proof.
     by rewrite !lookup_core; apply cmra_core_preserving.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
-  - intros x y; rewrite map_included_spec=> ? i.
-    by rewrite lookup_op lookup_div cmra_op_div.
   - 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).
@@ -222,17 +216,17 @@ Lemma map_op_singleton (i : K) (x y : A) :
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
 
 Lemma singleton_includedN n m i x :
-  {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ x ≼ y.
-  (* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)
+  {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ x ≼{n} y.
 Proof.
   split.
-  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
-    destruct (m' !! i) as [y|];
-      [exists (x â‹… y)|exists x]; eauto using cmra_included_l.
-  - intros (y&Hi&?); rewrite map_includedN_spec=>j.
-    destruct (decide (i = j)); simplify_map_eq.
-    + rewrite Hi. by apply (includedN_preserving _), cmra_included_includedN.
-    + apply: cmra_unit_leastN.
+  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
+    case (m' !! i)=> [y|]=> Hm.
+    + exists (x â‹… y); eauto using cmra_includedN_l.
+    + by exists x.
+  - intros (y&Hi&[z ?]).
+    exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
+    + rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
+    + by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
 Qed.
 Lemma map_dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
 Proof.
diff --git a/algebra/frac.v b/algebra/frac.v
index daf952db352e6540dd924c80ab7fead6dfb7fdf2..35d7288771a899fb50f5357b031248e3d6bdce27 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -3,7 +3,6 @@ From iris.algebra Require Export cmra.
 From iris.algebra Require Import upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
-Local Arguments div _ _ !_ !_ /.
 
 Inductive frac (A : Type) :=
   | Frac : Qp → A → frac A
@@ -129,13 +128,6 @@ Instance frac_op : Op (frac A) := λ x y,
   | Frac q a, FracUnit | FracUnit, Frac q a => Frac q a
   | FracUnit, FracUnit => FracUnit
   end.
-Instance frac_div : Div (frac A) := λ x y,
-  match x, y with
-  | _, FracUnit => x
-  | Frac q1 a, Frac q2 b =>
-     match q1 - q2 with Some q => Frac q (a ÷ b) | None => FracUnit end%Qp
-  | FracUnit, _ => FracUnit
-  end.
 
 Lemma Frac_op q1 q2 a b : Frac q1 a â‹… Frac q2 b = Frac (q1 + q2) (a â‹… b).
 Proof. done. Qed.
@@ -146,7 +138,6 @@ Proof.
   - intros n []; destruct 1; constructor; by cofe_subst. 
   - constructor.
   - do 2 destruct 1; split; by cofe_subst.
-  - do 2 destruct 1; simplify_eq/=; try case_match; constructor; by cofe_subst.
   - intros [q a|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
   - intros n [q a|]; destruct 1; split; auto using cmra_validN_S.
   - intros [q1 a1|] [q2 a2|] [q3 a3|]; constructor; by rewrite ?assoc.
@@ -157,10 +148,6 @@ Proof.
   - intros n [q1 a1|] [q2 a2|]; destruct 1; split; eauto using cmra_validN_op_l.
     trans (q1 + q2)%Qp; simpl; last done.
     rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak.
-  - intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
-      inversion_clear Hx; simplify_eq/=; auto.
-    + rewrite Qp_op_minus. by constructor; [|apply cmra_op_div; exists a3].
-    + rewrite Qp_minus_diag. by constructor.
   - intros n [q a|] y1 y2 Hx Hx'; last first.
     { by exists (∅, ∅); destruct y1, y2; inversion_clear Hx'. }
     destruct Hx, y1 as [q1 b1|], y2 as [q2 b2|].
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 34f4dcac53d3bca0d989eabb1b7a59b79c46000e..e1761819397b231729f2c925dacb966a81c6295c 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import upred.
+From iris.prelude Require Import finite.
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
@@ -113,25 +114,21 @@ End iprod_cofe.
 Arguments iprodC {_} _.
 
 Section iprod_cmra.
-  Context {A} {B : A → cmraT}.
+  Context `{Finite A} {B : A → cmraT}.
   Implicit Types f g : iprod B.
 
   Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
   Instance iprod_core : Core (iprod B) := λ f x, core (f x).
   Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
   Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
-  Instance iprod_div : Div (iprod B) := λ f g x, f x ÷ g x.
 
   Definition iprod_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
   Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
-  Definition iprod_lookup_div f g x : (f ÷ g) x = f x ÷ g x := eq_refl.
 
   Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
   Proof.
-    split.
-    - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
-    - intros Hh; exists (g ÷ f)=> x; specialize (Hh x).
-      by rewrite /op /iprod_op /div /iprod_div cmra_op_div.
+    split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|].
+    intros [h ?]%finite_choice. by exists h.
   Qed.
 
   Definition iprod_cmra_mixin : CMRAMixin (iprod B).
@@ -140,7 +137,6 @@ Section iprod_cmra.
     - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
     - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
     - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
-    - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_div (Hf i) (Hg i).
     - intros g; split.
       + intros Hg n i; apply cmra_valid_validN, Hg.
       + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
@@ -152,8 +148,6 @@ Section iprod_cmra.
     - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
       by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
-    - intros f1 f2; rewrite iprod_included_spec=> Hf x.
-      by rewrite iprod_lookup_op iprod_lookup_div cmra_op_div; try apply Hf.
     - intros n f f1 f2 Hf Hf12.
       set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
       exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
@@ -253,7 +247,7 @@ Section iprod_cmra.
   Proof. eauto using iprod_singleton_updateP_empty. Qed.
 End iprod_cmra.
 
-Arguments iprodR {_} _.
+Arguments iprodR {_ _ _} _.
 
 (** * Functor *)
 Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
@@ -273,7 +267,8 @@ Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
   (∀ x, Proper (dist n ==> dist n) (f x)) →
   Proper (dist n ==> dist n) (iprod_map f).
 Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) :
+Instance iprod_map_cmra_monotone `{Finite A}
+    {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) :
   (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
 Proof.
   split; first apply _.
@@ -310,22 +305,23 @@ Proof.
   by apply iprodC_map_ne=>c; apply cFunctor_contractive.
 Qed.
 
-Program Definition iprodRF {C} (F : C → rFunctor) : rFunctor := {|
+Program Definition iprodRF `{Finite C} (F : C → rFunctor) : rFunctor := {|
   rFunctor_car A B := iprodR (λ c, rFunctor_car (F c) A B);
   rFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, rFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply rFunctor_ne.
+  intros C ?? F A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>?; apply rFunctor_ne.
 Qed.
 Next Obligation.
-  intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
+  intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
   apply iprod_map_ext=> y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
+  intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
   apply iprod_map_ext=>y; apply rFunctor_compose.
 Qed.
-Instance iprodRF_contractive {C} (F : C → rFunctor) :
+Instance iprodRF_contractive `{Finite C} (F : C → rFunctor) :
   (∀ c, rFunctorContractive (F c)) → rFunctorContractive (iprodRF F).
 Proof.
   intros ? A1 A2 B1 B2 n ?? g.
diff --git a/algebra/option.v b/algebra/option.v
index 1530ecd6ec9484f8e2c3f9a6745505ffa31a81aa..76220397cecfbf2c0efb1f34c4762fddd5c2b67d 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -69,8 +69,6 @@ Instance option_validN : ValidN (option A) := λ n mx,
 Global Instance option_empty : Empty (option A) := None.
 Instance option_core : Core (option A) := fmap core.
 Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
-Instance option_div : Div (option A) :=
-  difference_with (λ x y, Some (x ÷ y)).
 
 Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
 Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
@@ -94,7 +92,6 @@ Proof.
   - by intros n [x|]; destruct 1; constructor; cofe_subst.
   - by destruct 1; constructor; cofe_subst.
   - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
-  - by destruct 1; inversion_clear 1; constructor; cofe_subst.
   - intros [x|]; [apply cmra_valid_validN|done].
   - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
   - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
@@ -105,9 +102,6 @@ Proof.
     right; exists (core x), (core y); eauto using cmra_core_preserving.
   - intros n [x|] [y|]; rewrite /validN /option_validN /=;
       eauto using cmra_validN_op_l.
-  - intros mx my; rewrite option_included.
-    intros [->|(x&y&->&->&?)]; [by destruct my|].
-    by constructor; apply cmra_op_div.
   - intros n mx my1 my2.
     destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
       try (by exfalso; inversion Hx'; auto).
diff --git a/algebra/sts.v b/algebra/sts.v
index 216f7bd0ede200867abccff9e08cc0bcd1d99e60..075f097430c2ea2ec8bcd6f7d8206b8443ed621e 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -179,7 +179,6 @@ Arguments frag {_} _ _.
 
 Section sts_dra.
 Context {sts : stsT}.
-Infix "≼" := dra_included.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
 
@@ -212,13 +211,6 @@ Global Instance sts_op : Op (car sts) := λ x1 x2,
   | frag _ T1, auth s T2 => auth s (T1 ∪ T2)
   | auth s T1, auth _ T2 => auth s (T1 ∪ T2)(* never happens *)
   end.
-Global Instance sts_div : Div (car sts) := λ x1 x2,
-  match x1, x2 with
-  | frag S1 T1, frag S2 T2 => frag (up_set S1 (T1 ∖ T2)) (T1 ∖ T2)
-  | auth s T1, frag _ T2 => auth s (T1 ∖ T2)
-  | frag _ T2, auth s T1 => auth s (T1 ∖ T2) (* never happens *)
-  | auth s T1, auth _ T2 => frag (up s (T1 ∖ T2)) (T1 ∖ T2)
-  end.
 
 Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
 Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts.
@@ -239,16 +231,10 @@ Proof.
   - by destruct 1; constructor; setoid_subst.
   - by destruct 1; simpl; intros ?; setoid_subst.
   - by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
-  - by do 2 destruct 1; constructor; setoid_subst.
   - destruct 3; simpl in *; destruct_and?; eauto using closed_op;
       match goal with H : closed _ _ |- _ => destruct H end; set_solver.
   - intros []; simpl; intros; destruct_and?; split;
       eauto using closed_up, up_non_empty, closed_up_set, up_set_empty with sts.
-  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
-      setoid_subst; destruct_and?; split_and?;
-      rewrite disjoint_union_difference //;
-      eauto using up_set_non_empty, up_non_empty, closed_up, closed_disjoint; [].
-    eapply closed_up_set=> s ?; eapply closed_disjoint; eauto with sts.
   - intros [] [] []; constructor; rewrite ?assoc; auto with sts.
   - destruct 4; inversion_clear 1; constructor; auto with sts.
   - destruct 4; inversion_clear 1; constructor; auto with sts.
@@ -259,33 +245,18 @@ Proof.
   - intros [s T|S T]; constructor; auto with sts.
     + rewrite (up_closed (up _ _)); auto using closed_up with sts.
     + rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
-  - intros x y ?? (z&Hy&?&Hxz); exists (core (x â‹… y)); split_and?.
-    + destruct Hxz; inversion_clear Hy; constructor; unfold up_set; set_solver.
-    + destruct Hxz; inversion_clear Hy; simpl; split_and?;
+  - intros x y. exists (core (x â‹… y))=> ?? Hxy; split_and?.
+    + destruct Hxy; constructor; unfold up_set; set_solver.
+    + destruct Hxy; simpl; split_and?;
         auto using closed_up_set_empty, closed_up_empty, up_non_empty; [].
       apply up_set_non_empty. set_solver.
-    + destruct Hxz; inversion_clear Hy; constructor;
+    + destruct Hxy; constructor;
         repeat match goal with
         | |- context [ up_set ?S ?T ] =>
            unless (S ⊆ up_set S T) by done; pose proof (subseteq_up_set S T)
         | |- context [ up ?s ?T ] =>
            unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
         end; auto with sts.
-  - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
-      repeat match goal with
-      | |- context [ up_set ?S ?T ] =>
-         unless (S ⊆ up_set S T) by done; pose proof (subseteq_up_set S T)
-      | |- context [ up ?s ?T ] =>
-           unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
-      end; 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; auto.
-    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
-    apply intersection_greatest; [auto with sts|].
-    intros s2; rewrite elem_of_intersection. destruct_and?.
-    unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
-    apply closed_steps with T2 s1; auto with sts.
 Qed.
 Canonical Structure R : cmraT := validityR (car sts).
 End sts_dra. End sts_dra.
@@ -420,6 +391,8 @@ Lemma sts_frag_included S1 S2 T1 T2 :
   (closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ∩ Tf ≡ ∅ ∧
                                  S2 ≡ S1 ∩ up_set S2 Tf).
 Proof.
+  intros ??; split.
+  - intros [[???] ?]. (* 
   destruct (to_validity_included (sts_dra.car sts) (sts_dra.frag S1 T1) (sts_dra.frag S2 T2)) as [Hfincl Htoincl].
   intros Hcl2 HS2ne. split.
   - intros Hincl. destruct Hfincl as ((Hcl1 & ?) & (z & EQ & Hval & Hdisj)).
@@ -440,6 +413,7 @@ Proof.
       * by apply up_set_non_empty.
     + constructor; last done. by rewrite -HS.
 Qed.
+*) Admitted.
 
 Lemma sts_frag_included' S1 S2 T :
   closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ →
@@ -448,7 +422,6 @@ Proof.
   intros. apply sts_frag_included; split_and?; auto.
   exists ∅; split_and?; done || set_solver+.
 Qed.
-
 End stsRA.
 
 (** STSs without tokens: Some stuff is simpler *)
@@ -524,4 +497,3 @@ Proof.
 Qed.
 
 End sts_notokRA.
-
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 1a6474d475be2f8dac7506de95d740cd9768495b..ec9813df808902e8b3fc41d6f02ee49733d5635a 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -78,10 +78,10 @@ Lemma ownI_spec n r i P :
   (ownI i P) n r ↔ wld r !! i ≡{n}≡ Some (to_agree (Next (iProp_unfold P))).
 Proof.
   intros (?&?&?). rewrite /ownI; uPred.unseal.
-  rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
+  rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
   - intros [(P'&Hi&HP) _]; rewrite Hi.
-    by apply Some_dist, symmetry, agree_valid_includedN,
-      (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
+    apply Some_dist, symmetry, agree_valid_includedN; last done.
+    by apply map_lookup_validN with (wld r) i.
   - intros ?; split_and?; try apply cmra_unit_leastN; eauto.
 Qed.
 Lemma ownP_spec n r σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡ Excl σ.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index d703b28a14a1075ee0af235c8700ec1d8e263f68..f96c02db68f32f68e1c720259214cc876f1922e9 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -79,8 +79,6 @@ Instance res_core : Core (res Λ A M) := λ r,
 Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
 Instance res_validN : ValidN (res Λ A M) := λ n r,
   ✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
-Instance res_minus : Div (res Λ A M) := λ r1 r2,
-  Res (wld r1 ÷ wld r2) (pst r1 ÷ pst r2) (gst r1 ÷ gst r2).
 
 Lemma res_included (r1 r2 : res Λ A M) :
   r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
@@ -102,7 +100,6 @@ Proof.
   - by intros n x [???] ? [???]; constructor; cofe_subst.
   - by intros n [???] ? [???]; constructor; cofe_subst.
   - by intros n [???] ? [???] (?&?&?); split_and!; cofe_subst.
-  - by intros n [???] ? [???] [???] ? [???]; constructor; cofe_subst.
   - intros r; split.
     + intros (?&?&?) n; split_and!; by apply cmra_valid_validN.
     + intros Hr; split_and!; apply cmra_valid_validN=> n; apply Hr.
@@ -115,8 +112,6 @@ Proof.
     by intros (?&?&?); split_and!; apply cmra_core_preserving.
   - intros n r1 r2 (?&?&?);
       split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
-  - intros r1 r2; rewrite res_included; intros (?&?&?).
-    by constructor; apply cmra_op_div.
   - intros n r r1 r2 (?&?&?) [???]; simpl in *.
     destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
       (cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),