diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index c60bfe6c2828dc2703e50f3e2538a458bab71b8e..c5f6a696ec150fc25c7023c12d3cccb296984c8f 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -35,92 +35,101 @@ Notation "x ≼{ n } y" := (includedN n x y)
 Instance: Params (@includedN) 4.
 Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
-Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
+Record cmra_laws A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
   (* setoids *)
-  mixin_cmra_op_ne (x : A) : NonExpansive (op x);
-  mixin_cmra_pcore_ne n x y cx :
+  law_cmra_op_ne (x : A) : NonExpansive (op x);
+  law_cmra_pcore_ne n x y cx :
     x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
-  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
+  law_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
   (* valid *)
-  mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
-  mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
+  law_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
+  law_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
   (* monoid *)
-  mixin_cmra_assoc : Assoc (≡) (⋅);
-  mixin_cmra_comm : Comm (≡) (⋅);
-  mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
-  mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
-  mixin_cmra_pcore_mono x y cx :
+  law_cmra_assoc : Assoc (≡) (⋅);
+  law_cmra_comm : Comm (≡) (⋅);
+  law_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x;
+  law_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx;
+  law_cmra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
-  mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
-  mixin_cmra_extend n x y1 y2 :
+  law_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
+  law_cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2
 }.
 
-(** Bundeled version *)
-Structure cmraT := CMRAT' {
-  cmra_car :> Type;
-  cmra_equiv : Equiv cmra_car;
-  cmra_dist : Dist cmra_car;
-  cmra_pcore : PCore cmra_car;
-  cmra_op : Op cmra_car;
-  cmra_valid : Valid cmra_car;
-  cmra_validN : ValidN cmra_car;
-  cmra_ofe_mixin : OfeMixin cmra_car;
-  cmra_mixin : CMRAMixin cmra_car;
-  _ : Type
+Record cmra_mixin (A : Type) := CMRAMixin {
+  cmra_mixin_equiv : Equiv A;
+  cmra_mixin_dist : Dist A;
+  cmra_mixin_pcore : PCore A;
+  cmra_mixin_op : Op A;
+  cmra_mixin_valid : Valid A;
+  cmra_mixin_validN : ValidN A;
+  cmra_mixin_ofe_laws_of : ofe_laws A;
+  cmra_mixin_laws_of : cmra_laws A;
 }.
-Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
-Notation CMRAT A m m' := (CMRAT' A m m' A).
+Arguments CMRAMixin {_ _ _ _ _ _ _} _ _.
+
+(** Bundeled version *)
+Structure cmraT := CMRAT' { cmra_car :> Type; _ : cmra_mixin cmra_car; _ : Type }.
+Notation CMRAT A m := (CMRAT' A m A).
+Add Printing Constructor cmraT.
 Arguments cmra_car : simpl never.
-Arguments cmra_equiv : simpl never.
-Arguments cmra_dist : simpl never.
+
+Definition cmra_mixin_of (A : cmraT) : cmra_mixin A := let 'CMRAT' _ m _ := A in m.
+Arguments cmra_mixin_of : simpl never.
+
+Definition cmra_pcore {A : cmraT} : PCore A := cmra_mixin_pcore _ (cmra_mixin_of A).
 Arguments cmra_pcore : simpl never.
-Arguments cmra_op : simpl never.
-Arguments cmra_valid : simpl never.
-Arguments cmra_validN : simpl never.
-Arguments cmra_ofe_mixin : simpl never.
-Arguments cmra_mixin : simpl never.
-Add Printing Constructor cmraT.
 Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
+Definition cmra_op {A : cmraT} : Op A := cmra_mixin_op _ (cmra_mixin_of A).
+Arguments cmra_op : simpl never.
 Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
+Definition cmra_valid {A : cmraT} : Valid A := cmra_mixin_valid _ (cmra_mixin_of A).
+Arguments cmra_valid : simpl never.
 Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
+Definition cmra_validN {A : cmraT} : ValidN A := cmra_mixin_validN _ (cmra_mixin_of A).
+Arguments cmra_validN : simpl never.
 Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
-Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
+
+Definition cmra_ofe_mixin_of {A} (m : cmra_mixin A) : ofe_mixin A :=
+  OfeMixin (cmra_mixin_ofe_laws_of _ m).
+Coercion cmra_ofeC (A : cmraT) : ofeT :=
+  OfeT A (cmra_ofe_mixin_of (cmra_mixin_of A)).
 Canonical Structure cmra_ofeC.
 
 (** Lifting properties from the mixin *)
 Section cmra_mixin.
   Context {A : cmraT}.
   Implicit Types x y : A.
+  Local Coercion cmra_mixin_of : cmraT >-> cmra_mixin.
   Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
-  Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_op_ne _ (cmra_mixin_laws_of _ A)). Qed.
   Lemma cmra_pcore_ne n x y cx :
     x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy.
