diff --git a/Iris/Iris/BI/Algebra.lean b/Iris/Iris/BI/Algebra.lean
index e46003ce5..93467f064 100644
--- a/Iris/Iris/BI/Algebra.lean
+++ b/Iris/Iris/BI/Algebra.lean
@@ -270,7 +270,7 @@ theorem agree_includedI (x y : Agree A) :
   · refine siPure_mono (exists_elim (fun c => ?_))
     exact (fun n Heq => (includedN.mp ⟨c, Heq⟩).trans op_commN)
   · refine siPure_mono (exists_intro_trans y ?_)
-    exact entails_preorder.refl
+    rfl
 
 @[rocq_alias to_agree_includedI]
 theorem toAgree_includedI (a b : A) :
diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean
index 7b83c8ddc..3582c54dc 100644
--- a/Iris/Iris/BI/BI.lean
+++ b/Iris/Iris/BI/BI.lean
@@ -22,7 +22,9 @@ theorem liftRel_eq : liftRel (@Eq α) A B ↔ A = B := by
 
 /-- Require that a separation logic with carrier type `PROP` fulfills all necessary axioms. -/
 class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where
-  entails_preorder : Preorder Entails
+  entails_refl {P : PROP} : P ⊢ P
+  entails_trans {P Q R : PROP} : (P ⊢ Q) → (Q ⊢ R) → P ⊢ R
+
   equiv_iff {P Q : PROP} : (P ≡ Q) ↔ P ⊣⊢ Q := by simp
 
   and_ne : OFE.NonExpansive₂ and
@@ -82,12 +84,17 @@ class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where
 
 namespace BI
 
-attribute [instance] BI.entails_preorder
+instance [BIBase PROP] : LE PROP where
+  le := BIBase.Entails
+
+instance BI.entails_preorder [BI PROP] : Std.IsPreorder PROP where
+  le_refl _ := BI.entails_refl
+  le_trans _ _ _ := BI.entails_trans
 
 theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R :=
-  Transitive.trans h1 h2
+  BI.entails_trans h1 h2
 
-@[simp] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := refl
+@[simp,refl] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := BI.entails_refl
 
 theorem BIBase.Entails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q := h ▸ .rfl
 
diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean
index 2e71ef58c..447aaf4c2 100644
--- a/Iris/Iris/BI/DerivedLaws.lean
+++ b/Iris/Iris/BI/DerivedLaws.lean
@@ -21,7 +21,8 @@ open Iris.Std BI
 
 /-! # Entails -/
 
-instance entails_trans [BI PROP] : Trans (α := PROP) Entails Entails Entails where
+/- Necessary for `calc`-style proofs. -/
+instance entails_trans' [BI PROP] : Trans (α := PROP) Entails Entails Entails where
   trans h1 h2 := h1.trans h2
 instance entails_antisymm [BI PROP] : Antisymmetric (α := PROP) BiEntails Entails where
   antisymm h1 h2 := ⟨h1, h2⟩
@@ -2026,7 +2027,7 @@ theorem intuitionisticallyIf_sep {p : Bool} [BI PROP] [BIPositive PROP] {P Q : P
 theorem intuitionisticallyIf_sep_conj {p1 p2 : Bool} [BI PROP] {P Q : PROP} :
   (□?p1 P ∗ □?p2 Q) ⊢ □?(p1 && p2) (P ∗ Q) :=
   match p1, p2 with
-  | false, false => refl
+  | false, false => by rfl
   | false, true  => sep_mono_right intuitionisticallyIf_elim
   | true,  false => sep_mono_left intuitionisticallyIf_elim
   | true,  true  => intuitionisticallyIf_sep_mpr
diff --git a/Iris/Iris/BI/MonPred.lean b/Iris/Iris/BI/MonPred.lean
index 71a753ce5..74e5a33d9 100644
--- a/Iris/Iris/BI/MonPred.lean
+++ b/Iris/Iris/BI/MonPred.lean
@@ -43,8 +43,8 @@ predicates are functions out of a `BiIndex` that are monotone w.r.t. this order.
 structure BiIndex where
   car : Type _
   [inhabited : Inhabited car]
-  rel : car → car → Prop
-  [preorder : Std.Preorder rel]
+  rel : LE car
+  [preorder : Std.IsPreorder car]
 
 attribute [instance] BiIndex.inhabited BiIndex.preorder
 
@@ -56,7 +56,7 @@ scoped infix:40 " ⊑ᵢ " => BiIndex.rel _
 /-- A `BiIndex` with a bottom element `bot`: every index is above `bot`. -/
 @[rocq_alias BiIndexBottom]
 class BiIndexBottom (I : BiIndex) (bot : I.car) : Prop where
-  bot_le : ∀ i : I.car, I.rel bot i
+  bot_le : ∀ i : I.car, I.rel.le bot i
 
 /-- A monotone predicate over `BiIndex` `I` valued in the base BI `PROP`: a function
 `monPred_at : I → PROP` monotone w.r.t. the index order. -/
@@ -65,7 +65,7 @@ structure MonPred (I : BiIndex) (PROP : Type _) [BIBase PROP] where
   /-- The underlying index-indexed family (Rocq `monPred_at`). -/
   monPred_at : I.car → PROP
   /-- Monotonicity in the index (Rocq `monPred_mono`: `Proper ((⊑) ==> (⊢))`). -/
-  monPred_mono : ∀ {i j : I.car}, I.rel i j → (monPred_at i ⊢ monPred_at j)
+  monPred_mono : ∀ {i j : I.car}, I.rel.le i j → (monPred_at i ⊢ monPred_at j)
 
 namespace MonPred
 
@@ -85,7 +85,7 @@ theorem ext {P Q : MonPred I PROP} (h : ∀ i, P.monPred_at i = Q.monPred_at i)
 so the result is monotone. -/
 @[rocq_alias monPred_defs.monPred_upclosed]
 def upclosed [BI PROP] (Φ : I.car → PROP) : I.car → PROP :=
-  fun i => iprop(∀ j, ⌜I.rel i j⌝ → Φ j)
+  fun i => iprop(∀ j, ⌜I.rel.le i j⌝ → Φ j)
 
 end MonPred
 
@@ -118,7 +118,7 @@ namespace MonPred
 `monPred_sig`. -/
 @[rocq_alias monPred_sig]
 def toSig :
-    MonPred I PROP -n> { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) } where
+    MonPred I PROP -n> { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) } where
   f P := ⟨P.monPred_at, fun h => P.monPred_mono h⟩
   ne.1 _ _ _ h := h
 
