diff --git a/algebra/agree.v b/algebra/agree.v
index cb82e126cb986a5d286104c181e2e8939955c457..ecc0bd9758028e8fab806b46a3e96f514da1e2b5 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -49,7 +49,7 @@ Proof.
   - intros n c; apply and_wlog_r; intros;
       symmetry; apply (chain_cauchy c); naive_solver.
 Qed.
-Canonical Structure agreeC := CofeT agree_cofe_mixin.
+Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
 
 Lemma agree_car_ne n (x y : agree A) : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n.
 Proof. by intros [??] Hxy; apply Hxy. Qed.
@@ -116,7 +116,8 @@ Proof.
     + by rewrite agree_idemp.
     + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
 Qed.
-Canonical Structure agreeR : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin.
+Canonical Structure agreeR : cmraT :=
+  CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
 
 Global Instance agree_persistent (x : agree A) : Persistent x.
 Proof. done. Qed.
diff --git a/algebra/auth.v b/algebra/auth.v
index 5a103b2313559d0ca2d81a8acfdda368e813a045..a1ffd49f36b4c031b921bda0bbc44363d40d54ee 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -51,7 +51,7 @@ Proof.
   - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
     apply (conv_compl n (chain_map own c)).
 Qed.
-Canonical Structure authC := CofeT auth_cofe_mixin.
+Canonical Structure authC := CofeT (auth A) auth_cofe_mixin.
 
 Global Instance Auth_timeless a b :
   Timeless a → Timeless b → Timeless (Auth a b).
@@ -128,7 +128,8 @@ Proof.
       as (b&?&?&?); auto using own_validN.
     by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
 Qed.