-  Proof. apply (mixin_cmra_pcore_ne _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_pcore_ne _ (cmra_mixin_laws_of _ 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.
+  Proof. apply (law_cmra_validN_ne _ (cmra_mixin_laws_of _ A)). Qed.
   Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
-  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_valid_validN _ (cmra_mixin_laws_of _ A)). Qed.
   Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
-  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_validN_S _ (cmra_mixin_laws_of _ A)). Qed.
   Global Instance cmra_assoc : Assoc (≡) (@op A _).
-  Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_assoc _ (cmra_mixin_laws_of _ A)). Qed.
   Global Instance cmra_comm : Comm (≡) (@op A _).
-  Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_comm _ (cmra_mixin_laws_of _ A)). Qed.
   Lemma cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x.
-  Proof. apply (mixin_cmra_pcore_l _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_pcore_l _ (cmra_mixin_laws_of _ A)). Qed.
   Lemma cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx.
-  Proof. apply (mixin_cmra_pcore_idemp _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_pcore_idemp _ (cmra_mixin_laws_of _ A)). Qed.
   Lemma cmra_pcore_mono x y cx :
     x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
-  Proof. apply (mixin_cmra_pcore_mono _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_pcore_mono _ (cmra_mixin_laws_of _ 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.
+  Proof. apply (law_cmra_validN_op_l _ (cmra_mixin_laws_of _ A)). Qed.
   Lemma cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2.
-  Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
+  Proof. apply (law_cmra_extend _ (cmra_mixin_laws_of _ A)). Qed.
 End cmra_mixin.
 
 Definition opM {A : cmraT} (x : A) (my : option A) :=
@@ -163,56 +172,66 @@ Arguments core' _ _ _ /.
 (** * CMRAs with a unit element *)
 (** We use the notation ∅ because for most instances (maps, sets, etc) the
 `empty' element is the unit. *)
-Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
+Record ucmra_laws A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
   mixin_ucmra_unit_valid : ✓ ∅;
   mixin_ucmra_unit_left_id : LeftId (≡) ∅ (⋅);
   mixin_ucmra_pcore_unit : pcore ∅ ≡ Some ∅
 }.
 
-Structure ucmraT := UCMRAT' {
-  ucmra_car :> Type;
-  ucmra_equiv : Equiv ucmra_car;
-  ucmra_dist : Dist ucmra_car;
-  ucmra_pcore : PCore ucmra_car;
-  ucmra_op : Op ucmra_car;
-  ucmra_valid : Valid ucmra_car;
-  ucmra_validN : ValidN ucmra_car;
-  ucmra_empty : Empty ucmra_car;
-  ucmra_ofe_mixin : OfeMixin ucmra_car;
-  ucmra_cmra_mixin : CMRAMixin ucmra_car;
-  ucmra_mixin : UCMRAMixin ucmra_car;
-  _ : Type;
+Record ucmra_mixin (A : Type) := UCMRAMixin {
+  ucmra_mixin_equiv : Equiv A;
+  ucmra_mixin_dist : Dist A;
+  ucmra_mixin_pcore : PCore A;
+  ucmra_mixin_op : Op A;
+  ucmra_mixin_valid : Valid A;
+  ucmra_mixin_validN : ValidN A;
+  ucmra_mixin_empty : Empty A;
+  ucmra_mixin_ofe_laws_of : ofe_laws A;
+  ucmra_mixin_cmra_laws_of : cmra_laws A;
+  ucmra_mixin_laws_of : ucmra_laws A;
 }.
-Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
-Notation UCMRAT A m m' m'' := (UCMRAT' A m m' m'' A).
-Arguments ucmra_car : simpl never.
-Arguments ucmra_equiv : simpl never.
-Arguments ucmra_dist : simpl never.
-Arguments ucmra_pcore : simpl never.
-Arguments ucmra_op : simpl never.
-Arguments ucmra_valid : simpl never.
-Arguments ucmra_validN : simpl never.
-Arguments ucmra_ofe_mixin : simpl never.
-Arguments ucmra_cmra_mixin : simpl never.
-Arguments ucmra_mixin : simpl never.
+Arguments UCMRAMixin {_ _ _ _ _ _ _ _} _ _ _.
+
+Structure ucmraT :=
+  UCMRAT' { ucmra_car :> Type; _ : ucmra_mixin ucmra_car; _ : Type }.
+Notation UCMRAT A m := (UCMRAT' A m A).
 Add Printing Constructor ucmraT.
+Arguments ucmra_car : simpl never.
+
+Definition ucmra_mixin_of (A : ucmraT) : ucmra_mixin A :=
+  let 'UCMRAT' _ m _ := A in m.
+Arguments ucmra_mixin_of : simpl never.
+
+Definition ucmra_empty {A : ucmraT} : Empty A :=
+  ucmra_mixin_empty _ (ucmra_mixin_of A).
+Arguments ucmra_empty : simpl never.
 Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
-Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
+
+Definition ucmra_ofe_mixin_of {A} (m : ucmra_mixin A) : ofe_mixin A :=
+  OfeMixin (ucmra_mixin_ofe_laws_of _ m).
+Definition ucmra_cmra_mixin_of {A} (m : ucmra_mixin A) : cmra_mixin A :=
+  CMRAMixin (ucmra_mixin_ofe_laws_of _ m) (ucmra_mixin_cmra_laws_of _ m).
+Arguments ucmra_ofe_mixin_of : simpl never.
+Arguments ucmra_cmra_mixin_of : simpl never.
+
+Coercion ucmra_ofeC (A : ucmraT) : ofeT :=
+  OfeT A (ucmra_ofe_mixin_of (ucmra_mixin_of A)).
 Canonical Structure ucmra_ofeC.
 Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
-  CMRAT A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
+  CMRAT A (ucmra_cmra_mixin_of (ucmra_mixin_of A)).
 Canonical Structure ucmra_cmraR.
 
 (** Lifting properties from the mixin *)
 Section ucmra_mixin.
   Context {A : ucmraT}.
   Implicit Types x y : A.
+  Local Coercion ucmra_mixin_of : ucmraT >-> ucmra_mixin.
   Lemma ucmra_unit_valid : ✓ (∅ : A).
-  Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
+  Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin_laws_of _ A)). Qed.
   Global Instance ucmra_unit_left_id : LeftId (≡) ∅ (@op A _).
-  Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
+  Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin_laws_of _ A)). Qed.
   Lemma ucmra_pcore_unit : pcore (∅:A) ≡ Some ∅.
-  Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
+  Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin_laws_of _ A)). Qed.
 End ucmra_mixin.
 
 (** * Discrete CMRAs *)
@@ -698,7 +717,7 @@ Section cmra_total.
   Context (extend : ∀ n (x y1 y2 : A),
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2).
-  Lemma cmra_total_mixin : CMRAMixin A.
+  Lemma cmra_total_laws : cmra_laws A.
   Proof using Type*.
     split; auto.
     - intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
@@ -850,7 +869,7 @@ End cmra_transport.
 
 (** * Instances *)
 (** ** Discrete CMRA *)
-Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
+Record ra_laws A `{Equiv A, PCore A, Op A, Valid A} := {
   (* setoids *)
   ra_op_proper (x : A) : Proper ((≡) ==> (≡)) (op x);
   ra_core_proper x y cx :
@@ -869,18 +888,19 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
 Section discrete.
   Local Set Default Proof Using "Type*".
   Context `{Equiv A, PCore A, Op A, Valid A, @Equivalence A (≡)}.
-  Context (ra_mix : RAMixin A).
+  Context (laws : ra_laws A).
   Existing Instances discrete_dist.
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
-  Definition discrete_cmra_mixin : CMRAMixin A.
+  Definition discrete_cmra_laws : cmra_laws A.
   Proof.
-    destruct ra_mix; split; try done.
+    destruct laws; split; try done.
     - intros x; split; first done. by move=> /(_ 0).
     - intros n x y1 y2 ??; by exists y1, y2.
   Qed.
 End discrete.
 
+(*
 Notation discreteR A ra_mix :=
   (CMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix)).
 Notation discreteUR A ra_mix ucmra_mix :=
@@ -889,7 +909,7 @@ Notation discreteUR A ra_mix ucmra_mix :=
 Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
   @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
 Proof. split. apply _. done. Qed.
-
+*)
 Section ra_total.
   Local Set Default Proof Using "Type*".
   Context A `{Equiv A, PCore A, Op A, Valid A}.
@@ -903,7 +923,7 @@ Section ra_total.
   Context (core_idemp : ∀ x : A, core (core x) ≡ core x).
   Context (core_mono : ∀ x y : A, x ≼ y → core x ≼ core y).
   Context (valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x).
-  Lemma ra_total_mixin : RAMixin A.
+  Lemma ra_total_laws : ra_laws A.
   Proof.
     split; auto.
     - intros x y ? Hcx%core_proper Hx; move: Hcx. rewrite /core /= Hx /=.
@@ -922,15 +942,17 @@ Section unit.
   Instance unit_validN : ValidN () := λ n x, True.
   Instance unit_pcore : PCore () := λ x, Some x.
   Instance unit_op : Op () := λ x y, ().
-  Lemma unit_cmra_mixin : CMRAMixin ().
-  Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
-  Canonical Structure unitR : cmraT := CMRAT () unit_ofe_mixin unit_cmra_mixin.
+  Lemma unit_cmra_laws : cmra_laws ().
+  Proof. apply discrete_cmra_laws, ra_total_laws; by eauto. Qed.
+  Definition unit_cmra_mixin := CMRAMixin unit_ofe_laws unit_cmra_laws.
+  Canonical Structure unitR : cmraT := CMRAT () unit_cmra_mixin.
 
   Instance unit_empty : Empty () := ().
-  Lemma unit_ucmra_mixin : UCMRAMixin ().
+  Lemma unit_ucmra_laws : ucmra_laws ().
   Proof. done. Qed.
-  Canonical Structure unitUR : ucmraT :=
-    UCMRAT () unit_ofe_mixin unit_cmra_mixin unit_ucmra_mixin.
+  Definition unit_ucmra_mixin :=
+    UCMRAMixin unit_ofe_laws unit_cmra_laws unit_ucmra_laws.
+  Canonical Structure unitUR : ucmraT := UCMRAT () unit_ucmra_mixin.
 
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
   Proof. done. Qed.
@@ -953,31 +975,35 @@ Section nat.
     - intros [z ->]; unfold op, nat_op; lia.
     - exists (y - x). by apply le_plus_minus.
   Qed.
-  Lemma nat_ra_mixin : RAMixin nat.
+  Lemma nat_ra_laws : ra_laws nat.
   Proof.
-    apply ra_total_mixin; try by eauto.
+    apply ra_total_laws; try by eauto.
     - solve_proper.
     - intros x y z. apply Nat.add_assoc.
     - intros x y. apply Nat.add_comm.
     - by exists 0.
   Qed.
+(*
+  Definition nat_cmra_mixin := CMRAMixin unit_ofe_laws unit_cmra_laws.
   Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
-
+*)
   Instance nat_empty : Empty nat := 0.
-  Lemma nat_ucmra_mixin : UCMRAMixin nat.
+  Lemma nat_ucmra_laws : ucmra_laws nat.
   Proof. split; apply _ || done. Qed.
+(*
   Canonical Structure natUR : ucmraT :=
     discreteUR nat nat_ra_mixin nat_ucmra_mixin.
 
   Global Instance nat_cmra_discrete : CMRADiscrete natR.
   Proof. constructor; apply _ || done. Qed.
-
   Global Instance nat_cancelable (x : nat) : Cancelable x.
   Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
+*)
 End nat.
 
 Definition mnat := nat.
 
+(*
 Section mnat.
   Instance mnat_valid : Valid mnat := λ x, True.
   Instance mnat_validN : ValidN mnat := λ n x, True.
@@ -1045,6 +1071,7 @@ Section positive.
     by apply leibniz_equiv.
   Qed.
 End positive.
+*)
 
 (** ** Product *)
 Section prod.
@@ -1082,7 +1109,7 @@ Section prod.
     intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
   Qed.
 
-  Definition prod_cmra_mixin : CMRAMixin (A * B).
+  Definition prod_cmra_laws : cmra_laws (A * B).
   Proof.
     split; try apply _.
     - by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
@@ -1111,8 +1138,8 @@ Section prod.
       destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
       by exists (z11,z21), (z12,z22).
   Qed.
-  Canonical Structure prodR :=
-    CMRAT (A * B) prod_ofe_mixin prod_cmra_mixin.
+  Definition prod_cmra_mixin := CMRAMixin prod_ofe_laws prod_cmra_laws.
+  Canonical Structure prodR := CMRAT (A * B) prod_cmra_mixin.
 
   Lemma pair_op (a a' : A) (b b' : B) : (a, b) â‹… (a', b') = (a â‹… a', b â‹… b').
   Proof. done. Qed.
@@ -1152,15 +1179,16 @@ Section prod_unit.
   Context {A B : ucmraT}.
 
   Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
-  Lemma prod_ucmra_mixin : UCMRAMixin (A * B).
+  Lemma prod_ucmra_laws : ucmra_laws (A * B).
   Proof.
     split.
     - split; apply ucmra_unit_valid.
     - by split; rewrite /=left_id.
     - rewrite prod_pcore_Some'; split; apply (persistent _).
   Qed.
-  Canonical Structure prodUR :=
-    UCMRAT (A * B) prod_ofe_mixin prod_cmra_mixin prod_ucmra_mixin.
+  Definition prod_ucmra_mixin :=
+    UCMRAMixin prod_ofe_laws prod_cmra_laws prod_ucmra_laws.
+  Canonical Structure prodUR := UCMRAT (A * B) prod_ucmra_mixin.
 
   Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
   Proof. by rewrite pair_op left_id right_id. Qed.
@@ -1263,9 +1291,9 @@ Section option.
       + exists (Some z); by constructor.
   Qed.
 
-  Lemma option_cmra_mixin : CMRAMixin (option A).
+  Lemma option_cmra_laws : cmra_laws (option A).
   Proof.
-    apply cmra_total_mixin.
+    apply cmra_total_laws.
     - eauto.
     - by intros [x|] n; destruct 1; constructor; cofe_subst.
     - destruct 1; by cofe_subst.
@@ -1295,17 +1323,18 @@ Section option.
       + by exists None, (Some x); repeat constructor.
       + exists None, None; repeat constructor.
   Qed.
-  Canonical Structure optionR :=
-    CMRAT (option A) option_ofe_mixin option_cmra_mixin.
+  Definition option_cmra_mixin := CMRAMixin option_ofe_laws option_cmra_laws.
+  Canonical Structure optionR := CMRAT (option A) option_cmra_mixin.
 
   Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
   Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
 
   Instance option_empty : Empty (option A) := None.
-  Lemma option_ucmra_mixin : UCMRAMixin optionR.
+  Lemma option_ucmra_laws : ucmra_laws (option A).
   Proof. split. done. by intros []. done. Qed.
-  Canonical Structure optionUR :=
-    UCMRAT (option A) option_ofe_mixin option_cmra_mixin option_ucmra_mixin.
+  Definition option_ucmra_mixin :=
+    UCMRAMixin option_ofe_laws option_cmra_laws option_ucmra_laws.
+  Canonical Structure optionUR := UCMRAT (option A) option_ucmra_mixin.
 
   (** Misc *)
   Global Instance Some_cmra_monotone : CMRAMonotone Some.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 0474eb3a8b2d9fdb32cb6695c2190976b04b3c0e..30b3be9ef5d4aee3f4a239474e03e042fba2fa0c 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -52,7 +52,7 @@ Record tower := {
 }.
 Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
 Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
-Definition tower_ofe_mixin : OfeMixin tower.
+Lemma tower_ofe_laws : ofe_laws tower.
 Proof.
   split.
   - intros X Y; split; [by intros HXY n k; apply equiv_dist|].
@@ -64,6 +64,7 @@ Proof.
   - intros k X Y HXY n; apply dist_S.
     by rewrite -(g_tower X) (HXY (S n)) g_tower.
 Qed.
+Definition tower_ofe_mixin := OfeMixin tower_ofe_laws.
 Definition T : ofeT := OfeT tower tower_ofe_mixin.
 
 Program Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 36bd80ee99439aa7ac3c3caa5818d87ed4e6ceb6..a36cb9e3c94f6d2211e9790b6c1e27b5f63252c2 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -1,7 +1,9 @@
 From iris.algebra Require Export cmra.
 From iris.prelude Require Export gmap.
+(*
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
+*)
 Set Default Proof Using "Type".
 
 Section cofe.
@@ -10,12 +12,33 @@ Implicit Types m : gmap K A.
 
 Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
   ∀ i, m1 !! i ≡{n}≡ m2 !! i.
-Definition gmap_ofe_mixin : OfeMixin (gmap K A).
+Definition gmap_ofe_mixin : ofe_laws (gmap K A).
 Proof.
   split.
   - intros m1 m2; split.
     + by intros Hm n k; apply equiv_dist.
-    + intros Hm k; apply equiv_dist; intros n; apply Hm.
+    + intros Hm k.
+Check @equiv_dist.
+apply equiv_dist.
+(** FOOBAR -- This gives:
+Error:
+In environment
+K : Type
+EqDecision0 : EqDecision K
+H : Countable K
+A : ofeT
+m1, m2 : gmap K A
+Hm : ∀ n : nat, m1 ≡{n}≡ m2
+k : K
+Unable to unify
+ "(?M4301 ≡ ?M4302 → ∀ n : nat, ?M4301 ≡{n}≡ ?M4302)
+  ∧ ((∀ n : nat, ?M4301 ≡{n}≡ ?M4302) → ?M4301 ≡ ?M4302)" with
+ "option_Forall2 equiv (m1 !! k) (m2 !! k)".
+
+*)
+ (A:=optionC A).
+apply H0.
+apply equiv_dist. intros n; apply Hm.
   - intros n; split.
     + by intros m k.
     + by intros m1 m2 ? k.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index d3ebd8e71cb0cbf2877b6a719a1f05fb868a652f..2c5118d2b5cbb6374288f698f48630633e35fd57 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -33,40 +33,45 @@ Tactic Notation "cofe_subst" :=
   | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
   end.
 
-Record OfeMixin A `{Equiv A, Dist A} := {
-  mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
-  mixin_dist_equivalence n : Equivalence (dist n);
-  mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y
+Record ofe_laws A `{Equiv A, Dist A} := {
+  law_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
+  law_dist_equivalence n : Equivalence (dist n);
+  law_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y
 }.
+Record ofe_mixin A := OfeMixin {
+  ofe_mixin_equiv : Equiv A;
+  ofe_mixin_dist : Dist A;
+  ofe_mixin_laws_of : ofe_laws A;
+}.
+Arguments OfeMixin {_ _ _} _.
 
 (** Bundeled version *)
-Structure ofeT := OfeT' {
-  ofe_car :> Type;
-  ofe_equiv : Equiv ofe_car;
-  ofe_dist : Dist ofe_car;
-  ofe_mixin : OfeMixin ofe_car;
-  _ : Type
-}.
-Arguments OfeT' _ {_ _} _ _.
+Structure ofeT := OfeT' { ofe_car :> Type; _ : ofe_mixin ofe_car; _ : Type }.
 Notation OfeT A m := (OfeT' A m A).
 Add Printing Constructor ofeT.
-Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
-Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
 Arguments ofe_car : simpl never.
+
+Definition ofe_mixin_of (A : ofeT) : ofe_mixin A := let 'OfeT' _ m _ := A in m.
+Arguments ofe_mixin_of : simpl never.
+
+Definition ofe_equiv {A : ofeT} : Equiv A := ofe_mixin_equiv _ (ofe_mixin_of A).
 Arguments ofe_equiv : simpl never.
+Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
+Definition ofe_dist {A : ofeT} : Dist A := ofe_mixin_dist _ (ofe_mixin_of A).
 Arguments ofe_dist : simpl never.
-Arguments ofe_mixin : simpl never.
+Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
 
 (** Lifting properties from the mixin *)
 Section ofe_mixin.
   Context {A : ofeT}.
   Implicit Types x y : A.
+  Local Coercion ofe_mixin_of : ofeT >-> ofe_mixin.
   Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y.
-  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
+  Proof. apply (law_equiv_dist _ (ofe_mixin_laws_of _ A)). Qed.
   Global Instance dist_equivalence n : Equivalence (@dist A _ n).
-  Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
+  Proof. apply (law_dist_equivalence _ (ofe_mixin_laws_of _ A)). Qed.
   Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
-  Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
+  Proof. apply (law_dist_S _ (ofe_mixin_laws_of _ A)). Qed.
 End ofe_mixin.
 
 Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
@@ -100,8 +105,7 @@ Class Cofe (A : ofeT) := {
 }.
 Arguments compl : simpl never.
 
-Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c
-      `(NonExpansive f) :
+Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
   compl (chain_map f c) ≡ f (compl c).
 Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
 
@@ -395,7 +399,7 @@ Section ofe_fun.
   Context {A : Type} {B : ofeT}.
   Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, ∀ x, f x ≡ g x.
   Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B).
+  Definition ofe_fun_ofe_laws : ofe_laws (ofe_fun A B).
   Proof.
     split.
     - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -406,6 +410,7 @@ Section ofe_fun.
       + by intros f g h ?? x; trans (g x).
     - by intros n f g ? x; apply dist_S.
   Qed.
+  Definition ofe_fun_ofe_mixin := OfeMixin ofe_fun_ofe_laws.
   Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
 
   Program Definition ofe_fun_chain `(c : chain ofe_funC)
@@ -441,7 +446,7 @@ Section ofe_mor.
   Proof. apply ne_proper, ofe_mor_ne. Qed.
   Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x.
   Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B).
+  Definition ofe_mor_ofe_laws : ofe_laws (ofe_mor A B).
   Proof.
     split.
     - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -452,6 +457,7 @@ Section ofe_mor.
       + by intros f g h ?? x; trans (g x).
     - by intros n f g ? x; apply dist_S.
   Qed.
+  Definition ofe_mor_ofe_mixin := OfeMixin ofe_mor_ofe_laws.
   Canonical Structure ofe_morC := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
 
   Program Definition ofe_mor_chain (c : chain ofe_morC)
@@ -518,8 +524,9 @@ Qed.
 (** unit *)
 Section unit.
   Instance unit_dist : Dist unit := λ _ _ _, True.
-  Definition unit_ofe_mixin : OfeMixin unit.
+  Definition unit_ofe_laws : ofe_laws unit.
   Proof. by repeat split; try exists 0. Qed.
+  Definition unit_ofe_mixin := OfeMixin unit_ofe_laws.
   Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin.
 
   Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
@@ -538,7 +545,7 @@ Section product.
     NonExpansive2 (@pair A B) := _.
   Global Instance fst_ne : NonExpansive (@fst A B) := _.
   Global Instance snd_ne : NonExpansive (@snd A B) := _.
-  Definition prod_ofe_mixin : OfeMixin (A * B).
+  Definition prod_ofe_laws : ofe_laws (A * B).
   Proof.
     split.
     - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
@@ -546,6 +553,7 @@ Section product.
     - apply _.
     - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
   Qed.
+  Definition prod_ofe_mixin := OfeMixin prod_ofe_laws.
   Canonical Structure prodC : ofeT := OfeT (A * B) prod_ofe_mixin.
 
   Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodC :=
@@ -704,7 +712,7 @@ Section sum.
   Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _.
   Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _.
 
-  Definition sum_ofe_mixin : OfeMixin (A + B).
+  Definition sum_ofe_laws : ofe_laws (A + B).
   Proof.
     split.
     - intros x y; split=> Hx.
@@ -713,6 +721,7 @@ Section sum.
     - apply _.
     - destruct 1; constructor; by apply dist_S.
   Qed.
+  Definition sum_ofe_mixin := OfeMixin sum_ofe_laws.
   Canonical Structure sumC : ofeT := OfeT (A + B) sum_ofe_mixin.
 
   Program Definition inl_chain (c : chain sumC) (a : A) : chain A :=
@@ -787,20 +796,22 @@ Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
 
   Instance discrete_dist : Dist A := λ n x y, x ≡ y.
-  Definition discrete_ofe_mixin : OfeMixin A.
+  Definition discrete_ofe_laws : ofe_laws A.
   Proof using Type*.
     split.
     - intros x y; split; [done|intros Hn; apply (Hn 0)].
     - done.
     - done.
   Qed.
+  Definition discrete_ofe_mixin := OfeMixin discrete_ofe_laws.
 
   Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
     { compl c := c 0 }.
   Next Obligation.
-    intros n c. rewrite /compl /=;
-    symmetry; apply (chain_cauchy c 0 n). omega.
+    intros n c. by rewrite /compl /= -(chain_cauchy c 0 n); last omega.
   Qed.
+  Global Instance discrete_discrete : Discrete (OfeT A discrete_ofe_mixin).
+  Proof. by intros x y. Qed.
 End discrete_cofe.
 
 Notation discreteC A := (OfeT A discrete_ofe_mixin).
@@ -826,7 +837,7 @@ Section option.
   Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
   Proof. done. Qed.
 
-  Definition option_ofe_mixin : OfeMixin (option A).
+  Definition option_ofe_laws : ofe_laws (option A).
   Proof.
     split.
     - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
@@ -835,6 +846,7 @@ Section option.
     - apply _.
     - destruct 1; constructor; by apply dist_S.
   Qed.
+  Definition option_ofe_mixin := OfeMixin option_ofe_laws.
   Canonical Structure optionC := OfeT (option A) option_ofe_mixin.
 
   Program Definition option_chain (c : chain optionC) (x : A) : chain A :=
@@ -927,7 +939,7 @@ Section later.
   Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
   Instance later_dist : Dist (later A) := λ n x y,
     dist_later n (later_car x) (later_car y).
-  Definition later_ofe_mixin : OfeMixin (later A).
+  Definition later_ofe_laws : ofe_laws (later A).
   Proof.
     split.
     - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
@@ -938,6 +950,7 @@ Section later.
       + by intros [x] [y] [z] ??; trans y.
     - intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S.
   Qed.
+  Definition later_ofe_mixin := OfeMixin later_ofe_laws.
   Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin.
 
   Program Definition later_chain (c : chain laterC) : chain A :=
@@ -1046,7 +1059,7 @@ Section sigma.
   Proof. done. Qed.
   Global Instance proj1_sig_ne : NonExpansive (@proj1_sig _ P).
   Proof. by intros n [a Ha] [b Hb] ?. Qed.
-  Definition sig_ofe_mixin : OfeMixin (sig P).
+  Definition sig_ofe_laws : ofe_laws (sig P).
   Proof.
     split.
     - intros [a ?] [b ?]. rewrite /dist /sig_dist /equiv /sig_equiv /=.
@@ -1055,6 +1068,7 @@ Section sigma.
       split; [intros []| intros [] []| intros [] [] []]=> //= -> //.
     - intros n [a ?] [b ?]. rewrite /dist /sig_dist /=. apply dist_S.
   Qed.
+  Definition sig_ofe_mixin := OfeMixin sig_ofe_laws.
   Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
 
   (* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 0ac232c72952ca916afb8f7c528a2d0d75b2bc15..d2fbb6d31de2a74f4f8fa897ce792bac6e9dce53 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -28,7 +28,8 @@ Section cofe.
   Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
     { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
   Instance uPred_dist : Dist (uPred M) := uPred_dist'.
-  Definition uPred_ofe_mixin : OfeMixin (uPred M).
+
+  Lemma uPred_ofe_laws : ofe_laws (uPred M).
   Proof.
     split.
     - intros P Q; split.
@@ -41,6 +42,7 @@ Section cofe.
         by trans (Q i x);[apply HP|apply HQ].
     - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
   Qed.
+  Definition uPred_ofe_mixin := OfeMixin uPred_ofe_laws.
   Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.
 
   Program Definition uPred_compl : Compl uPredC := λ c,
@@ -73,9 +75,27 @@ Qed.
 
 (** functor *)
 Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} (P : uPred M1) :
+    `{!CMRAMonotone f} (P : uPred M1) :
   uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
+Next Obligation. (* naive_solver eauto using uPred_mono, cmra_monotoneN. *)
+intros; simpl in *.
+eapply uPred_mono. eauto.
+eapply cmra_monotoneN.
+(** FOOBAR -- This yields:
+Error:
+In environment
+M1, M2 : ucmraT
+f : M2 -n> M1
+CMRAMonotone0 : CMRAMonotone f
+P : uPred M1
+n : nat
+x1, x2 : M2
+H : P n (f x1)
+H0 : x1 ≼{n} x2
+Unable to unify "∃ z : ?B, ?M3650 ?M3654 ≡{?M3652}≡ ?M3650 ?M3653 ⋅ z" with
+ "∃ z : M1, f x2 ≡{n}≡ f x1 ⋅ z".
+*)
+Qed.
 Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
 
 Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)