@@ -126,7 +126,7 @@ def toSig :
 Rocq `sig_monPred`. -/
 @[rocq_alias sig_monPred]
 def ofSig :
-    { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) } -n> MonPred I PROP where
+    { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) } -n> MonPred I PROP where
   f P := ⟨P.val, P.property⟩
   ne.1 _ _ _ h := h
 
@@ -134,7 +134,7 @@ def ofSig :
 theorem ofSig_ne : OFE.NonExpansive (ofSig (I := I) (PROP := PROP)) := ofSig.ne
 
 @[rocq_alias sig_monPred_proper]
-theorem ofSig_proper {P Q : { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) }}
+theorem ofSig_proper {P Q : { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) }}
     (h : P ≡ Q) : ofSig P ≡ ofSig Q := ofSig.ne.eqv h
 
 @[rocq_alias monPred_sig_ne]
@@ -147,7 +147,7 @@ theorem toSig_proper {P Q : MonPred I PROP} (h : P ≡ Q) : toSig P ≡ toSig Q
 theorem ofSig_toSig (P : MonPred I PROP) : ofSig (toSig P) = P := rfl
 
 @[rocq_alias monPred_sig_monPred]
-theorem toSig_ofSig (P : { f : I.car → PROP // ∀ {i j : I.car}, I.rel i j → (f i ⊢ f j) }) :
+theorem toSig_ofSig (P : { f : I.car → PROP // ∀ {i j : I.car}, I.rel.le i j → (f i ⊢ f j) }) :
     toSig (ofSig P) = P := rfl
 
 end MonPred
@@ -219,7 +219,7 @@ def imp (P Q : MonPred I PROP) : MonPred I PROP where
   monPred_at := MonPred.upclosed (fun i => iprop(P.monPred_at i → Q.monPred_at i))
   monPred_mono h :=
     forall_intro fun k => (forall_elim k).trans
-      (imp_mono_left (pure_mono fun hjk => Transitive.trans h hjk))
+      (imp_mono_left (pure_mono fun hjk => Trans.trans h hjk))
 
 #rocq_ignore monPred_defs.monPred_impl_def "Rocq unsealed definition body; use MonPred.imp."
 #rocq_ignore monPred_defs.monPred_impl_aux "Rocq sealing auxiliary definition."
@@ -279,7 +279,7 @@ def wand (P Q : MonPred I PROP) : MonPred I PROP where
   monPred_at := MonPred.upclosed (fun i => iprop(P.monPred_at i -∗ Q.monPred_at i))
   monPred_mono h :=
     forall_intro fun k => (forall_elim k).trans
-      (imp_mono_left (pure_mono fun hjk => Transitive.trans h hjk))
+      (imp_mono_left (pure_mono fun hjk => Trans.trans h hjk))
 
 #rocq_ignore monPred_defs.monPred_wand_def "Rocq unsealed definition body; use MonPred.wand."
 #rocq_ignore monPred_defs.monPred_wand_aux "Rocq sealing auxiliary definition."
@@ -309,8 +309,8 @@ def later (P : MonPred I PROP) : MonPred I PROP where
 
 @[rocq_alias monPred_defs.monPred_in]
 def monPred_in (j : I.car) : MonPred I PROP where
-  monPred_at i := iprop(⌜I.rel j i⌝)
-  monPred_mono h := pure_mono fun hji => Transitive.trans hji h
+  monPred_at i := iprop(⌜I.rel.le j i⌝)
+  monPred_mono h := pure_mono fun hji => Trans.trans hji h
 
 #rocq_ignore monPred_defs.monPred_in_def "Rocq unsealed definition body; use MonPred.monPred_in."
 #rocq_ignore monPred_defs.monPred_in_aux "Rocq sealing auxiliary definition."
@@ -392,9 +392,8 @@ theorem dist_at {n : Nat} {P Q : MonPred I PROP} :
 mixins, packaged into `monPredI : bi`). -/
 @[rocq_alias monPredI]
 instance : BI (MonPred I PROP) where
-  entails_preorder :=
-    { refl := entails_at.mpr fun _ => BIBase.Entails.rfl
-      trans := fun h h' => entails_at.mpr fun i => (entails_at.mp h i).trans (entails_at.mp h' i) }
+  entails_refl := entails_at.mpr fun _ => BIBase.Entails.rfl
+  entails_trans := fun h h' => entails_at.mpr fun i => (entails_at.mp h i).trans (entails_at.mp h' i)
   equiv_iff := fun {P Q} =>
     ⟨fun h => ⟨entails_at.mpr fun i => (equiv_iff.mp (equiv_at.mp h i)).mp,
               entails_at.mpr fun i => (equiv_iff.mp (equiv_at.mp h i)).mpr⟩,
@@ -431,11 +430,11 @@ instance : BI (MonPred I PROP) where
   or_intro_r := entails_at.mpr fun i => or_intro_r
   or_elim h h' := entails_at.mpr fun i => or_elim (entails_at.mp h i) (entails_at.mp h' i)
   imp_intro {P Q R} h := entails_at.mpr fun i =>