-Canonical Structure authR : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
+Canonical Structure authR : cmraT :=
+  CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
 Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
 Proof.
   split; first apply _.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index fadeb8576a1710e662d3903838c4c1f2981e6d71..e9cc36887737969989d254fcbc31ca71444fa04a 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -62,7 +62,7 @@ Structure cmraT := CMRAT {
   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.
@@ -75,7 +75,7 @@ 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.
-Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
+Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
 (** Lifting properties from the mixin *)
@@ -474,14 +474,14 @@ End cmra_transport.
 
 (** * Instances *)
 (** ** Discrete CMRA *)
-Class RA A `{Equiv A, Core A, Op A, Valid A} := {
+Record RAMixin 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_core_ne : Proper ((≡) ==> (≡)) core;
+  ra_validN_ne : Proper ((≡) ==> impl) valid;
   (* monoid *)
-  ra_assoc :> Assoc (≡) (⋅);
-  ra_comm :> Comm (≡) (⋅);
+  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;
@@ -489,36 +489,41 @@ Class RA A `{Equiv A, Core A, Op A, Valid A} := {
 }.
 
 Section discrete.
-  Context {A : cofeT} `{Discrete A}.
-  Context `{Core A, Op A, Valid A} (ra : RA A).
+  Context `{Equiv A, Core A, Op A, Valid A, @Equivalence A (≡)}.
+  Context (ra_mix : RAMixin A).
+  Existing Instances discrete_dist discrete_compl.
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
   Proof.
-    destruct ra; split; unfold Proper, respectful, includedN;
-      try setoid_rewrite <-(timeless_iff _ _); try done.
+    destruct ra_mix; split; try done.
     - intros x; split; first done. by move=> /(_ 0).
-    - intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
-      apply (timeless _), dist_le with n; auto with lia.
+    - intros n x y1 y2 ??; by exists (y1,y2).
   Qed.
-  Definition discreteR : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
-  Global Instance discrete_cmra_discrete : CMRADiscrete discreteR.
-  Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
 End discrete.
 
+Notation discreteR A ra_mix :=
+  (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
+Notation discreteLeibnizR A ra_mix :=
+  (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).
+
+Global Instance discrete_cmra_discrete `{Equiv A, Core A, Op A, Valid A,
+  @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
+Proof. split. apply _. done. Qed.
+
 (** ** CMRA for the unit type *)
 Section unit.
   Instance unit_valid : Valid () := λ x, True.
+  Instance unit_validN : ValidN () := λ n x, True.
   Instance unit_core : Core () := λ x, x.
   Instance unit_op : Op () := λ x y, ().
   Global Instance unit_empty : Empty () := ().
-  Definition unit_ra : RA ().
-  Proof. by split. Qed.
-  Canonical Structure unitR : cmraT :=
-    Eval cbv [unitC discreteR cofe_car] in discreteR unit_ra.
+  Definition unit_cmra_mixin : CMRAMixin ().
+  Proof. by split; last exists ((),()). Qed.
+  Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
   Global Instance unit_cmra_unit : CMRAUnit unitR.
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
-  Proof. by apply discrete_cmra_discrete. Qed.
+  Proof. done. Qed.
   Global Instance unit_persistent (x : ()) : Persistent x.
   Proof. done. Qed.
 End unit.
@@ -563,7 +568,8 @@ Section prod.
       destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
       by exists ((z1.1,z2.1),(z1.2,z2.2)).
   Qed.
-  Canonical Structure prodR : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
+  Canonical Structure prodR : cmraT :=
+    CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
   Global Instance prod_cmra_unit `{Empty A, Empty B} :
     CMRAUnit A → CMRAUnit B → CMRAUnit prodR.
   Proof.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 301e0399659231d6c56e09a6e6efd8d55dc6365c..c3cefe2fda4212b930c772f78146a9dbd1b8a814 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -65,7 +65,7 @@ Structure cofeT := CofeT {
   cofe_compl : Compl cofe_car;
   cofe_mixin : CofeMixin cofe_car
 }.
-Arguments CofeT {_ _ _ _} _.
+Arguments CofeT _ {_ _ _} _.
 Add Printing Constructor cofeT.
 Existing Instances cofe_equiv cofe_dist cofe_compl.
 Arguments cofe_car : simpl never.
@@ -239,7 +239,7 @@ Section cofe_mor.
     - intros n c x; simpl.
       by rewrite (conv_compl n (fun_chain c x)) /=.
   Qed.
-  Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
+  Canonical Structure cofe_mor : cofeT := CofeT (cofeMor A B) cofe_mor_cofe_mixin.
 
   Global Instance cofe_mor_car_ne n :
     Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
@@ -291,7 +291,7 @@ Section unit.
   Instance unit_compl : Compl unit := λ _, ().
   Definition unit_cofe_mixin : CofeMixin unit.
   Proof. by repeat split; try exists 0. Qed.
-  Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
+  Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin.
   Global Instance unit_discrete_cofe : Discrete unitC.
   Proof. done. Qed.
 End unit.
@@ -317,7 +317,7 @@ Section product.
     - intros n c; split. apply (conv_compl n (chain_map fst c)).
       apply (conv_compl n (chain_map snd c)).
   Qed.
-  Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
+  Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
   Global Instance pair_timeless (x : A) (y : B) :
     Timeless x → Timeless y → Timeless (x,y).
   Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
@@ -436,15 +436,16 @@ Section discrete_cofe.
     - intros n c. rewrite /compl /discrete_compl /=;
       symmetry; apply (chain_cauchy c 0 n). omega.
   Qed.
-  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
-  Global Instance discrete_discrete_cofe : Discrete discreteC.
-  Proof. by intros x y. Qed.
 End discrete_cofe.
-Arguments discreteC _ {_ _}.
 
-Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
-Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
-Proof. by intros A x y. Qed.
+Notation discreteC A := (CofeT A discrete_cofe_mixin).
+Notation leibnizC A := (CofeT A (@discrete_cofe_mixin _ equivL _)).
+
+Instance discrete_discrete_cofe `{Equiv A, @Equivalence A (≡)} :
+  Discrete (discreteC A).
+Proof. by intros x y. Qed.
+Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
+Proof. by intros x y. Qed.
 
 Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
@@ -478,7 +479,7 @@ Section later.
     - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
     - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
   Qed.
-  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
+  Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin.
   Global Instance Next_contractive : Contractive (@Next A).
   Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 280dce025a9e92c1d4eb88622ad4ab1bcc97d016..515028163eaa79d7aa529cfeb42c6c6b8e0ffe08 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -71,7 +71,7 @@ Proof.
   - intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
     apply (chain_cauchy c); lia.
 Qed.
-Definition T : cofeT := CofeT tower_cofe_mixin.
+Definition T : cofeT := CofeT tower tower_cofe_mixin.
 
 Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
   match i with 0 => cid | S i => f (i + k) â—Ž ff i end.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 2eeaeaa5185c79c054ad4507ea06d575b5e2e96f..07352633a70f500e7d48caf421a33381fe4d97b4 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -28,7 +28,7 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
   end.
 Instance dec_agree_core : Core (dec_agree A) := id.
 
-Definition dec_agree_ra : RA (dec_agree A).
+Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
 Proof.
   split.
   - apply _.
@@ -42,7 +42,8 @@ Proof.
   - by intros [?|] [?|] ?.
 Qed.
 
-Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
+Canonical Structure dec_agreeR : cmraT :=
+  discreteR (dec_agree A) dec_agree_ra_mixin.
 
 (* Some properties of this CMRA *)
 Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
diff --git a/algebra/dra.v b/algebra/dra.v
index b2a0439d0b948ea68d610656da4094f6833fe2f7..6d2e9c893d5213475856f921e0a61b39b42259d2 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -1,53 +1,112 @@
 From iris.algebra Require Export cmra.
 
-(** From disjoint pcm *)
-Record validity {A} (P : A → Prop) : Type := Validity {
-  validity_car : A;
-  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 {_ _} _.
-
-Definition to_validity {A} {P : A → Prop} (x : A) : validity P :=
-  Validity x (P x) id.
-
-Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A} := {
+Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid 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);
+  mixin_dra_equivalence : Equivalence ((≡) : relation A);
+  mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
+  mixin_dra_core_proper : Proper ((≡) ==> (≡)) core;
+  mixin_dra_valid_proper : Proper ((≡) ==> impl) valid;
+  mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x);
   (* validity *)
-  dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
-  dra_core_valid x : ✓ x → ✓ core x;
+  mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
+  mixin_dra_core_valid x : ✓ x → ✓ core x;
   (* monoid *)
-  dra_assoc :> Assoc (≡) (⋅);
-  dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
-  dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
-  dra_symmetric :> Symmetric (@disjoint A _);
-  dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
-  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 : 
+  mixin_dra_assoc : Assoc (≡) (⋅);
+  mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
+  mixin_dra_disjoint_move_l x y z :
+    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
+  mixin_dra_symmetric : Symmetric (@disjoint A _);
+  mixin_dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
+  mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
+  mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
+  mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
+  mixin_dra_core_preserving x y : 
     ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
 }.
