diff --git a/_CoqProject b/_CoqProject
index 8b92bf43d222c4576183e23b4bc6a1b13f745f4a..1211cbed0529c738bdb43a0fe4613700e3149d70 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -26,7 +26,8 @@ theories/algebra/coPset.v
 theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/bi/interface.v
-theories/bi/derived.v
+theories/bi/derived_connectives.v
+theories/bi/derived_laws.v
 theories/bi/big_op.v
 theories/bi/bi.v
 theories/bi/tactics.v
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 09441f1496b5febde2cc75b45cbc228b9a453a55..829788b85e7fff596535ba78967837bd7d60cd17 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,8 +1,8 @@
 From iris.base_logic Require Export upred.
-From iris.bi Require Export interface derived.
+From iris.bi Require Export derived_laws.
 Set Default Proof Using "Type".
 Import upred.uPred.
-Import interface.bi derived.bi.
+Import interface.bi derived_laws.bi.
 
 Module uPred.
 Section derived.
@@ -31,10 +31,6 @@ Proof.
   apply limit_preserving_and; by apply limit_preserving_entails.
 Qed.
 
-(* Affine *)
-Global Instance uPred_affine : AffineBI (uPredI M) | 0.
-Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
-
 (* Own and valid derived *)
 Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
   ✓ a ⊢ bi_persistently (✓ a : uPred M).
@@ -131,6 +127,6 @@ Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 
 (* Also add this to the global hint database, otherwise [eauto] won't work for
-many lemmas that have [AffineBI] as a premise. *)
+many lemmas that have [BiAffine] as a premise. *)
 Hint Immediate uPred_affine.
 End uPred.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index f8a5aea4c83b6f3d838455f118c9f3e623c2be6f..f78d85f128c83b8d0f1b49dc88a6b23f1141b250 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra updates.
-From iris.bi Require Export interface.
+From iris.bi Require Export derived_connectives.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
@@ -608,10 +608,13 @@ Proof.
 Qed.
 Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_proper _.
 
-(** PlainlyExist1BI *)
+(** BI instances *)
 
-Global Instance uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
-Proof. unfold PlainlyExist1BI. by unseal. Qed.
+Global Instance uPred_affine : BiAffine (uPredI M) | 0.
+Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
+
+Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredI M).
+Proof. unfold BiPlainlyExist. by unseal. Qed.
 
 (** Limits *)
 Lemma entails_lim (cP cQ : chain (uPredC M)) :
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index f4c5f8fc6f5c07972946c9d2b7af8d3351350853..8e90d845f18483d4895004e58ec0c4fe5652082d 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,9 +1,9 @@
-From iris.bi Require Export interface derived big_op.
+From iris.bi Require Export derived_laws big_op.
 Set Default Proof Using "Type".
 
 Module Import bi.
   Export bi.interface.bi.
-  Export bi.derived.bi.
+  Export bi.derived_laws.bi.
   Export bi.big_op.bi.
 End bi.
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index aba95a69c699e02f77b5ec326ad120e8521a75de..3472d004e2a2af15305b93e0d33de27ba92dbedb 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export big_op.
-From iris.bi Require Export derived.
+From iris.bi Require Export derived_laws.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
 
@@ -41,7 +41,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
 
 (** * Properties *)
 Module bi.
-Import interface.bi derived.bi.
+Import interface.bi derived_laws.bi.
 Section bi_big_op.
 Context {PROP : bi}.
 Implicit Types Ps Qs : list PROP.
@@ -55,7 +55,7 @@ Section sep_list.
 
   Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ emp.
   Proof. done. Qed.
-  Lemma big_sepL_nil' `{AffineBI PROP} P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
+  Lemma big_sepL_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
   Proof. apply (affine _). Qed.
   Lemma big_sepL_cons Φ x l :
     ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y.
@@ -75,7 +75,7 @@ Section sep_list.
     (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
     ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∗ list] k ↦ y ∈ l, Ψ k y).
   Proof. apply big_opL_proper. Qed.
-  Lemma big_sepL_submseteq `{AffineBI PROP} (Φ : A → PROP) l1 l2 :
+  Lemma big_sepL_submseteq `{BiAffine PROP} (Φ : A → PROP) l1 l2 :
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
   Proof.
     intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