-    forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel i j) =>
+    forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel.le i j) =>
       (P.monPred_mono hij).trans <| imp_intro (entails_at.mp h j)
   imp_elim {P Q R} h := entails_at.mpr fun i =>
     imp_elim <| (entails_at.mp h i).trans <|
-      (forall_elim i).trans <| pure_imp_elim (Reflexive.refl : I.rel i i)
+      (forall_elim i).trans <| pure_imp_elim (Std.Refl.refl i : I.rel.le i i)
   sForall_intro h := entails_at.mpr fun i =>
     MonPred.sForall_at_intro i fun q hΨ => entails_at.mp (h q hΨ) i
   sForall_elim h := entails_at.mpr fun i => MonPred.sForall_at_elim i h
@@ -448,12 +447,12 @@ instance : BI (MonPred I PROP) where
   sep_assoc_l := entails_at.mpr fun i => sep_assoc_l
   wand_intro {P Q R} h := entails_at.mpr fun i => by
     refine forall_intro fun j => imp_intro ?_
-    refine pure_elim_right fun (hij : I.rel i j) => ?_
+    refine pure_elim_right fun (hij : I.rel.le i j) => ?_
     refine wand_intro (sep_symm.trans ?_)
     exact (sep_mono_right (P.monPred_mono hij)).trans (sep_symm.trans (entails_at.mp h j))
   wand_elim {P Q R} h := entails_at.mpr fun i =>
     (sep_mono_left ((entails_at.mp h i).trans
-      ((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))))).trans wand_elim_left
+      ((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))))).trans wand_elim_left
   persistently_mono h := entails_at.mpr fun i => persistently_mono (entails_at.mp h i)
   persistently_idem_2 := entails_at.mpr fun i => persistently_idem_2
   persistently_emp_2 := entails_at.mpr fun i => persistently_emp_2
@@ -477,7 +476,7 @@ instance : BI (MonPred I PROP) where
     refine (MonPred.sForall_at_elim (q := MonPred.imp (MonPred.pure (Φ r)) (MonPred.later r))
         i ⟨r, rfl⟩).trans ?_
     refine (forall_elim i).trans ?_
-    exact (pure_imp_elim (Reflexive.refl : I.rel i i)).trans (pure_imp_elim hΦ)
+    exact (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)).trans (pure_imp_elim hΦ)
   later_sExists_false := fun {Φ} => entails_at.mpr fun i => by
     refine later_sExists_false.trans (or_mono BIBase.Entails.rfl ?_)
     refine exists_elim fun p => pure_elim_left fun ⟨q, hΦ, hq⟩ => ?_
@@ -491,7 +490,7 @@ instance : BI (MonPred I PROP) where
   later_false_em {P} := entails_at.mpr fun i => by
     refine later_false_em.trans (or_mono_right ?_)
     refine forall_intro fun j => imp_intro ?_
-    refine pure_elim_right fun (hij : I.rel i j) => ?_
+    refine pure_elim_right fun (hij : I.rel.le i j) => ?_
     exact imp_mono BIBase.Entails.rfl (P.monPred_mono hij)
 
 #rocq_ignore monPred_unseal "Rocq unsealing command."
@@ -518,14 +517,14 @@ instance : BiEmbed PROP (MonPred I PROP) where
   emp_valid_inj _ h := entails_at.mp h (Inhabited.default : I.car)
   emp_2 := entails_at.mpr fun _ => .rfl
   impl_2 _ _ := entails_at.mpr fun i =>
-    (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))
+    (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))
   forall_2 := fun _Ψ {_} h => entails_at.mpr fun i =>
     sForall_intro fun P hΨ => entails_at.mp (h P hΨ) i
   exist_1 := fun _Ψ {_} h => entails_at.mpr fun i =>
     sExists_elim fun P hΨ => entails_at.mp (h P hΨ) i
   sep _ _ := BIBase.BiEntails.of_eq rfl
   wand_2 _ _ := entails_at.mpr fun i =>
-    (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))
+    (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))
   persistently _ := BIBase.BiEntails.of_eq rfl
 
 #rocq_ignore monPred_embedding_mixin "Rocq mixin record; subsumed by the BiEmbed instance."