+Structure draT := DRAT {
+  dra_car :> Type;
+  dra_equiv : Equiv dra_car;
+  dra_core : Core dra_car;
+  dra_disjoint : Disjoint dra_car;
+  dra_op : Op dra_car;
+  dra_valid : Valid dra_car;
+  dra_mixin : DRAMixin dra_car
+}.
+Arguments DRAT _ {_ _ _ _ _} _.
+Arguments dra_car : simpl never.
+Arguments dra_equiv : simpl never.
+Arguments dra_core : simpl never.
+Arguments dra_disjoint : simpl never.
+Arguments dra_op : simpl never.
+Arguments dra_valid : simpl never.
+Arguments dra_mixin : simpl never.
+Add Printing Constructor draT.
+Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
 
+(** Lifting properties from the mixin *)
+Section dra_mixin.
+  Context {A : draT}.
+  Implicit Types x y : A.
+  Global Instance dra_equivalence : Equivalence ((≡) : relation A).
+  Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
+  Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
+  Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
+  Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
+  Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
+  Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _).
+  Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
+  Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x).
+  Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
+  Lemma dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y).
+  Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
+  Lemma dra_core_valid x : ✓ x → ✓ core x.
+  Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
+  Global Instance dra_assoc : Assoc (≡) (@op A _).
+  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
+  Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z.
+  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
+  Lemma dra_disjoint_move_l x y z :
+    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z.
+  Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
+  Global Instance  dra_symmetric : Symmetric (@disjoint A _).
+  Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
+  Lemma dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x.
+  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
+  Lemma dra_core_disjoint_l x : ✓ x → core x ⊥ x.
+  Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
+  Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x.
+  Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
+  Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
+  Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
+  Lemma dra_core_preserving x y : 
+    ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
+  Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
+End dra_mixin.
+
+Record validity (A : draT) := Validity {
+  validity_car : A;
+  validity_is_valid : Prop;
+  validity_prf : validity_is_valid → valid validity_car
+}.
+Add Printing Constructor validity.
+Arguments Validity {_} _ _ _.
+Arguments validity_car {_} _.
+Arguments validity_is_valid {_} _.
+
+Definition to_validity {A : draT} (x : A) : validity A :=
+  Validity x (valid x) id.
+
+(* The actual construction *)
 Section dra.