@@ -125,16 +125,16 @@ Section sep_list.
     ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x).
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepL_plainly `{AffineBI PROP} Φ l :
+  Lemma big_sepL_plainly `{BiAffine PROP} Φ l :
     bi_plainly ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, bi_plainly (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
+  Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
     bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢
     [∗ list] k↦x ∈ l, bi_persistently (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_sepL_forall `{AffineBI PROP} Φ l :
+  Lemma big_sepL_forall `{BiAffine PROP} Φ l :
     (∀ k x, Persistent (Φ k x)) →
     ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
@@ -287,7 +287,7 @@ Section and_list.
     [∧ list] k↦x ∈ l, bi_persistently (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_andL_forall `{AffineBI PROP} Φ l :
+  Lemma big_andL_forall `{BiAffine PROP} Φ l :
     ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
     apply (anti_symm _).
@@ -328,7 +328,7 @@ Section gmap.
     (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x).
   Proof. apply big_opM_proper. Qed.
-  Lemma big_sepM_subseteq `{AffineBI PROP} Φ m1 m2 :
+  Lemma big_sepM_subseteq `{BiAffine PROP} Φ m1 m2 :
     m2 ⊆ m1 → ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Φ k x.
   Proof. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
 
@@ -339,7 +339,7 @@ Section gmap.
 
   Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ emp.
   Proof. by rewrite big_opM_empty. Qed.
-  Lemma big_sepM_empty' `{AffineBI PROP} P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x.
+  Lemma big_sepM_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x.
   Proof. rewrite big_sepM_empty. apply: affine. Qed.
 
   Lemma big_sepM_insert Φ m i x :
@@ -420,16 +420,16 @@ Section gmap.
     ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x).
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepM_plainly `{AffineBI PROP} Φ m :
+  Lemma big_sepM_plainly `{BiAffine PROP} Φ m :
     bi_plainly ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, bi_plainly (Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
+  Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
     (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
       ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM_forall `{AffineBI PROP} Φ m :
+  Lemma big_sepM_forall `{BiAffine PROP} Φ m :
     (∀ k x, Persistent (Φ k x)) →
     ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
   Proof.
@@ -499,7 +499,7 @@ Section gset.
     (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
     ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x).
   Proof. apply big_opS_proper. Qed.
-  Lemma big_sepS_subseteq `{AffineBI PROP} Φ X Y :
+  Lemma big_sepS_subseteq `{BiAffine PROP} Φ X Y :
     Y ⊆ X → ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Φ x.
   Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
 
@@ -509,7 +509,7 @@ Section gset.
 
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opS_empty. Qed.
-  Lemma big_sepS_empty' `{!AffineBI PROP} P Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
+  Lemma big_sepS_empty' `{!BiAffine PROP} P Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
   Proof. rewrite big_sepS_empty. apply: affine. Qed.
 
   Lemma big_sepS_insert Φ X x :
@@ -575,12 +575,12 @@ Section gset.
     by apply sep_mono_r, wand_intro_l.
   Qed.
 
-  Lemma big_sepS_filter `{AffineBI PROP}
+  Lemma big_sepS_filter `{BiAffine PROP}
       (P : A → Prop) `{∀ x, Decision (P x)} Φ X :
     ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y).
   Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.
 
-  Lemma big_sepS_filter_acc `{AffineBI PROP}
+  Lemma big_sepS_filter_acc `{BiAffine PROP}
       (P : A → Prop) `{∀ y, Decision (P y)} Φ X Y :
     (∀ y, y ∈ Y → P y → y ∈ X) →
     ([∗ set] y ∈ X, Φ y) -∗
@@ -596,15 +596,15 @@ Section gset.
     ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepS_plainly `{AffineBI PROP} Φ X :
+  Lemma big_sepS_plainly `{BiAffine PROP} Φ X :
     bi_plainly ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_plainly (Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
-  Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
+  Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
     bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
-  Lemma big_sepS_forall `{AffineBI PROP} Φ X :
+  Lemma big_sepS_forall `{BiAffine PROP} Φ X :
     (∀ x, Persistent (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
     intros. apply (anti_symm _).
@@ -671,7 +671,7 @@ Section gmultiset.
     (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
     ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x ∈ X, Ψ x).
   Proof. apply big_opMS_proper. Qed.
-  Lemma big_sepMS_subseteq `{AffineBI PROP} Φ X Y :
+  Lemma big_sepMS_subseteq `{BiAffine PROP} Φ X Y :
     Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x.
   Proof. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
 
@@ -681,7 +681,7 @@ Section gmultiset.
 
   Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opMS_empty. Qed.
-  Lemma big_sepMS_empty' `{!AffineBI PROP} P Φ : P ⊢ [∗ mset] x ∈ ∅, Φ x.
+  Lemma big_sepMS_empty' `{!BiAffine PROP} P Φ : P ⊢ [∗ mset] x ∈ ∅, Φ x.
   Proof. rewrite big_sepMS_empty. apply: affine. Qed.
 
   Lemma big_sepMS_union Φ X Y :
@@ -714,11 +714,11 @@ Section gmultiset.
     ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepMS_plainly `{AffineBI PROP} Φ X :
+  Lemma big_sepMS_plainly `{BiAffine PROP} Φ X :
     bi_plainly ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, bi_plainly (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
+  Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
     bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
       [∗ mset] y ∈ X, bi_persistently (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
@@ -756,11 +756,11 @@ Section list.
   Implicit Types l : list A.
   Implicit Types Φ Ψ : nat → A → PROP.
 
-  Lemma big_sepL_later `{AffineBI PROP} Φ l :
+  Lemma big_sepL_later `{BiAffine PROP} Φ l :
     ▷ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷ Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_sepL_laterN `{AffineBI PROP} Φ n l :
+  Lemma big_sepL_laterN `{BiAffine PROP} Φ n l :
     ▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
@@ -781,11 +781,11 @@ Section gmap.
   Implicit Types m : gmap K A.
   Implicit Types Φ Ψ : K → A → PROP.
 
-  Lemma big_sepM_later `{AffineBI PROP} Φ m :
+  Lemma big_sepM_later `{BiAffine PROP} Φ m :
     ▷ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷ Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
-  Lemma big_sepM_laterN `{AffineBI PROP} Φ n m :
+  Lemma big_sepM_laterN `{BiAffine PROP} Φ n m :
     ▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
   Proof. apply (big_opM_commute _). Qed.
 
@@ -803,11 +803,11 @@ Section gset.
   Implicit Types X : gset A.
   Implicit Types Φ : A → PROP.
 
-  Lemma big_sepS_later `{AffineBI PROP} Φ X :
+  Lemma big_sepS_later `{BiAffine PROP} Φ X :
     ▷ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷ Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
-  Lemma big_sepS_laterN `{AffineBI PROP} Φ n X :
+  Lemma big_sepS_laterN `{BiAffine PROP} Φ n X :
     ▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
@@ -825,11 +825,11 @@ Section gmultiset.
   Implicit Types X : gmultiset A.
   Implicit Types Φ : A → PROP.
 
-  Lemma big_sepMS_later `{AffineBI PROP} Φ X :
+  Lemma big_sepMS_later `{BiAffine PROP} Φ X :
     ▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Lemma big_sepMS_laterN `{AffineBI PROP} Φ n X :
+  Lemma big_sepMS_laterN `{BiAffine PROP} Φ n X :
     ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
diff --git a/theories/bi/counter_examples.v b/theories/bi/counter_examples.v
index d3410120a3e53f165a9538715780da86f617f7f4..e3e1214d3d28d2affebd7ad17f6c37ee93b43bb1 100644
--- a/theories/bi/counter_examples.v
+++ b/theories/bi/counter_examples.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type*".
 (** This proves that we need the â–· in a "Saved Proposition" construction with
 name-dependent allocation. *)
 Module savedprop. Section savedprop.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
   Notation "¬ P" := (□ (P → False))%I : bi_scope.
   Implicit Types P : PROP.
 
@@ -65,7 +65,7 @@ End savedprop. End savedprop.
 
 (** This proves that we need the â–· when opening invariants. *)
 Module inv. Section inv.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
   Implicit Types P : PROP.
 
   (** Assumptions *)
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
new file mode 100644
index 0000000000000000000000000000000000000000..d3fe0fab587ddf13f8eddaba7a6d7d978fbca0f9
--- /dev/null
+++ b/theories/bi/derived_connectives.v
@@ -0,0 +1,116 @@
+From iris.bi Require Export interface.
+From iris.algebra Require Import monoid.
+From stdpp Require Import hlist.
+
+Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
+Arguments bi_iff {_} _%I _%I : simpl never.
+Instance: Params (@bi_iff) 1.
+Infix "↔" := bi_iff : bi_scope.
+
+Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
+  ((P -∗ Q) ∧ (Q -∗ P))%I.
+Arguments bi_wand_iff {_} _%I _%I : simpl never.
+Instance: Params (@bi_wand_iff) 1.
+Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
+
+Class Plain {PROP : bi} (P : PROP) := plain : P ⊢ bi_plainly P.
+Arguments Plain {_} _%I : simpl never.
+Arguments plain {_} _%I {_}.
+Hint Mode Plain + ! : typeclass_instances.
+Instance: Params (@Plain) 1.
+
+Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
+Arguments Persistent {_} _%I : simpl never.
+Arguments persistent {_} _%I {_}.
+Hint Mode Persistent + ! : typeclass_instances.
+Instance: Params (@Persistent) 1.
+
+Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
+Arguments bi_affinely {_} _%I : simpl never.
+Instance: Params (@bi_affinely) 1.
+Typeclasses Opaque bi_affinely.
+Notation "â–¡ P" := (bi_affinely (bi_persistently P))%I
+  (at level 20, right associativity) : bi_scope.
+Notation "â–  P" := (bi_affinely (bi_plainly P))%I
+  (at level 20, right associativity) : bi_scope.
+
+Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
+Arguments Affine {_} _%I : simpl never.
+Arguments affine {_} _%I {_}.
+Hint Mode Affine + ! : typeclass_instances.
+
+Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
+Existing Instance absorbing_bi | 0.
+
+Class BiPositive (PROP : bi) :=
+  bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
+
+Class BiPlainlyExist (PROP : bi) :=
+  plainly_exist_1 A (Ψ : A → PROP) :
+    bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a).
+Arguments plainly_exist_1 _ {_ _} _.
+
+Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
+Arguments bi_absorbingly {_} _%I : simpl never.
+Instance: Params (@bi_absorbingly) 1.
+Typeclasses Opaque bi_absorbingly.
+
+Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P.
+Arguments Absorbing {_} _%I : simpl never.
+Arguments absorbing {_} _%I.
+
+Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then bi_plainly P else P)%I.
+Arguments bi_plainly_if {_} !_ _%I /.
+Instance: Params (@bi_plainly_if) 2.
+Typeclasses Opaque bi_plainly_if.
+
+Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then bi_persistently P else P)%I.
+Arguments bi_persistently_if {_} !_ _%I /.
+Instance: Params (@bi_persistently_if) 2.
+Typeclasses Opaque bi_persistently_if.
+
+Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then bi_affinely P else P)%I.
+Arguments bi_affinely_if {_} !_ _%I /.
+Instance: Params (@bi_affinely_if) 2.
+Typeclasses Opaque bi_affinely_if.
+Notation "â–¡? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "â–¡? p  P") : bi_scope.
+Notation "â– ? p P" := (bi_affinely_if p (bi_plainly_if p P))%I
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "â– ? p  P") : bi_scope.
+
+Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
+  match As return himpl As PROP → PROP with
+  | tnil => id
+  | tcons A As => λ Φ, ∃ x, bi_hexist (Φ x)
+  end%I.
+Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
+  match As return himpl As PROP → PROP with
+  | tnil => id
+  | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x)
+  end%I.
+
+Definition bi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
+  Nat.iter n bi_later P.
+Arguments bi_laterN {_} !_%nat_scope _%I.
+Instance: Params (@bi_laterN) 2.
+Notation "â–·^ n P" := (bi_laterN n P)
+  (at level 20, n at level 9, P at level 20, format "â–·^ n  P") : bi_scope.
+Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P)
+  (at level 20, p at level 9, P at level 20, format "â–·? p  P") : bi_scope.
+
+Definition bi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
+Arguments bi_except_0 {_} _%I : simpl never.
+Notation "â—‡ P" := (bi_except_0 P) (at level 20, right associativity) : bi_scope.
+Instance: Params (@bi_except_0) 1.
+Typeclasses Opaque bi_except_0.
+
+Class Timeless {PROP : sbi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
+Arguments Timeless {_} _%I : simpl never.
+Arguments timeless {_} _%I {_}.
+Hint Mode Timeless + ! : typeclass_instances.
+Instance: Params (@Timeless) 1.
diff --git a/theories/bi/derived.v b/theories/bi/derived_laws.v
similarity index 93%
rename from theories/bi/derived.v
rename to theories/bi/derived_laws.v
index 7d8e53b00414652db494d30429a82eedc217909b..a3f10be7f2635320ed9ca5c1fa2831badd4dd90e 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived_laws.v
@@ -1,115 +1,7 @@
-From iris.bi Require Export interface.
+From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
 From stdpp Require Import hlist.
 
-Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
-Arguments bi_iff {_} _%I _%I : simpl never.
-Instance: Params (@bi_iff) 1.
-Infix "↔" := bi_iff : bi_scope.
-
-Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
-  ((P -∗ Q) ∧ (Q -∗ P))%I.
-Arguments bi_wand_iff {_} _%I _%I : simpl never.
-Instance: Params (@bi_wand_iff) 1.
-Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
-
-Class Plain {PROP : bi} (P : PROP) := plain : P ⊢ bi_plainly P.
-Arguments Plain {_} _%I : simpl never.
-Arguments plain {_} _%I {_}.
-Hint Mode Plain + ! : typeclass_instances.
-Instance: Params (@Plain) 1.
-
-Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
-Arguments Persistent {_} _%I : simpl never.
-Arguments persistent {_} _%I {_}.
-Hint Mode Persistent + ! : typeclass_instances.
-Instance: Params (@Persistent) 1.
-
-Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
-Arguments bi_affinely {_} _%I : simpl never.
-Instance: Params (@bi_affinely) 1.
-Typeclasses Opaque bi_affinely.
-Notation "â–¡ P" := (bi_affinely (bi_persistently P))%I
-  (at level 20, right associativity) : bi_scope.
-Notation "â–  P" := (bi_affinely (bi_plainly P))%I
-  (at level 20, right associativity) : bi_scope.
-
-Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
-Arguments Affine {_} _%I : simpl never.
-Arguments affine {_} _%I {_}.
-Hint Mode Affine + ! : typeclass_instances.
-
-Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
-Existing Instance absorbing_bi | 0.
-
-Class PositiveBI (PROP : bi) :=
-  positive_bi (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
-
-Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
-Arguments bi_absorbingly {_} _%I : simpl never.
-Instance: Params (@bi_absorbingly) 1.
-Typeclasses Opaque bi_absorbingly.
-
-Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P.
-Arguments Absorbing {_} _%I : simpl never.
-Arguments absorbing {_} _%I.
-
-Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_plainly P else P)%I.
-Arguments bi_plainly_if {_} !_ _%I /.
-Instance: Params (@bi_plainly_if) 2.
-Typeclasses Opaque bi_plainly_if.
-
-Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_persistently P else P)%I.
-Arguments bi_persistently_if {_} !_ _%I /.
-Instance: Params (@bi_persistently_if) 2.
-Typeclasses Opaque bi_persistently_if.
-
-Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_affinely P else P)%I.
-Arguments bi_affinely_if {_} !_ _%I /.
-Instance: Params (@bi_affinely_if) 2.
-Typeclasses Opaque bi_affinely_if.
-Notation "â–¡? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "â–¡? p  P") : bi_scope.
-Notation "â– ? p P" := (bi_affinely_if p (bi_plainly_if p P))%I
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "â– ? p  P") : bi_scope.
-
-Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
-  match As return himpl As PROP → PROP with
-  | tnil => id
-  | tcons A As => λ Φ, ∃ x, bi_hexist (Φ x)
-  end%I.
-Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
-  match As return himpl As PROP → PROP with
-  | tnil => id
-  | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x)
-  end%I.
-
-Definition bi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
-  Nat.iter n bi_later P.
-Arguments bi_laterN {_} !_%nat_scope _%I.
-Instance: Params (@bi_laterN) 2.
-Notation "â–·^ n P" := (bi_laterN n P)
-  (at level 20, n at level 9, P at level 20, format "â–·^ n  P") : bi_scope.
-Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P)
-  (at level 20, p at level 9, P at level 20, format "â–·? p  P") : bi_scope.
-
-Definition bi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
-Arguments bi_except_0 {_} _%I : simpl never.
-Notation "â—‡ P" := (bi_except_0 P) (at level 20, right associativity) : bi_scope.
-Instance: Params (@bi_except_0) 1.
-Typeclasses Opaque bi_except_0.
-
-Class Timeless {PROP : sbi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
-Arguments Timeless {_} _%I : simpl never.
-Arguments timeless {_} _%I {_}.
-Hint Mode Timeless + ! : typeclass_instances.
-Instance: Params (@Timeless) 1.
-
 Module bi.
 Import interface.bi.
 Section bi_derived.
@@ -732,11 +624,11 @@ Proof.
   - by rewrite !and_elim_l right_id.
   - by rewrite !and_elim_r.
 Qed.
-Lemma affinely_sep `{PositiveBI PROP} P Q :
+Lemma affinely_sep `{BiPositive PROP} P Q :
   bi_affinely (P ∗ Q) ⊣⊢ bi_affinely P ∗ bi_affinely Q.
 Proof.
   apply (anti_symm _), affinely_sep_2.
-  by rewrite -{1}affinely_idemp positive_bi !(comm _ (bi_affinely P)%I) positive_bi.
+  by rewrite -{1}affinely_idemp bi_positive !(comm _ (bi_affinely P)%I) bi_positive.
 Qed.
 Lemma affinely_forall {A} (Φ : A → PROP) :
   bi_affinely (∀ a, Φ a) ⊢ ∀ a, bi_affinely (Φ a).
@@ -815,7 +707,7 @@ Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
 Lemma absorbingly_sep_lr P Q : bi_absorbingly P ∗ Q ⊣⊢ P ∗ bi_absorbingly Q.
 Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
 
-Lemma affinely_absorbingly `{!PositiveBI PROP} P :
+Lemma affinely_absorbingly `{!BiPositive PROP} P :
   bi_affinely (bi_absorbingly P) ⊣⊢ bi_affinely P.
 Proof.
   apply (anti_symm _), affinely_mono, absorbingly_intro.
@@ -875,12 +767,12 @@ Proof. apply (anti_symm _); auto using True_sep_2. Qed.
 Lemma sep_True P `{!Absorbing P} : P ∗ True ⊣⊢ P.
 Proof. by rewrite comm True_sep. Qed.
 
-Section affine_bi.
-  Context `{AffineBI PROP}.
+Section bi_affine.
+  Context `{BiAffine PROP}.
 
-  Global Instance affine_bi_absorbing P : Absorbing P | 0.
+  Global Instance bi_affine_absorbing P : Absorbing P | 0.
   Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
-  Global Instance affine_bi_positive : PositiveBI PROP.
+  Global Instance bi_affine_positive : BiPositive PROP.
   Proof. intros P Q. by rewrite !affine_affinely. Qed.
 
   Lemma True_emp : True ⊣⊢ emp.
@@ -906,7 +798,7 @@ Section affine_bi.
     - by rewrite pure_True // True_impl.
     - by rewrite pure_False // False_impl True_emp.
   Qed.
-End affine_bi.
+End bi_affine.
 
 (* Properties of the persistence modality *)
 Hint Resolve persistently_mono.
@@ -1044,7 +936,7 @@ Qed.
 Lemma persistently_sep_2 P Q :
   bi_persistently P ∗ bi_persistently Q ⊢ bi_persistently (P ∗ Q).
 Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
-Lemma persistently_sep `{PositiveBI PROP} P Q :
+Lemma persistently_sep `{BiPositive PROP} P Q :
   bi_persistently (P ∗ Q) ⊣⊢ bi_persistently P ∗ bi_persistently Q.
 Proof.
   apply (anti_symm _); auto using persistently_sep_2.
@@ -1076,7 +968,7 @@ Lemma impl_wand_persistently_2 P Q : (bi_persistently P -∗ Q) ⊢ (bi_persiste
 Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
 
 Section persistently_affinely_bi.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
 
   Lemma persistently_emp : bi_persistently emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp persistently_pure. Qed.
@@ -1186,14 +1078,14 @@ Qed.
 Lemma plainly_exist_2 {A} (Ψ : A → PROP) :
   (∃ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∃ a, Ψ a).
 Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed.
-Lemma plainly_exist `{PlainlyExist1BI PROP} {A} (Ψ : A → PROP) :
+Lemma plainly_exist `{BiPlainlyExist PROP} {A} (Ψ : A → PROP) :
   bi_plainly (∃ a, Ψ a) ⊣⊢ ∃ a, bi_plainly (Ψ a).
 Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed.
 Lemma plainly_and P Q : bi_plainly (P ∧ Q) ⊣⊢ bi_plainly P ∧ bi_plainly Q.
 Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
 Lemma plainly_or_2 P Q : bi_plainly P ∨ bi_plainly Q ⊢ bi_plainly (P ∨ Q).
 Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed.
-Lemma plainly_or `{PlainlyExist1BI PROP} P Q :
+Lemma plainly_or `{BiPlainlyExist PROP} P Q :
   bi_plainly (P ∨ Q) ⊣⊢ bi_plainly P ∨ bi_plainly Q.
 Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
 Lemma plainly_impl P Q : bi_plainly (P → Q) ⊢ bi_plainly P → bi_plainly Q.
@@ -1246,7 +1138,7 @@ Qed.
 Lemma plainly_sep_2 P Q :
   bi_plainly P ∗ bi_plainly Q ⊢ bi_plainly (P ∗ Q).
 Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
-Lemma plainly_sep `{PositiveBI PROP} P Q :
+Lemma plainly_sep `{BiPositive PROP} P Q :
   bi_plainly (P ∗ Q) ⊣⊢ bi_plainly P ∗ bi_plainly Q.
 Proof.
   apply (anti_symm _); auto using plainly_sep_2.
@@ -1274,7 +1166,7 @@ Lemma impl_wand_plainly_2 P Q : (bi_plainly P -∗ Q) ⊢ (bi_plainly P → Q).
 Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
 
 Section plainly_affinely_bi.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
 
   Lemma plainly_emp : bi_plainly emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp plainly_pure. Qed.
@@ -1319,7 +1211,7 @@ Lemma affinely_persistently_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣
 Proof. by rewrite persistently_exist affinely_exist. Qed.
 Lemma affinely_persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
 Proof. by rewrite affinely_sep_2 persistently_sep_2. Qed.
-Lemma affinely_persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma affinely_persistently_sep `{BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
 Proof. by rewrite -affinely_sep -persistently_sep. Qed.
 
 Lemma affinely_persistently_idemp P : □ □ P ⊣⊢ □ P.
@@ -1367,16 +1259,16 @@ Lemma affinely_plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
 Proof. by rewrite plainly_and affinely_and. Qed.
 Lemma affinely_plainly_or_2 P Q : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q).
 Proof. by rewrite -plainly_or_2 affinely_or. Qed.
-Lemma affinely_plainly_or `{PlainlyExist1BI PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+Lemma affinely_plainly_or `{BiPlainlyExist PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
 Proof. by rewrite plainly_or affinely_or. Qed.
 Lemma affinely_plainly_exist_2 {A} (Φ : A → PROP) : (∃ x, ■ Φ x) ⊢ ■ (∃ x, Φ x).
 Proof. by rewrite -plainly_exist_2 affinely_exist. Qed.
-Lemma affinely_plainly_exist `{PlainlyExist1BI PROP} {A} (Φ : A → PROP) :
+Lemma affinely_plainly_exist `{BiPlainlyExist PROP} {A} (Φ : A → PROP) :
   ■ (∃ x, Φ x) ⊣⊢ ∃ x, ■ Φ x.
 Proof. by rewrite plainly_exist affinely_exist. Qed.
 Lemma affinely_plainly_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
 Proof. by rewrite affinely_sep_2 plainly_sep_2. Qed.
-Lemma affinely_plainly_sep `{PositiveBI PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Lemma affinely_plainly_sep `{BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
 Proof. by rewrite -affinely_sep -plainly_sep. Qed.
 
 Lemma affinely_plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
@@ -1435,7 +1327,7 @@ Proof. destruct p; simpl; auto using affinely_exist. Qed.
 Lemma affinely_if_sep_2 p P Q :
   bi_affinely_if p P ∗ bi_affinely_if p Q ⊢ bi_affinely_if p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_sep_2. Qed.
-Lemma affinely_if_sep `{PositiveBI PROP} p P Q :
+Lemma affinely_if_sep `{BiPositive PROP} p P Q :
   bi_affinely_if p (P ∗ Q) ⊣⊢ bi_affinely_if p P ∗ bi_affinely_if p Q.
 Proof. destruct p; simpl; auto using affinely_sep. Qed.
 
@@ -1474,7 +1366,7 @@ Proof. destruct p; simpl; auto using persistently_exist. Qed.
 Lemma persistently_if_sep_2 p P Q :
   bi_persistently_if p P ∗ bi_persistently_if p Q ⊢ bi_persistently_if p (P ∗ Q).
 Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
-Lemma persistently_if_sep `{PositiveBI PROP} p P Q :
+Lemma persistently_if_sep `{BiPositive PROP} p P Q :
   bi_persistently_if p (P ∗ Q) ⊣⊢ bi_persistently_if p P ∗ bi_persistently_if p Q.
 Proof. destruct p; simpl; auto using persistently_sep. Qed.
 
@@ -1504,7 +1396,7 @@ Lemma affinely_persistently_if_exist {A} p (Ψ : A → PROP) :
 Proof. destruct p; simpl; auto using affinely_persistently_exist. Qed.
 Lemma affinely_persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_persistently_sep_2. Qed.
-Lemma affinely_persistently_if_sep `{PositiveBI PROP} p P Q :
+Lemma affinely_persistently_if_sep `{BiPositive PROP} p P Q :
   □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
 Proof. destruct p; simpl; auto using affinely_persistently_sep. Qed.
 
@@ -1534,16 +1426,16 @@ Proof. destruct p; simpl; auto using plainly_and. Qed.
 Lemma plainly_if_or_2 p P Q :
   bi_plainly_if p P ∨ bi_plainly_if p Q ⊢ bi_plainly_if p (P ∨ Q).
 Proof. destruct p; simpl; auto using plainly_or_2. Qed.
-Lemma plainly_if_or `{PlainlyExist1BI PROP} p P Q :
+Lemma plainly_if_or `{BiPlainlyExist PROP} p P Q :
   bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P ∨ bi_plainly_if p Q.
 Proof. destruct p; simpl; auto using plainly_or. Qed.
 Lemma plainly_if_exist_2 {A} p (Ψ : A → PROP) :
   (∃ a, bi_plainly_if p (Ψ a)) ⊢ bi_plainly_if p (∃ a, Ψ a).
 Proof. destruct p; simpl; auto using plainly_exist_2. Qed.
-Lemma plainly_if_exist `{PlainlyExist1BI PROP} {A} p (Ψ : A → PROP) :
+Lemma plainly_if_exist `{BiPlainlyExist PROP} {A} p (Ψ : A → PROP) :
   bi_plainly_if p (∃ a, Ψ a) ⊣⊢ ∃ a, bi_plainly_if p (Ψ a).
 Proof. destruct p; simpl; auto using plainly_exist. Qed.
-Lemma plainly_if_sep `{PositiveBI PROP} p P Q :
+Lemma plainly_if_sep `{BiPositive PROP} p P Q :
   bi_plainly_if p (P ∗ Q) ⊣⊢ bi_plainly_if p P ∗ bi_plainly_if p Q.
 Proof. destruct p; simpl; auto using plainly_sep. Qed.
 
@@ -1568,18 +1460,18 @@ Lemma affinely_plainly_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q
 Proof. destruct p; simpl; auto using affinely_plainly_and. Qed.
 Lemma affinely_plainly_if_or_2 p P Q : ■?p P ∨ ■?p Q ⊢ ■?p (P ∨ Q).
 Proof. destruct p; simpl; auto using affinely_plainly_or_2. Qed.
-Lemma affinely_plainly_if_or `{PlainlyExist1BI PROP} p P Q :
+Lemma affinely_plainly_if_or `{BiPlainlyExist PROP} p P Q :
   ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
 Proof. destruct p; simpl; auto using affinely_plainly_or. Qed.
 Lemma affinely_plainly_if_exist_2 {A} p (Ψ : A → PROP) :
   (∃ a, ■?p Ψ a) ⊢ ■?p ∃ a, Ψ a .
 Proof. destruct p; simpl; auto using affinely_plainly_exist_2. Qed.
-Lemma affinely_plainly_if_exist `{PlainlyExist1BI PROP}  {A} p (Ψ : A → PROP) :
+Lemma affinely_plainly_if_exist `{BiPlainlyExist PROP}  {A} p (Ψ : A → PROP) :
   (■?p ∃ a, Ψ a) ⊣⊢ ∃ a, ■?p Ψ a.
 Proof. destruct p; simpl; auto using affinely_plainly_exist. Qed.
 Lemma affinely_plainly_if_sep_2 p P Q : ■?p P ∗ ■?p Q ⊢ ■?p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_plainly_sep_2. Qed.
-Lemma affinely_plainly_if_sep `{PositiveBI PROP} p P Q :
+Lemma affinely_plainly_if_sep `{BiPositive PROP} p P Q :
   ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
 Proof. destruct p; simpl; auto using affinely_plainly_sep. Qed.
 
@@ -1648,7 +1540,7 @@ Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
 Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
 
 Section persistent_bi_absorbing.
-  Context `{AffineBI PROP}.
+  Context `{BiAffine PROP}.
 
   Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
     P ∧ Q ⊣⊢ P ∗ Q.
@@ -1874,17 +1766,17 @@ Proof.
   split; [split|]; try apply _. apply plainly_and. apply plainly_pure.
 Qed.
 
-Global Instance bi_plainly_or_homomorphism `{PlainlyExist1BI PROP} :
+Global Instance bi_plainly_or_homomorphism `{BiPlainlyExist PROP} :
   MonoidHomomorphism bi_or bi_or (≡) (@bi_plainly PROP).
 Proof.
   split; [split|]; try apply _. apply plainly_or. apply plainly_pure.
 Qed.
 
-Global Instance bi_plainly_sep_weak_homomorphism `{PositiveBI PROP} :
+Global Instance bi_plainly_sep_weak_homomorphism `{BiPositive PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP).
 Proof. split; try apply _. apply plainly_sep. Qed.
 
-Global Instance bi_plainly_sep_homomorphism `{AffineBI PROP} :
+Global Instance bi_plainly_sep_homomorphism `{BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP).
 Proof. split. apply _. apply plainly_emp. Qed.
 
@@ -1908,11 +1800,11 @@ Proof.
   split; [split|]; try apply _. apply persistently_or. apply persistently_pure.
 Qed.
 
-Global Instance bi_persistently_sep_weak_homomorphism `{PositiveBI PROP} :
+Global Instance bi_persistently_sep_weak_homomorphism `{BiPositive PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
 Proof. split; try apply _. apply persistently_sep. Qed.
 
-Global Instance bi_persistently_sep_homomorphism `{AffineBI PROP} :
+Global Instance bi_persistently_sep_homomorphism `{BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
 Proof. split. apply _. apply persistently_emp. Qed.
 
@@ -2000,7 +1892,7 @@ Qed.
 
 Lemma later_True : ▷ True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
-Lemma later_emp `{!AffineBI PROP} : ▷ emp ⊣⊢ emp.
+Lemma later_emp `{!BiAffine PROP} : ▷ emp ⊣⊢ emp.
 Proof. by rewrite -True_emp later_True. Qed.
 Lemma later_forall {A} (Φ : A → PROP) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
 Proof.
@@ -2081,7 +1973,7 @@ Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
 
 Lemma laterN_True n : ▷^n True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using laterN_intro, True_intro. Qed.
-Lemma laterN_emp `{!AffineBI PROP} n : ▷^n emp ⊣⊢ emp.
+Lemma laterN_emp `{!BiAffine PROP} n : ▷^n emp ⊣⊢ emp.
 Proof. by rewrite -True_emp laterN_True. Qed.
 Lemma laterN_forall {A} n (Φ : A → PROP) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
 Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
@@ -2146,7 +2038,7 @@ Proof. apply (anti_symm _); rewrite /bi_except_0; auto. Qed.
 
 Lemma except_0_True : ◇ True ⊣⊢ True.
 Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
-Lemma except_0_emp `{!AffineBI PROP} : ◇ emp ⊣⊢ emp.
+Lemma except_0_emp `{!BiAffine PROP} : ◇ emp ⊣⊢ emp.
 Proof. by rewrite -True_emp except_0_True. Qed.
 Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
 Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
@@ -2185,7 +2077,7 @@ Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
 Lemma except_0_plainly_1 P : ◇ bi_plainly P ⊢ bi_plainly (◇ P).
 Proof. by rewrite /bi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
-Lemma except_0_plainly `{PlainlyExist1BI PROP} P :
+Lemma except_0_plainly `{BiPlainlyExist PROP} P :
   ◇ bi_plainly P ⊣⊢ bi_plainly (◇ P).
 Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
 Lemma except_0_persistently P : ◇ bi_persistently P ⊣⊢ bi_persistently (◇ P).
@@ -2194,11 +2086,11 @@ Proof.
 Qed.
 Lemma except_0_affinely_2 P : bi_affinely (◇ P) ⊢ ◇ bi_affinely P.
 Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
-Lemma except_0_affinely_plainly_2 `{PlainlyExist1BI PROP} P : ■ ◇ P ⊢ ◇ ■ P.
+Lemma except_0_affinely_plainly_2 `{BiPlainlyExist PROP} P : ■ ◇ P ⊢ ◇ ■ P.
 Proof. by rewrite -except_0_plainly except_0_affinely_2. Qed.
 Lemma except_0_affinely_persistently_2 P : □ ◇ P ⊢ ◇ □ P.
 Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed.
-Lemma except_0_affinely_plainly_if_2  `{PlainlyExist1BI PROP} p P :
+Lemma except_0_affinely_plainly_if_2  `{BiPlainlyExist PROP} p P :
   ■?p ◇ P ⊢ ◇ ■?p P.
 Proof. destruct p; simpl; auto using except_0_affinely_plainly_2. Qed.
 Lemma except_0_affinely_persistently_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
@@ -2234,7 +2126,7 @@ Proof.
   rewrite /Timeless /bi_except_0 pure_alt later_exist_false.
   apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
 Qed.
-Global Instance emp_timeless `{AffineBI PROP} : Timeless (emp : PROP)%I.
+Global Instance emp_timeless `{BiAffine PROP} : Timeless (emp : PROP)%I.
 Proof. rewrite -True_emp. apply _. Qed.
 
 Global Instance and_timeless P Q : Timeless P → Timeless Q → Timeless (P ∧ Q).
@@ -2276,7 +2168,7 @@ Proof.
   - rewrite /bi_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
-Global Instance plainly_timeless P  `{PlainlyExist1BI PROP} :
+Global Instance plainly_timeless P  `{BiPlainlyExist PROP} :
   Timeless P → Timeless (bi_plainly P).
 Proof.
   intros. rewrite /Timeless /bi_except_0 later_plainly_1.
@@ -2332,13 +2224,13 @@ Global Instance bi_except_0_sep_weak_homomorphism :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
 Proof. split; try apply _. apply except_0_sep. Qed.
 
-Global Instance bi_later_monoid_sep_homomorphism `{!AffineBI PROP} :
+Global Instance bi_later_monoid_sep_homomorphism `{!BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_later PROP).
 Proof. split; try apply _. apply later_emp. Qed.
-Global Instance bi_laterN_sep_homomorphism `{!AffineBI PROP} n :
+Global Instance bi_laterN_sep_homomorphism `{!BiAffine PROP} n :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_laterN PROP n).
 Proof. split; try apply _. apply laterN_emp. Qed.
-Global Instance bi_except_0_sep_homomorphism `{!AffineBI PROP} :
+Global Instance bi_except_0_sep_homomorphism `{!BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
 Proof. split; try apply _. apply except_0_emp. Qed.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index f0d9dbc6360a0aa65c0210e322aac439b8066ca1..cd37669c48f9c55d852a1a24f30df76ce7db79de 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -329,10 +329,6 @@ Coercion sbi_valid {PROP : sbi} : PROP → Prop := bi_valid.
 Arguments bi_valid {_} _%I : simpl never.
 Typeclasses Opaque bi_valid.
 
-Class PlainlyExist1BI (PROP : bi) :=
-  plainly_exist_1 A (Ψ : A → PROP) : bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a).
-Arguments plainly_exist_1 {_ _ _} _.
-
 Module bi.
 Section bi_laws.
 Context {PROP : bi}.
diff --git a/theories/bi/tactics.v b/theories/bi/tactics.v
index 9fdb1345ac542d324a582264ee410fbcd12b3861..b755cce52f287c442bbb7f5f0914be9acf738b87 100644
--- a/theories/bi/tactics.v
+++ b/theories/bi/tactics.v
@@ -32,7 +32,7 @@ Module bi_reflection. Section bi_reflection.
   Qed.
 
   (* Can be related to the RHS being affine *)
-  Lemma flatten_entails `{AffineBI PROP} Σ e1 e2 :
+  Lemma flatten_entails `{BiAffine PROP} Σ e1 e2 :
     flatten e2 ⊆+ flatten e1 → eval Σ e1 ⊢ eval Σ e2.
   Proof. intros. rewrite !eval_flatten. by apply big_sepL_submseteq. Qed.
   Lemma flatten_equiv Σ e1 e2 :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 91ba48abe17459a911f0b9be5bba1d541b3c64f1..9acab53c39ad388b7a5f0fb7f2725e64be3d345e 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -50,7 +50,7 @@ Proof.
   rewrite /FromAssumption /= =><-.
   by rewrite persistently_elim plainly_elim_persistently.
 Qed.
-Global Instance from_assumption_plainly_l_false `{AffineBI PROP} P Q :
+Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
   FromAssumption true P Q → FromAssumption false (bi_plainly P) Q.
 Proof.
   rewrite /FromAssumption /= =><-.
@@ -62,7 +62,7 @@ Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim
 Global Instance from_assumption_persistently_l_true P Q :
   FromAssumption true P Q → FromAssumption true (bi_persistently P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
-Global Instance from_assumption_persistently_l_false `{AffineBI PROP} P Q :
+Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
   FromAssumption true P Q → FromAssumption false (bi_persistently P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
 Global Instance from_assumption_affinely_l_true p P Q :
@@ -224,7 +224,7 @@ Proof.
   rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
 Qed.
 
-Global Instance into_wand_impl_false_false `{!AffineBI PROP} P Q P' :
+Global Instance into_wand_impl_false_false `{!BiAffine PROP} P Q P' :
   FromAssumption false P P' → IntoWand false false (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => ->. apply wand_intro_r.
@@ -274,7 +274,7 @@ Proof. by rewrite /IntoWand affinely_plainly_elim. Qed.
 Global Instance into_wand_plainly_true q R P Q :
   IntoWand true q R P Q → IntoWand true q (bi_plainly R) P Q.
 Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
-Global Instance into_wand_plainly_false `{!AffineBI PROP} q R P Q :
+Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_plainly R) P Q.
 Proof. by rewrite /IntoWand plainly_elim. Qed.
 
@@ -284,7 +284,7 @@ Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
 Global Instance into_wand_persistently_true q R P Q :
   IntoWand true q R P Q → IntoWand true q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
-Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
+Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
 
@@ -388,7 +388,7 @@ Proof.
   by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
 Qed.
 
-Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
+Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P ∗ Q) P Q.
 Proof.
   by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
 Qed.
@@ -460,10 +460,10 @@ Global Instance into_sep_affinely P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_affinely P) Q1 Q2 | 20.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
 
-Global Instance into_sep_plainly `{PositiveBI PROP} P Q1 Q2 :
+Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
-Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
+Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 →
   IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
@@ -512,7 +512,7 @@ Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
 Global Instance into_or_absorbingly P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
 Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
-Global Instance into_or_plainly `{PlainlyExist1BI PROP} P Q1 Q2 :
+Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
 Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
 Global Instance into_or_persistently P Q1 Q2 :
@@ -564,7 +564,7 @@ Qed.
 Global Instance into_exist_absorbingly {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
-Global Instance into_exist_plainly `{PlainlyExist1BI PROP} {A} P (Φ : A → PROP) :
+Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
@@ -609,7 +609,7 @@ Proof.
   - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
 Qed.
 
-Global Instance from_forall_affinely `{AffineBI PROP} {A} P (Φ : A → PROP) :
+Global Instance from_forall_affinely `{BiAffine PROP} {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (bi_affinely P)%I (λ a, bi_affinely (Φ a))%I.
 Proof.
   rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
@@ -1051,7 +1051,7 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_affinely_2. Qed.
 Global Instance into_except_0_absorbingly P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_absorbingly P) (bi_absorbingly Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
-Global Instance into_except_0_plainly `{PlainlyExist1BI PROP} P Q :
+Global Instance into_except_0_plainly `{BiPlainlyExist PROP} P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_plainly P) (bi_plainly Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
 Global Instance into_except_0_persistently P Q :
@@ -1234,7 +1234,7 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
   FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
 Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 
-Global Instance from_later_affinely n P Q `{AffineBI PROP} :
+Global Instance from_later_affinely n P Q `{BiAffine PROP} :
   FromLaterN n P Q → FromLaterN n (bi_affinely P) (bi_affinely Q).
 Proof. rewrite /FromLaterN=><-. by rewrite affinely_elim affine_affinely. Qed.
 Global Instance from_later_plainly n P Q :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 08708214ec629141f15c8132993a7ff7a0c48b94..0648e90709ddd3a1602496861f9c6e51637c4232 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -458,7 +458,7 @@ Global Instance affine_env_snoc Γ i P :
 Proof. by constructor. Qed.
 
 (* If the BI is affine, no need to walk on the whole environment. *)
-Global Instance affine_env_bi `(AffineBI PROP) Γ : AffineEnv Γ | 0.
+Global Instance affine_env_bi `(BiAffine PROP) Γ : AffineEnv Γ | 0.
 Proof. induction Γ; apply _. Qed.
 
 Instance affine_env_spatial Δ :
@@ -800,7 +800,7 @@ Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
   envs_entails Δ (bi_absorbingly R) →
   IntoPersistent false R R' →
-  (if q then TCTrue else AffineBI PROP) →
+  (if q then TCTrue else BiAffine PROP) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
   envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.