@@ -627,7 +626,7 @@ instance [BIFUpdate PROP] : BIFUpdate (MonPred I PROP) where
   trans := entails_at.mpr fun _ => BIFUpdate.trans
   mask_frame_right_strong h := entails_at.mpr fun i =>
     (BIFUpdate.mono
-      (((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))) : _ ⊢@{PROP} _)).trans
+      (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))) : _ ⊢@{PROP} _)).trans
       (BIFUpdate.mask_frame_right_strong h)
   frame_right := entails_at.mpr fun _ => fupd_frame_right
 
@@ -676,7 +675,7 @@ theorem monPred_at_or (i : I.car) (P Q : MonPred I PROP) :
 @[rocq_alias monPred_at_impl]
 theorem monPred_at_impl (i : I.car) (P Q : MonPred I PROP) :
     (iprop(P → Q)).monPred_at i ⊣⊢
-      iprop(∀ j, ⌜I.rel i j⌝ → (P.monPred_at j → Q.monPred_at j)) :=
+      iprop(∀ j, ⌜I.rel.le i j⌝ → (P.monPred_at j → Q.monPred_at j)) :=
   BIBase.BiEntails.of_eq rfl
 
 @[rocq_alias monPred_at_forall]
@@ -700,7 +699,7 @@ theorem monPred_at_sep (i : I.car) (P Q : MonPred I PROP) :
 @[rocq_alias monPred_at_wand]
 theorem monPred_at_wand (i : I.car) (P Q : MonPred I PROP) :
     (iprop(P -∗ Q)).monPred_at i ⊣⊢
-      iprop(∀ j, ⌜I.rel i j⌝ → (P.monPred_at j -∗ Q.monPred_at j)) :=
+      iprop(∀ j, ⌜I.rel.le i j⌝ → (P.monPred_at j -∗ Q.monPred_at j)) :=
   BIBase.BiEntails.of_eq rfl
 
 @[rocq_alias monPred_at_persistently]
@@ -715,7 +714,7 @@ theorem monPred_at_later (i : I.car) (P : MonPred I PROP) :
 
 @[rocq_alias monPred_at_in]
 theorem monPred_at_in (i j : I.car) :
-    (MonPred.monPred_in j : MonPred I PROP).monPred_at i ⊣⊢ iprop(⌜I.rel j i⌝) :=
+    (MonPred.monPred_in j : MonPred I PROP).monPred_at i ⊣⊢ iprop(⌜I.rel.le j i⌝) :=
   BIBase.BiEntails.of_eq rfl
 
 @[rocq_alias monPred_at_embed]
@@ -795,12 +794,12 @@ theorem monPred_at_emp_valid (P : MonPred I PROP) : (⊢ P) ↔ ∀ i, ⊢ P.mon
   entails_at
 
 @[rocq_alias monPred_at_mono]
-theorem monPred_at_mono {P Q : MonPred I PROP} {i j : I.car} (h : P ⊢ Q) (hij : I.rel i j) :
+theorem monPred_at_mono {P Q : MonPred I PROP} {i j : I.car} (h : P ⊢ Q) (hij : I.rel.le i j) :
     P.monPred_at i ⊢ Q.monPred_at j :=
   (entails_at.mp h i).trans (Q.monPred_mono hij)
 
 @[rocq_alias monPred_at_flip_mono]
-theorem monPred_at_flip_mono {P Q : MonPred I PROP} {i j : I.car} (h : Q ⊢ P) (hij : I.rel j i) :
+theorem monPred_at_flip_mono {P Q : MonPred I PROP} {i j : I.car} (h : Q ⊢ P) (hij : I.rel.le j i) :
     Q.monPred_at j ⊢ P.monPred_at i :=
   monPred_at_mono h hij
 
@@ -849,12 +848,12 @@ instance monPred_affine (P : MonPred I PROP) [∀ i, Affine (P.monPred_at i)] :
 @[rocq_alias monPred_impl_force]
 theorem monPred_impl_force (i : I.car) (P Q : MonPred I PROP) :
     (iprop(P → Q) : MonPred I PROP).monPred_at i ⊢ iprop(P.monPred_at i → Q.monPred_at i) :=
-  (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))
+  (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))
 
 @[rocq_alias monPred_wand_force]
 theorem monPred_wand_force (i : I.car) (P Q : MonPred I PROP) :
     (iprop(P -∗ Q) : MonPred I PROP).monPred_at i ⊢ iprop(P.monPred_at i -∗ Q.monPred_at i) :=
-  (forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))
+  (forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))
 
 /-! ### The `monPred_in` assertion -/
 
@@ -862,7 +861,7 @@ theorem monPred_wand_force (i : I.car) (P Q : MonPred I PROP) :
 theorem monPred_in_intro (P : MonPred I PROP) :
     P ⊢ iprop(∃ i, MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤) :=
   entails_at.mpr fun j =>
-    (and_intro (pure_intro (Reflexive.refl : I.rel j j)) .rfl).trans <|
+    (and_intro (pure_intro (Std.Refl.refl j : I.rel.le j j)) .rfl).trans <|
       (exists_intro (Ψ := fun i =>
           (iprop(MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤) : MonPred I PROP).monPred_at j) j).trans
         (monPred_at_exist j fun i => iprop(MonPred.monPred_in i ∧ ⎡P.monPred_at i⎤)).mpr
