diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d4418c515e2d989ff513ce006dfa32448a8228e1..cff69e8da34b3b7c82c5b7d7b2ae3e7cdc9bebbf 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -874,6 +874,22 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
   ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x
 }.
 
+Section leibniz.
+  Local Set Default Proof Using "Type*".
+  Context A `{Equiv A, PCore A, Op A, Valid A}.
+  Context `{!Equivalence (≡@{A}), !LeibnizEquiv A}.
+  Context (op_assoc : Assoc (=@{A}) (⋅)).
+  Context (op_comm : Comm (=@{A}) (⋅)).
+  Context (pcore_l : ∀ (x : A) cx, pcore x = Some cx → cx ⋅ x = x).
+  Context (ra_pcore_idemp : ∀ (x : A) cx, pcore x = Some cx → pcore cx = Some cx).
+  Context (ra_pcore_mono : ∀ (x y : A) cx,
+    x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy).
+  Context (ra_valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x).
+
+  Definition ra_leibniz_mixin : RAMixin A.
+  Proof. split; repeat intro; fold_leibniz; naive_solver. Qed.
+End leibniz.
+
 Section discrete.
   Local Set Default Proof Using "Type*".
   Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A (≡)).
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 2c8165cf10bff603132c3f7e054bee0c1129537d..245cb63fdc28704d51a063247fecd8f14b1e5db0 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -40,10 +40,12 @@ Instance dec_agree_pcore : PCore (dec_agree A) := Some.
 
 Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
 Proof.
-  apply ra_total_mixin; apply _ || eauto.
+  apply ra_leibniz_mixin; try (apply _ || done).
   - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
   - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|]; by repeat (simplify_eq/= || case_match).
+  - rewrite /pcore /dec_agree_pcore=> -? [?|] [->];
+      by repeat (simplify_eq/= || case_match).
+  - rewrite /pcore /dec_agree_pcore. naive_solver.
   - by intros [?|] [?|] ?.
 Qed.
 
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index f5f84eb01cf3f4fb43fcde9ef143018548e7da74..003a4fe23c70da4fea180ef4692c4b99477d5a58 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -28,7 +28,7 @@ Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
 
 Definition frac_ra_mixin : RAMixin frac.
 Proof.
-  split; try apply _; try done.
+  apply ra_leibniz_mixin; try (apply _ || done).
   unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
   rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
 Qed.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 4ace8f8f7f88b43f6c969ebf5107126deff23b6d..3375a0af2ed8f0519d273ad5c38fa1edb7df2763 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -89,7 +89,7 @@ Section cmra.
   Proof.
     move=>x'; destruct (decide (x = x')) as [->|];
       by rewrite ofe_fun_lookup_core ?ofe_fun_lookup_singleton
-      ?ofe_fun_lookup_singleton_ne // (core_id_core ∅).
+      ?ofe_fun_lookup_singleton_ne // (core_id_core ε).
   Qed.
 
   Global Instance ofe_fun_singleton_core_id x (y : B x) :
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index f2bcdfe9919b9710933f370b339cd9c53da12f67..9b0d7c5fe44cf934b492bef95b1ebe21b5ae3c99 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -92,7 +92,8 @@ Proof.
   by apply: discrete; rewrite -Hm lookup_insert_ne.
 Qed.
 Global Instance gmap_singleton_discrete i x :
-  Discrete x → Discrete ({[ i := x ]} : gmap K A) := _.
+  Discrete x → Discrete ({[ i := x ]} : gmap K A).
+Proof. rewrite /singletonM. apply _. Qed.
 Lemma insert_idN n m i x :
   m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m.
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 8d9aa0db0086194ae2d81942f979aee5ee6e7948..976d4d2dd906198d9be0c08cde00c1ffc465b3af 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -296,10 +296,10 @@ Section properties.
   Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
   Proof. apply Forall_replicate. Qed.
   Global Instance list_singletonM_ne i :
-    NonExpansive (@list_singletonM A i).
+    NonExpansive (singletonM (M:=list A) i).
   Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
   Global Instance list_singletonM_proper i :
-    Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
+    Proper ((≡) ==> (≡)) (singletonM (M:=list A) i) := ne_proper _.
 
   Lemma elem_of_list_singletonM i z x : z ∈ ({[i := x]} : list A) → z = ε ∨ z = x.
   Proof.
@@ -332,7 +332,7 @@ Section properties.
   Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
   Proof.
     rewrite /singletonM /list_singletonM.
-    by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ∅).
+    by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ε).
   Qed.
   Lemma list_op_singletonM i (x y : A) :
     {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index 1b378db332bf62a98772e3e548dd6322c7e64d77..75ec408d376ca2a6672e10a6b1ccfaf759060a9c 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -24,7 +24,7 @@ Corollary ufrac_included_weak (x y : ufrac) : x ≼ y → (x ≤ y)%Qc.
 Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed.
 
 Definition ufrac_ra_mixin : RAMixin ufrac.
-Proof. split; try apply _; try done. Qed.
+Proof. apply ra_leibniz_mixin; try (apply _ || done). Qed.
 Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
 
 Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index 387b24bf8d789e3f0d09910a85b943dcc9333e24..d48098738a2318a615bb01e6eff89a3c0ee2adb1 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -10,7 +10,7 @@ Definition stuckness_leb (s1 s2 : stuckness) : bool :=
   | _, _ => true
   end.
 Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
-Instance stuckness_le_po : PreOrder stuckness_le.
+Instance stuckness_le_po : PreOrder (⊑@{stuckness}).
 Proof. split; by repeat intros []. Qed.
 
 Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 3b964c1fe6e944f5b6d3e6692ca42aa7e55db2fc..f9c150142695b179f724fdc06137d5077768c269 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -47,7 +47,8 @@ Proof.
   - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
     iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
-      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
+      [[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?];
+      simplify_eq/=.
     rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
 Qed.
 
@@ -79,7 +80,8 @@ Proof.
     prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ).
   assert (NonExpansive Ψ').
   { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
-      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
+      [[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?];
+      simplify_eq/=. by apply HΨ. }
   iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
   iIntros "!#" ([[??] ?]) "H". by iApply "IH".
 Qed.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 5d85ca71d0636797ebe12c4bcadf9a83204b5938..4fe446718c8410d8d3098cc9293ef5cd36dcfb94 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -375,7 +375,7 @@ Global Instance frame_monPred_at_wand p P R Q1 Q2 i j :
   Frame p R Q1 Q2 →
   FrameMonPredAt p j (R i) (P -∗ Q1) ((P -∗ Q2) i).
 Proof.
-  rewrite /Frame /FrameMonPredAt=>-> Hframe.
+  rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
   rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
   change ((□?p R ∗ (P -∗ Q2)) -∗ P -∗ Q1). apply bi.wand_intro_r.
   rewrite -assoc bi.wand_elim_l. done.
@@ -385,7 +385,7 @@ Global Instance frame_monPred_at_impl P R Q1 Q2 i j :
   Frame true R Q1 Q2 →
   FrameMonPredAt true j (R i) (P → Q1) ((P → Q2) i).
 Proof.
-  rewrite /Frame /FrameMonPredAt=>-> Hframe.
+  rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
   rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
   change ((□ R ∗ (P → Q2)) -∗ P → Q1).
   rewrite -bi.persistently_and_intuitionistically_sep_l. apply bi.impl_intro_r.