-Context A `{DRA A}.
+Context (A : draT).
+Implicit Types a b : A.
+Implicit Types x y z : validity A.
 Arguments valid _ _ !_ /.
-Hint Immediate dra_op_proper : typeclass_instances.
-
-Notation T := (validity (valid : A → Prop)).
 
-Instance validity_valid : Valid T := validity_is_valid.
-Instance validity_equiv : Equiv T := λ x y,
+Instance validity_valid : Valid (validity A) := validity_is_valid.
+Instance validity_equiv : Equiv (validity A) := λ x y,
   (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
-Instance validity_equivalence : Equivalence ((≡) : relation T).
+Instance validity_equivalence : Equivalence (@equiv (validity A) _).
 Proof.
   split; unfold equiv, validity_equiv.
   - by intros [x px ?]; simpl.
@@ -55,40 +114,43 @@ Proof.
   - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
     split; [|intros; trans y]; tauto.
 Qed.
+Canonical Structure validityC : cofeT := discreteC (validity A).
+
 Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
-Proof. by split; apply dra_valid_proper. Qed.
-Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
+Proof. by split; apply: dra_valid_proper. Qed.
+Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
 Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
-Instance: Proper ((≡) ==> (≡) ==> iff) (⊥).
+Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
 Proof.
   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 : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y.
-Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z.
+
+Lemma dra_disjoint_rl a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⊥ b.
+Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
+Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ⊥ b → a ⋅ b ⊥ c → b ⊥ c.
 Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_move_r x y z :
-  ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z.
+Lemma dra_disjoint_move_r a b c :
+  ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⋅ b ⊥ c.
 Proof.
   intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
   apply dra_disjoint_move_l; auto; by rewrite dra_comm.
 Qed.
 Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
 
-Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z.
+Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
 Hint Resolve validity_valid_car_valid.
-Program Instance validity_core : Core T := λ x,
+Program Instance validity_core : Core (validity A) := λ x,
   Validity (core (validity_car x)) (✓ x) _.
-Solve Obligations with naive_solver auto using dra_core_valid.
-Program Instance validity_op : Op T := λ x y,
+Solve Obligations with naive_solver eauto using dra_core_valid.
+Program Instance validity_op : Op (validity A) := λ 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.
+Solve Obligations with naive_solver eauto using dra_op_valid.
 
-Definition validity_ra : RA (discreteC T).
+Definition validity_ra_mixin : RAMixin (validity A).
 Proof.
   split.
   - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
@@ -98,7 +160,7 @@ Proof.
   - intros ?? [??]; naive_solver.
   - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
       [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |by intros; rewrite assoc].
+      |intros; by rewrite assoc].
   - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
   - intros [x px ?]; split;
       naive_solver eauto using dra_core_l, dra_core_disjoint_l.
@@ -111,21 +173,20 @@ Proof.
     + intros. rewrite Hy //. tauto.
   - by intros [x px ?] [y py ?] (?&?&?).
 Qed.
-Definition validityR : cmraT := discreteR validity_ra.
-Instance validity_cmra_discrete :
-  CMRADiscrete validityR := discrete_cmra_discrete _.
+Canonical Structure validityR : cmraT :=
+  discreteR (validity A) validity_ra_mixin.
 
-Lemma validity_update (x y : validityR) :
-  (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y.
+Lemma validity_update x y :
+  (∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
 Proof.
   intros Hxy; apply cmra_discrete_update=> z [?[??]].
   split_and!; try eapply Hxy; eauto.
 Qed.
 
-Lemma to_validity_op (x y : A) :
-  (✓ (x ⋅ y) → ✓ x ∧ ✓ y ∧ x ⊥ y) →
-  to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
-Proof. split; naive_solver auto using dra_op_valid. Qed.
+Lemma to_validity_op a b :
+  (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ⊥ b) →
+  to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b.
+Proof. split; naive_solver eauto using dra_op_valid. Qed.
 
 (* TODO: This has to be proven again. *)
 (*
diff --git a/algebra/excl.v b/algebra/excl.v
index bca3134c9eb555876245fe10760c990aa2212e89..356f06d84348acb13e6f5e45b5b819f3504de73d 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -59,7 +59,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
     rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
+Canonical Structure exclC : cofeT := CofeT (excl A) excl_cofe_mixin.
 Global Instance excl_discrete : Discrete A → Discrete exclC.
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
 Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
@@ -107,7 +107,8 @@ Proof.
       | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
       end; destruct y1, y2; inversion_clear Hx; repeat constructor.
 Qed.
-Canonical Structure exclR : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
+Canonical Structure exclR : cmraT :=
+  CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
 Global Instance excl_cmra_unit : CMRAUnit exclR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
diff --git a/algebra/frac.v b/algebra/frac.v
index f1ec2c20e0cd8a15fe32e644291bf9cbfe2b7b79..ede01ba395eb8d1a7a6f5ae918856cab5b9d99c0 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -72,7 +72,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first lia;
        constructor; destruct (c 0); simplify_eq/=.
 Qed.
-Canonical Structure fracC : cofeT := CofeT frac_cofe_mixin.
+Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin.
 Global Instance frac_discrete : Discrete A → Discrete fracC.
 Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
 Global Instance frac_leibniz : LeibnizEquiv A → LeibnizEquiv (frac A).
@@ -157,7 +157,8 @@ Proof.
     + exists (∅, Frac q a); inversion_clear Hx'; by repeat constructor.
     + exfalso; inversion_clear Hx'.
 Qed.
-Canonical Structure fracR : cmraT := CMRAT frac_cofe_mixin frac_cmra_mixin.
+Canonical Structure fracR : cmraT :=
+  CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
 Global Instance frac_cmra_unit : CMRAUnit fracR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index e85f39dd7b7cbae9b0a36e94e778d167b37fb85c..30d2f51aa3959b88526ebc3f03f0743fe6ba158a 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -28,7 +28,7 @@ Proof.
     feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia.
     by rewrite conv_compl /=; apply reflexive_eq.
 Qed.
-Canonical Structure gmapC : cofeT := CofeT gmap_cofe_mixin.
+Canonical Structure gmapC : cofeT := CofeT (gmap K A) gmap_cofe_mixin.
 Global Instance gmap_discrete : Discrete A → Discrete gmapC.
 Proof. intros ? m m' ? i. by apply (timeless _). Qed.
 (* why doesn't this go automatic? *)
@@ -152,7 +152,8 @@ Proof.
       pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
       by symmetry; apply option_op_positive_dist_r with (m1 !! i).
 Qed.
-Canonical Structure gmapR : cmraT := CMRAT gmap_cofe_mixin gmap_cmra_mixin.
+Canonical Structure gmapR : cmraT :=
+  CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
 Global Instance gmap_cmra_unit : CMRAUnit gmapR.
 Proof.
   split.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index b9dd41fad31f1f89d01d6a21b123ca6783cfe778..3a3883e935eb930556a6a68c3a38c9f8e1accda4 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -42,7 +42,7 @@ Section iprod_cofe.
       rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
       apply (chain_cauchy c); lia.
   Qed.
-  Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
+  Canonical Structure iprodC : cofeT := CofeT (iprod B) iprod_cofe_mixin.
 
   (** Properties of empty *)
   Section empty.
@@ -153,7 +153,8 @@ Section iprod_cmra.
       exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
       split_and?; intros x; apply (proj2_sig (g x)).
   Qed.
-  Canonical Structure iprodR : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin.
+  Canonical Structure iprodR : cmraT :=
+    CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.
   Global Instance iprod_cmra_unit `{∀ x, Empty (B x)} :
     (∀ x, CMRAUnit (B x)) → CMRAUnit iprodR.
   Proof.