@@ -871,36 +870,36 @@ theorem monPred_in_intro (P : MonPred I PROP) :
 theorem monPred_in_elim (P : MonPred I PROP) (i : I.car) :
     (MonPred.monPred_in i : MonPred I PROP) ⊢ iprop(⎡P.monPred_at i⎤ → P) :=
   entails_at.mpr fun j =>
-    pure_elim (I.rel i j) .rfl fun hij =>
+    pure_elim (I.rel.le i j) .rfl fun hij =>
       forall_intro fun _k => imp_intro_swap <| pure_elim_left fun hjk =>
-        imp_intro <| and_elim_r.trans (P.monPred_mono (Transitive.trans hij hjk))
+        imp_intro <| and_elim_r.trans (P.monPred_mono (Trans.trans hij hjk))
 
 @[rocq_alias monPred_in_mono]
-theorem monPred_in_mono {i j : I.car} (h : I.rel j i) :
+theorem monPred_in_mono {i j : I.car} (h : I.rel.le j i) :
     (MonPred.monPred_in i : MonPred I PROP) ⊢ MonPred.monPred_in j :=
-  entails_at.mpr fun _ => pure_mono fun hik => Transitive.trans h hik
+  entails_at.mpr fun _ => pure_mono fun hik => Trans.trans h hik
 
 #rocq_ignore monPred_in_proper "Use monPred_in_mono."
 
 @[rocq_alias monPred_in_flip_mono]
-theorem monPred_in_flip_mono {i j : I.car} (h : I.rel i j) :
+theorem monPred_in_flip_mono {i j : I.car} (h : I.rel.le i j) :
     (MonPred.monPred_in j : MonPred I PROP) ⊢ MonPred.monPred_in i :=
   monPred_in_mono h
 
 @[rocq_alias monPred_in_persistent]
 instance monPred_in_persistent (i : I.car) :
     Persistent (MonPred.monPred_in i : MonPred I PROP) where
-  persistent := entails_at.mpr fun j => (pure_persistent (I.rel i j)).persistent
+  persistent := entails_at.mpr fun j => (pure_persistent (I.rel.le i j)).persistent
 
 @[rocq_alias monPred_in_absorbing]
 instance monPred_in_absorbing (i : I.car) :
     Absorbing (MonPred.monPred_in i : MonPred I PROP) where
-  absorbing := entails_at.mpr fun j => (pure_absorbing (I.rel i j)).absorbing
+  absorbing := entails_at.mpr fun j => (pure_absorbing (I.rel.le i j)).absorbing
 
 @[rocq_alias monPred_in_timeless]
 instance monPred_in_timeless (i : I.car) :
     Timeless (MonPred.monPred_in i : MonPred I PROP) where
-  timeless := entails_at.mpr fun j => (pure_timeless (I.rel i j)).timeless
+  timeless := entails_at.mpr fun j => (pure_timeless (I.rel.le i j)).timeless
 
 /-! ### Objective predicates -/
 
@@ -944,7 +943,7 @@ instance impl_objective (P Q : MonPred I PROP) [Objective P] [Objective Q] :
     Objective (iprop(P → Q)) where
   objective_at i _j := forall_intro fun k => imp_intro <|
     and_elim_l.trans <|
-      (((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))) : _ ⊢@{PROP} _).trans <|
+      (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))) : _ ⊢@{PROP} _).trans <|
       imp_mono (Objective.objective_at k i) (Objective.objective_at i k)
 
 @[rocq_alias wand_objective]
@@ -952,7 +951,7 @@ instance wand_objective (P Q : MonPred I PROP) [Objective P] [Objective Q] :
     Objective (iprop(P -∗ Q)) where
   objective_at i _j := forall_intro fun k => imp_intro <|
     and_elim_l.trans <|
-      (((forall_elim i).trans (pure_imp_elim (Reflexive.refl : I.rel i i))) : _ ⊢@{PROP} _).trans <|
+      (((forall_elim i).trans (pure_imp_elim (Std.Refl.refl i : I.rel.le i i))) : _ ⊢@{PROP} _).trans <|
       wand_mono (Objective.objective_at k i) (Objective.objective_at i k)
 
 @[rocq_alias forall_objective]
@@ -1449,9 +1448,9 @@ instance instSbiMonPred : Sbi (MonPred I PROP) where
       monPred_impl_force i (iprop(⌜Ψi q⌝)) (SiPure.siPure q : MonPred I PROP)
   persistently_imp_siPure {P Q} := entails_at.mpr fun i => by
     refine (forall_elim i).trans ?_
-    refine (pure_imp_elim (Reflexive.refl : I.rel i i)).trans ?_
+    refine (pure_imp_elim (Std.Refl.refl i : I.rel.le i i)).trans ?_
     refine persistently_imp_siPure.trans (persistently_mono ?_)
-    refine forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel i j) => ?_
+    refine forall_intro fun j => imp_intro <| pure_elim_right fun (hij : I.rel.le i j) => ?_
     exact imp_mono_right (Q.monPred_mono hij)
   siPure_later {Pi} :=
     ⟨entails_at.mpr fun _ => siPure_later.mp, entails_at.mpr fun _ => siPure_later.mpr⟩
