diff --git a/_CoqProject b/_CoqProject
index f01a9bc225191ea7c4f9cec35a2baf92f72ecdfa..fa1ddef99141584de06118ac55bc3556ea6927d9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,8 +44,8 @@ theories/si_logic/bi.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
-theories/bi/derived_laws_bi.v
-theories/bi/derived_laws_sbi.v
+theories/bi/derived_laws.v
+theories/bi/derived_laws_later.v
 theories/bi/plainly.v
 theories/bi/internal_eq.v
 theories/bi/big_op.v
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 9fde00f1a5c85fb916f191363ba4ef5ddf431a44..8f5aa1aa0fc72846c4cc3cd612ef2e95d2756b1e 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,9 +1,9 @@
-From iris.bi Require Export derived_laws_bi derived_laws_sbi big_op.
+From iris.bi Require Export derived_laws derived_laws_later big_op.
 From iris.bi Require Export updates internal_eq plainly embedding.
 Set Default Proof Using "Type".
 
 Module Import bi.
   Export bi.interface.bi.
-  Export bi.derived_laws_bi.bi.
-  Export bi.derived_laws_sbi.bi.
+  Export bi.derived_laws.bi.
+  Export bi.derived_laws_later.bi.
 End bi.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 4bb1940211dcc1cb9beceeb6b55e8026ce9341df..bfe5cd18466c1bcad8aefe1fcb868608b83d20a1 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,8 +1,8 @@
 From stdpp Require Import countable fin_sets functions.
-From iris.bi Require Import derived_laws_sbi.
+From iris.bi Require Import derived_laws_later.
 From iris.algebra Require Export big_op.
 Set Default Proof Using "Type".
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** Notations for unary variants *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 4a64793a0cc79df75d0f6564b205ee2216d61097..b6c10d542eddc892f94d3645be889c87a3015a6b 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -119,7 +119,7 @@ Notation "mP -∗? Q" := (bi_wandM mP Q)
 
 (** This class is required for the [iLöb] tactic. For most logics this class
 should not be inhabited directly, but the instance [Contractive (▷) → BiLöb PROP]
-in [derived_laws_sbi] should be used. A direct instance of the class is useful
+in [derived_laws_later] should be used. A direct instance of the class is useful
 when considering a BI logic with a discrete OFE, instead of a OFE that takes
 step-indexing of the logic in account.*)
 Class BiLöb (PROP : bi) :=
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws.v
similarity index 99%
rename from theories/bi/derived_laws_bi.v
rename to theories/bi/derived_laws.v
index 1127e290b4b9f33db6276c7f74b8d6b877c800b8..40641c9b975a54c79f0e2b5c1fe7298add4d6ff9 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws.v
@@ -10,7 +10,7 @@ From iris.algebra Require Import monoid.
 
 Module bi.
 Import interface.bi.
-Section bi_derived.
+Section derived.
 Context {PROP : bi}.
 Implicit Types φ : Prop.
 Implicit Types P Q R : PROP.
@@ -1551,5 +1551,5 @@ Qed.
 Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP) :
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
-End bi_derived.
+End derived.
 End bi.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_later.v
similarity index 99%
rename from theories/bi/derived_laws_sbi.v
rename to theories/bi/derived_laws_later.v
index 19bafd7bfde2abab9adff074be32961ce5b47cc3..7f3d4bd4e93b9a0d60a7f2cef929fb4be8622e58 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,10 +1,11 @@
-From iris.bi Require Export derived_laws_bi.
+From iris.bi Require Export derived_laws.
 From iris.algebra Require Import monoid.
 
 Module bi.
 Import interface.bi.
-Import derived_laws_bi.bi.
-Section sbi_derived.
+Import derived_laws.bi.
+
+Section later_derived.
 Context {PROP : bi}.
 Implicit Types φ : Prop.
 Implicit Types P Q R : PROP.
@@ -398,5 +399,5 @@ Proof. split; try apply _. apply laterN_intro. Qed.
 Global Instance bi_except_0_sep_entails_homomorphism :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_except_0 PROP).
 Proof. split; try apply _. apply except_0_intro. Qed.
-End sbi_derived.
+End later_derived.
 End bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 24f4c237f29151889720cc74c3656b67cc75e8e8..9862bcd959f05e81187e958f753729ccb387388f 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import interface derived_laws_sbi big_op.
+From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.algebra Require Import monoid.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 5a460db1ca45961fad65dd39457c41e327478644..c0044e908c5eecde2697d9c080af039c8194d1b4 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -121,7 +121,7 @@ Section bi_mixin.
   identity function, as the Löb axiom or contractiveness of later is not part of
   [BiLaterMixin]. For step-indexed BIs one should separately prove an instance
   of the class [BiLöb PROP] or [Contractive (▷)]. (Note that there is an
-  instance [Contractive (▷) → BiLöb PROP] in [derived_laws_sbi].)
+  instance [Contractive (▷) → BiLöb PROP] in [derived_laws_later].)
 
   For non step-indexed BIs one can get a "free" instance of [BiLaterMixin] using
   the smart constructor [bi_later_mixin_id] below. *)
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 6e97b92e65b31f04af244213095d902e2788b051..6ecd8ec6f4a8cca9bd468c85124b177d36e471ee 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -1,5 +1,5 @@
-From iris.bi Require Import derived_laws_sbi big_op.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+From iris.bi Require Import derived_laws_later big_op.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** This file defines a type class for BIs with a notion of internal equality.
 Internal equality is not part of the [bi] canonical structure as [internal_eq]
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index f99e4b68a5c74ec6909a8ca971caa2ca2f27a72e..a5b5af0210bf293e7b5abf9ac2c7cf67c656cf2c 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,6 +1,6 @@
-From iris.bi Require Import derived_laws_sbi big_op internal_eq.
+From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.algebra Require Import monoid.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 Class Plainly (A : Type) := plainly : A → A.
 Hint Mode Plainly ! : typeclass_instances.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 7b2498dafe59a76bb95e473b08da7b811b664722..51f54aa594416bc12dfbfd5497455cb50f101db5 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,6 +1,6 @@
 From stdpp Require Import coPset.
-From iris.bi Require Import interface derived_laws_sbi big_op plainly.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+From iris.bi Require Import interface derived_laws_later big_op plainly.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (* We first define operational type classes for the notations, and then later
 bundle these operational type classes with the laws. *)