diff --git a/algebra/list.v b/algebra/list.v
index 058f2803eeb75c075ca440ab2ad9fcd7049d65b2..581ba0665dead2dc3b7213f6db4e1d5ca32f0f23 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -68,7 +68,7 @@ Proof.
     rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
     by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
 Qed.
-Canonical Structure listC := CofeT list_cofe_mixin.
+Canonical Structure listC := CofeT (list A) list_cofe_mixin.
 Global Instance list_discrete : Discrete A → Discrete listC.
 Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
 
@@ -196,7 +196,8 @@ Section cmra.
           [inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
         exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
   Qed.
-  Canonical Structure listR : cmraT := CMRAT list_cofe_mixin list_cmra_mixin.
+  Canonical Structure listR : cmraT :=
+    CMRAT (list A) list_cofe_mixin list_cmra_mixin.
 
   Global Instance empty_list : Empty (list A) := [].
   Global Instance list_cmra_unit : CMRAUnit listR.
diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 18db970bb868e745a38ff20ba404629ff2959f54..72588fd9c074ab1e272e4cd433cf1df9e201f1e0 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -65,7 +65,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
     rewrite (conv_compl n (one_shot_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure one_shotC : cofeT := CofeT one_shot_cofe_mixin.
+Canonical Structure one_shotC : cofeT := CofeT (one_shot A) one_shot_cofe_mixin.
 Global Instance one_shot_discrete : Discrete A → Discrete one_shotC.
 Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
 Global Instance one_shot_leibniz : LeibnizEquiv A → LeibnizEquiv (one_shot A).
@@ -186,7 +186,8 @@ Proof.
        * exists (Shot a, ∅). inversion_clear Hx'. by repeat constructor.
        * exists (∅, Shot a). inversion_clear Hx'. by repeat constructor.
 Qed.
-Canonical Structure one_shotR : cmraT := CMRAT one_shot_cofe_mixin one_shot_cmra_mixin.
+Canonical Structure one_shotR : cmraT :=
+  CMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin.
 Global Instance one_shot_cmra_unit : CMRAUnit one_shotR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance one_shot_cmra_discrete : CMRADiscrete A → CMRADiscrete one_shotR.
diff --git a/algebra/option.v b/algebra/option.v
index 86007543ad3f1fcac064457d50d3c7e6f73c784b..c7e4b1bd8793b7811f887ebd1dbb75b1582e52b0 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -34,7 +34,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
     rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure optionC := CofeT option_cofe_mixin.
+Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
 Global Instance option_discrete : Discrete A → Discrete optionC.
 Proof. destruct 2; constructor; by apply (timeless _). Qed.
 
@@ -110,7 +110,8 @@ Proof.
     + by exists (None,Some x); inversion Hx'; repeat constructor.
     + exists (None,None); repeat constructor.
 Qed.
-Canonical Structure optionR := CMRAT option_cofe_mixin option_cmra_mixin.
+Canonical Structure optionR :=
+  CMRAT (option A) option_cofe_mixin option_cmra_mixin.
 Global Instance option_cmra_unit : CMRAUnit optionR.
 Proof. split. done. by intros []. by inversion_clear 1. Qed.
 Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
diff --git a/algebra/sts.v b/algebra/sts.v
index 156becc0b5fde35ae3802d32f3d0d7ad81171921..7950bf8cd6d86e902b095eadae399e52c6c64539 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -155,15 +155,6 @@ Proof. move=> ?? s [s' [? ?]]. eauto using closed_steps. Qed.
 End sts.
 
 Notation steps := (rtc step).
-End sts.
-
-Notation stsT := sts.stsT.
-Notation STS := sts.STS.
-
-(** * STSs form a disjoint RA *)
-(* This module should never be imported, uses the module [sts] below. *)
-Module sts_dra.
-Import sts.
 
 (* The type of bounds we can give to the state of an STS. This is the type
    that we equip with an RA structure. *)
@@ -172,22 +163,28 @@ Inductive car (sts : stsT) :=
   | frag : set (state sts) → set (token sts ) → car sts.
 Arguments auth {_} _ _.
 Arguments frag {_} _ _.
+End sts.
 
+Notation stsT := sts.stsT.
+Notation STS := sts.STS.
+
+(** * STSs form a disjoint RA *)
 Section sts_dra.
-Context {sts : stsT}.
+Context (sts : stsT).
+Import sts.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
 
 Inductive sts_equiv : Equiv (car sts) :=
   | 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.
-Global Instance sts_valid : Valid (car sts) := λ x,
+Existing Instance sts_equiv.
+Instance sts_valid : Valid (car sts) := λ x,
   match x with
   | auth s T => tok s ⊥ T
   | frag S' T => closed S' T ∧ S' ≢ ∅
   end.
-Global Instance sts_core : Core (car sts) := λ x,
+Instance sts_core : Core (car sts) := λ x,
   match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
   | auth s _  => frag (up s ∅) ∅
@@ -197,8 +194,8 @@ Inductive sts_disjoint : Disjoint (car sts) :=
      S1 ∩ S2 ≢ ∅ → T1 ⊥ T2 → frag S1 T1 ⊥ frag S2 T2
   | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ⊥ T2 → auth s T1 ⊥ frag S T2
   | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ⊥ T2 → frag S T1 ⊥ auth s T2.
-Global Existing Instance sts_disjoint.
-Global Instance sts_op : Op (car sts) := λ x1 x2,
+Existing Instance sts_disjoint.
+Instance sts_op : Op (car sts) := λ x1 x2,
   match x1, x2 with
   | frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
   | auth s T1, frag _ T2 => auth s (T1 ∪ T2)
@@ -212,14 +209,19 @@ Hint Extern 50 (_ ∈ _) => set_solver : sts.
 Hint Extern 50 (_ ⊆ _) => set_solver : sts.
 Hint Extern 50 (_ ⊥ _) => set_solver : sts.
 
-Global Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
+Global Instance auth_proper s : Proper ((≡) ==> (≡)) (@auth sts s).
+Proof. by constructor. Qed.
+Global Instance frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@frag sts).
+Proof. by constructor. Qed.
+
+Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
 Proof.
   split.
   - by intros []; constructor.
   - by destruct 1; constructor.
   - destruct 1; inversion_clear 1; constructor; etrans; eauto.
 Qed.
-Global Instance sts_dra : DRA (car sts).
+Lemma sts_dra_mixin : DRAMixin (car sts).
 Proof.
   split.
   - apply _.
@@ -254,19 +256,20 @@ Proof.
            unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
         end; auto with sts.
 Qed.
-Canonical Structure R : cmraT := validityR (car sts).
-End sts_dra. End sts_dra.
+Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin.
+End sts_dra.
 
 (** * The STS Resource Algebra *)
 (** Finally, the general theory of STS that should be used by users *)
-Notation stsR := (@sts_dra.R).
+Notation stsC sts := (validityC (stsDR sts)).
+Notation stsR sts := (validityR (stsDR sts)).
 
 Section sts_definitions.
   Context {sts : stsT}.
   Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
-    to_validity (sts_dra.auth s T).
+    to_validity (sts.auth s T).
   Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
-    to_validity (sts_dra.frag S T).
+    to_validity (sts.frag S T).
   Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
     sts_frag (sts.up s T) T.
 End sts_definitions.
@@ -280,23 +283,15 @@ Context {sts : stsT}.
 Implicit Types s : state sts.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
-
-Global Instance sts_cmra_discrete : CMRADiscrete (stsR sts).
-Proof. apply validity_cmra_discrete. Qed.
+Arguments dra_valid _ !_/.
 
 (** Setoids *)
 Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
-Proof. (* this proof is horrible *)
-  intros T1 T2 HT. rewrite /sts_auth.
-  by eapply to_validity_proper; try apply _; constructor.
-Qed.
+Proof. solve_proper. Qed.
 Global Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag sts).
-Proof.
-  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
-  by eapply to_validity_proper; try apply _; constructor.
-Qed.
+Proof. solve_proper. Qed.
 Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
-Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
+Proof. solve_proper. Qed.
 
 (** Validity *)
 Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ⊥ T.
@@ -334,11 +329,8 @@ Lemma sts_op_frag S1 S2 T1 T2 :
   T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 →
   sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
 Proof.
-  intros HT HS1 HS2. rewrite /sts_frag.
-  (* FIXME why does rewrite not work?? *)
-  etrans; last eapply to_validity_op; first done; [].
-  move=>/=[??]. split_and!; [auto; set_solver..|].
-  constructor; done.
+  intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.
+  move=>/=[??]. split_and!; [auto; set_solver..|by constructor].
 Qed.
 
 (** Frame preserving updates *)
@@ -367,9 +359,8 @@ Proof.
   rewrite <-HT. eapply up_subseteq; done.
 Qed.
 
-Lemma up_set_intersection S1 Sf Tf :
-  closed Sf Tf → 
-  S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
+Lemma sts_up_set_intersection S1 Sf Tf :
+  closed Sf Tf → S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
 Proof.
   intros Hclf. apply (anti_symm (⊆)).
   + move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
diff --git a/algebra/upred.v b/algebra/upred.v
index 2a974d2be07004f07f8a60ca36320dff72fb9881..0e31b28cfb31a275b85ee0c26303e96e6f5e370e 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -47,7 +47,7 @@ Section cofe.
     - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
     - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
   Qed.
-  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
+  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
 End cofe.
 Arguments uPredC : clear implicits.
 
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 7d77145210b89861770dba0729156bfab60e2ef1..c076860352fcdd03e472da4db6074ce68efe4816 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -66,7 +66,7 @@ Proof.
     + apply (conv_compl n (chain_map pst c)).
     + apply (conv_compl n (chain_map gst c)).
 Qed.
-Canonical Structure resC : cofeT := CofeT res_cofe_mixin.
+Canonical Structure resC : cofeT := CofeT (res Λ A M) res_cofe_mixin.
 Global Instance res_timeless r :
   Timeless (wld r) → Timeless (gst r) → Timeless r.
 Proof. by destruct 3; constructor; try apply: timeless. Qed.
@@ -118,7 +118,8 @@ Proof.
       (cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
     by exists (Res w σ m, Res w' σ' m').
 Qed.
-Canonical Structure resR : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
+Canonical Structure resR : cmraT :=
+  CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
 Global Instance res_cmra_unit `{CMRAUnit M} : CMRAUnit resR.
 Proof.
   split.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 8ca7e243b1bc021c8c09f0447a0bcd2d71d861f1..22fe7d867ce663368daba66129693d391444290a 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -52,8 +52,7 @@ Proof.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
     + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
       iPvs (own_update with "Hγ") as "Hγ".
-      { (* FIXME: canonical structures are not working *)
-        by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)). }
+      { by apply (one_shot_update_shoot (DecAgree n)). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
     + wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
   - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".