diff --git a/Iris/Iris/BI/SIProp.lean b/Iris/Iris/BI/SIProp.lean
index 219bc52fb..9b7e5b7fe 100644
--- a/Iris/Iris/BI/SIProp.lean
+++ b/Iris/Iris/BI/SIProp.lean
@@ -153,15 +153,16 @@ instance : BIBase SiProp where
 #rocq_ignore siProp_wand "Included in BIBase instance."
 #rocq_ignore siProp_persistently "Included in BIBase instance."
 
-instance : Std.Preorder (BIBase.Entails (PROP := SiProp)) where
-  refl _ h := h
-  trans h₁ h₂ n h := h₂ n (h₁ n h)
+instance siPropPreorder : Std.IsPreorder SiProp where
+  le_refl _ _ := id
+  le_trans _ _ _ h₁ h₂ n h := h₂ n (h₁ n h)
 
 /-! ## BI instance -/
 
 @[rocq_alias siPropI]
 instance instBI : BI SiProp where
-  entails_preorder := inferInstance
+  entails_refl := siPropPreorder.le_refl _
+  entails_trans := siPropPreorder.le_trans _ _ _
   equiv_iff.mp heq := ⟨fun n hP => (heq n .refl).mp hP, fun n hQ => (heq n .refl).mpr hQ⟩
   equiv_iff.mpr H _ _ _ := ⟨H.1 _, H.2 _⟩
   and_ne.ne _ _ _ h₁ _ _ h₂ m h := ⟨.imp (h₁ h).mp (h₂ h).mp, .imp (h₁ h).mpr (h₂ h).mpr⟩
diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean
index b696b2d27..f94174b15 100644
--- a/Iris/Iris/HeapLang/PrimitiveLaws.lean
+++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean
@@ -559,11 +559,12 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val ×
   · iapply HWPe; iexact Hp
   ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗
       ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _
-    by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe
+    by rw [wp_unfold.to_eq]) $$ HWPe
   cases obs using List.reverseRec with
   | nil =>
     ihave Hσ_e : iprop(stateInterp σ₁ ns ([] ++ obs') nt) $$ [Hheap Hpmap]
     · iapply (stateInterp_split σ₁ ns ([] ++ obs') nt).mpr; iframe Hheap; iexact Hpmap
+    simp only [wp.pre, hne]
     imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, _⟩
     imodintro
     isplitr
@@ -578,6 +579,7 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val ×
     ihave Hσ_e : iprop(stateInterp σ₁ ns (init ++ (lastObs :: obs')) nt) $$ [Hheap Hpmap]
     · iapply (stateInterp_split σ₁ ns (init ++ (lastObs :: obs')) nt).mpr
       iframe Hheap; rw [← hassoc]; iexact Hpmap
+    simp only [wp.pre, hne]
     imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, HWPe⟩
     imodintro
     isplitr
diff --git a/Iris/Iris/Instances/Classical/Instance.lean b/Iris/Iris/Instances/Classical/Instance.lean
index df8272d39..2e56b78f8 100644
--- a/Iris/Iris/Instances/Classical/Instance.lean
+++ b/Iris/Iris/Instances/Classical/Instance.lean
@@ -32,13 +32,11 @@ instance : BIBase (HeapProp Val) where
   persistently P _ := P ∅
   later P        σ := P σ
 
-instance : Std.Preorder (Entails (PROP := HeapProp Val)) where
-  refl := by
-    simp only [BI.Entails]
+instance heapPropPreorder : Std.IsPreorder (HeapProp Val) where
+  le_refl := by
     intro _ _ h
     exact h
-  trans := by
-    simp only [BI.Entails]
+  le_trans := by
     intro _ _ _ h_xy h_yz σ h_x
     apply h_yz σ
     apply h_xy σ
@@ -47,9 +45,10 @@ instance : Std.Preorder (Entails (PROP := HeapProp Val)) where
 instance : COFE (HeapProp Val) := COFE.ofDiscrete _
 
 instance : BI (HeapProp Val) where
-  entails_preorder := by infer_instance
+  entails_refl := heapPropPreorder.le_refl _
+  entails_trans := heapPropPreorder.le_trans _ _ _
   equiv_iff {P Q} := ⟨
-    fun h => h.to_eq ▸ ⟨refl, refl⟩,
+    fun h => h.to_eq ▸ ⟨Std.IsPreorder.le_refl P, Std.IsPreorder.le_refl P⟩,
     fun ⟨h₁, h₂⟩ => OFE.Equiv.of_eq (funext fun σ => propext ⟨h₁ σ, h₂ σ⟩)
   ⟩
 
diff --git a/Iris/Iris/Instances/UPred/Instance.lean b/Iris/Iris/Instances/UPred/Instance.lean
index 05c64c011..0749cad0b 100644
--- a/Iris/Iris/Instances/UPred/Instance.lean
+++ b/Iris/Iris/Instances/UPred/Instance.lean
@@ -266,9 +266,9 @@ instance : BIBase (UPred M) where
 #rocq_ignore uPred_primitive.uPred_unseal "No `Ltac unseal` rewrite is needed; nothing is sealed."
 
 @[rocq_alias uPred_primitive.entails_po]
-instance uPred_entails_preorder : Std.Preorder (Entails (PROP := UPred M)) where
-  refl _ _ H := H
-  trans H1 H2 _ _ Hv := H2 _ _ <| H1 _ _ Hv
+instance uPred_entails_preorder : Std.IsPreorder (UPred M) where
+  le_refl _ _ _ H := H
+  le_trans _ _ _ H1 H2 _ _ Hv := H2 _ _ <| H1 _ _ Hv
 
 @[rocq_alias uPred_primitive.entails_lim]
 theorem uPred_entails_lim {cP cQ : Chain (UPred M)} (H : ∀ n, cP n ⊢ cQ n) :
@@ -280,7 +280,8 @@ theorem uPred_entails_lim {cP cQ : Chain (UPred M)} (H : ∀ n, cP n ⊢ cQ n) :
 
 @[rocq_alias uPredI]
 instance : BI (UPred M) where
-  entails_preorder := inferInstance
+  entails_refl := uPred_entails_preorder.le_refl _
+  entails_trans := uPred_entails_preorder.le_trans _ _ _
   equiv_iff {_ _} := by
     constructor <;> intro HE
     · exact ⟨fun n ⟨x, Hv⟩ H => (HE n n x .refl Hv).mp H,
@@ -386,8 +387,8 @@ instance : BI (UPred M) where
     refine P.mono H ?_ .refl
     refine (incN_iff_right ?_).mpr (incN_refl _)
     exact (core_idem x.val).dist
-  persistently_emp_2 := Std.refl
-  persistently_and_2 := Std.refl
+  persistently_emp_2 := uPred_entails_preorder.le_refl emp
+  persistently_and_2 {P Q} := uPred_entails_preorder.le_refl iprop(<pers> P ∧ <pers> Q)
   persistently_sExists_1 _ _ := fun ⟨p, HΨ, H⟩ => by
     refine ⟨iprop(<pers> p), ⟨p, ?_⟩, H⟩
     ext; exact and_iff_right HΨ
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 0bff74e2a..4162147f4 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -862,7 +862,7 @@ instance elimModal_absorbingly_here [BI PROP] p (P Q : PROP) [Absorbing Q] :
 @[rocq_alias maybe_combine_sep_as_default]
 instance (priority := default - 20) combineSepAs_default [BI PROP] (P Q : PROP) :
     CombineSepAs P Q iprop(P ∗ Q) where
-  combine_sep_as := refl
+  combine_sep_as := by rfl
 
 @[rocq_alias maybe_combine_sep_as_affinely]
 instance combineSepAs_affinely [BI PROP] (Q1 Q2 P : PROP)
diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean
index dd2d8e25a..2e910208e 100644
--- a/Iris/Iris/ProofMode/Tactics/Combine.lean
+++ b/Iris/Iris/ProofMode/Tactics/Combine.lean
@@ -47,7 +47,7 @@ theorem combine_gives_step [BI PROP] {p1 p2 : Bool} {e e1 e2 out1 out2 out : PRO
     _ ⊢ (e2 ∗ □?p2 out2) ∗ □?p1 out1                     := sep_mono_left pf2.mp
     _ ⊢ e2 ∗ □?p2 out2 ∗ □?p1 out1                       := sep_assoc.mp
     _ ⊢ e2 ∗ □?p1 out1 ∗ □?p2 out2                       := sep_mono_right sep_comm.mp
-    _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ (e2 ∗ <pers> out) := and_intro refl <| sep_mono_right pf3
+    _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ (e2 ∗ <pers> out) := and_intro .rfl <| sep_mono_right pf3
     _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∧ <pers> out        := and_mono_right sep_elim_right
     _ ⊢ (e2 ∗ □?p1 out1 ∗ □?p2 out2) ∗ □ out             := persistently_and_intuitionistically_sep_right.mp
     _ ⊢ (e2 ∗ □?p2 out2 ∗ □?p1 out1) ∗ □ out             := sep_mono_left <| sep_mono_right sep_comm.mp
@@ -77,7 +77,7 @@ theorem combine_gives_step_conj [BI PROP] {p1 p2 : Bool}
     _ ⊢ <pers> newOutGives           := persistently_absorb_right
   calc
     _ ⊢ e ∗ □ outGives                                          := pf1
-    _ ⊢ (e ∗ □ outGives) ∧ <pers> outGives ∧ <pers> newOutGives := and_intro refl <| and_intro pf4 pf5
+    _ ⊢ (e ∗ □ outGives) ∧ <pers> outGives ∧ <pers> newOutGives := and_intro .rfl <| and_intro pf4 pf5
     _ ⊢ (e ∗ □ outGives) ∧ <pers> (outGives ∧ newOutGives)      := and_mono_right <| persistently_and.mpr
     _ ⊢ (e ∗ □ outGives) ∧ <pers> outGivesCombined              := and_mono_right <| persistently_mono instGivesCombined.make_and.mp
     _ ⊢ (e ∗ □ outGives) ∗ □ outGivesCombined                   := persistently_and_intuitionistically_sep_right.mp
diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean
index 3b147de3c..acec5521b 100644
--- a/Iris/Iris/Std/Classes.lean
+++ b/Iris/Iris/Std/Classes.lean
@@ -19,20 +19,6 @@ export Top (top)
 
 notation "⊤" => top
 
-/-- Require that a relation `R` on `a` is reflexive. -/
-class Reflexive (R : Relation α) where
-  refl {x : α} : R x x
-export Reflexive (refl)
-
-/-- Require that a relation `R` on `α` is transitive. -/
-class Transitive (R : Relation α) where
-  trans {x y z : α} : R x y → R y z → R x z
-export Transitive (trans)
-
-/-- Require that a relation `R` on `α` is a preorder, i.e. that it is reflexive and transitive. -/
-class Preorder (R : Relation α) extends Reflexive R, Transitive R
-
-
 /-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/
 class Idempotent (R : Relation α) (f : α → α → α) where
   idem {x : α} : R (f x x) x
diff --git a/Iris/Iris/Std/PartialMap.lean b/Iris/Iris/Std/PartialMap.lean
index a6033e573..5827e7075 100644
--- a/Iris/Iris/Std/PartialMap.lean
+++ b/Iris/Iris/Std/PartialMap.lean
@@ -8,7 +8,6 @@ module
 import Batteries.Data.List.Perm
 import Iris.Std.FromMathlib
 public import Iris.Std.GenSets
-public import Iris.Std.GenSets
 
 /-! ## Partial Maps
 
@@ -159,9 +158,11 @@ instance : SDiff (M V) := ⟨difference⟩
 /-- Two PartialMaps are pointwise equivalent. -/
 @[simp] def equiv (m1 m2 : M V) : Prop := ∀ k, get? m1 k = get? m2 k
 
-theorem equiv.refl : ∀ {a : M V}, equiv a a := by simp only [equiv, implies_true]
+@[simp,refl]
+theorem equiv.refl : ∀ a : M V, equiv a a := by simp only [equiv, implies_true]
 
-instance instEquivRefl : Reflexive (@equiv K V M _) := ⟨equiv.refl⟩
+instance instEquivRefl : Std.Refl (@equiv K V M _) where
+  refl := equiv.refl
 
 theorem equiv.trans : ∀ {a b c : M V}, equiv a b → equiv b c → equiv a c := by simp_all
 
diff --git a/Iris/Iris/Std/Rewrite.lean b/Iris/Iris/Std/Rewrite.lean
index 25d2794a2..4af1b3378 100644
--- a/Iris/Iris/Std/Rewrite.lean
+++ b/Iris/Iris/Std/Rewrite.lean
@@ -118,7 +118,8 @@ private partial def rewriteTMR
 where
   applyTransitivity (goal : MVarId) : TacticM <| Option <| MVarId × MVarId := do
     try
-      let some <| goalL :: goalR :: [] ← apply' goal ``trans
+      let some <| goalL :: goalR :: [] ← apply' goal (← `((Trans.trans :
+          ∀ {α} {r} [Trans r r r] {a b c : α}, r a b → r b c → r a c)))
         | return none
       return some (goalL, goalR)
     catch _ =>
@@ -127,7 +128,7 @@ where
   applyMonotonicity (goal : MVarId) : TacticM <| Option <| List MVarId := do
     for rule in (← getMonotonicityRules) do
       try
-        if let some goals ← apply' goal rule then
+        if let some goals ← apply' goal (mkCIdent rule) then
           return ← goals.mapM normalizeGoal
       catch _ =>
         continue
@@ -135,7 +136,7 @@ where
 
   applyReflexivity (goal : MVarId) : TacticM Unit := do
     try
-      discard <| apply' goal ``refl
+      discard <| apply' goal (← `(Std.Refl.refl))
     catch _ => pure ()
 
   go (goal : MVarId) (rule : TSyntax `term) : TacticM Bool := do
@@ -194,7 +195,7 @@ elab "rw' " "[" rules:rwRule',*,? "]" : tactic => do
   withoutRecover <| evalTactic (← `(tactic|
     try first
     | rfl
-    | exact refl
+    | exact Std.Refl.refl _
   ))
 
 end Iris.Std
diff --git a/Iris/Iris/Std/Tactic.lean b/Iris/Iris/Std/Tactic.lean
index b2da2bac0..4eed9fd64 100644
--- a/Iris/Iris/Std/Tactic.lean
+++ b/Iris/Iris/Std/Tactic.lean
@@ -13,13 +13,13 @@ public meta section
 namespace Iris.Std
 open Lean Lean.Elab.Tactic Lean.Meta
 
-/-- Apply the theorem with the name `name` to the goal `goal`. The flag `recover` is set to `false`
+/--
+Apply the theorem expressed by `term` to the goal `goal`. The flag `recover` is set to `false`
 and the transparency mode is set to `reducible`. Only non-dependent arguments of the applied
-theorem are turned into goals. -/
-def apply' (goal : MVarId) (name : Name) : TacticM <| Option <| List MVarId := do
-  unless (← getEnv).contains name do return none
-  let value ← mkConstWithFreshMVarLevels name   -- reference, not body; needs only the type
-
+theorem are turned into goals.
+-/
+def apply' (goal : MVarId) (term : Term) : TacticM <| Option <| List MVarId := do
+  let value ← goal.withContext <| elabTermForApply term
   let goals ← withoutRecover <| withReducible <| goal.apply value { newGoals := .nonDependentOnly }
   setGoals <| goals ++ (← getUnsolvedGoals)
   return goals