diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index b193b947473f7f5821215bc262622ad99dd60608..829788b85e7fff596535ba78967837bd7d60cd17 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -31,10 +31,6 @@ Proof.
   apply limit_preserving_and; by apply limit_preserving_entails.
 Qed.
 
-(* Affine *)
-Global Instance uPred_affine : BiAffine (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).
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index d65acf875c1c96f89f62c63113a711046fdf11b2..f78d85f128c83b8d0f1b49dc88a6b23f1141b250 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -474,8 +474,6 @@ Proof.
     unseal; split=> n x ?? //.
   - (* (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a) *)
     by unseal.
-  - (* bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a) *)
-    by unseal.
   - (* bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q *)
     unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
     split; eapply HPQ; eauto using @ucmra_unit_least.
@@ -610,6 +608,14 @@ Proof.
 Qed.
 Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_proper _.
 
+(** BI instances *)
+
+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)) :
   (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 942c2f1dea2109b4b494ab75f64a5a251607f2b4..d3fe0fab587ddf13f8eddaba7a6d7d978fbca0f9 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -45,6 +45,11 @@ 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.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 6b64871b89c58c229cf97c13db8d1ee2d1b15b87..a3f10be7f2635320ed9ca5c1fa2831badd4dd90e 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1075,15 +1075,18 @@ Proof.
   apply (anti_symm _); auto using plainly_forall_2.
   apply forall_intro=> x. by rewrite (forall_elim x).
 Qed.
-Lemma plainly_exist {A} (Ψ : A → PROP) :
+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 `{BiPlainlyExist PROP} {A} (Ψ : A → PROP) :
   bi_plainly (∃ a, Ψ a) ⊣⊢ ∃ a, bi_plainly (Ψ a).
-Proof.
-  apply (anti_symm _); auto using plainly_exist_1.
-  apply exist_elim=> x. by rewrite (exist_intro x).
-Qed.
+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 P Q : bi_plainly (P ∨ Q) ⊣⊢ bi_plainly P ∨ bi_plainly Q.
+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 `{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.
 Proof.
@@ -1254,9 +1257,14 @@ Proof.
 Qed.
 Lemma affinely_plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
 Proof. by rewrite plainly_and affinely_and. Qed.
-Lemma affinely_plainly_or P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+Lemma affinely_plainly_or_2 P Q : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q).
+Proof. by rewrite -plainly_or_2 affinely_or. Qed.
+Lemma affinely_plainly_or `{BiPlainlyExist PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
 Proof. by rewrite plainly_or affinely_or. Qed.
-Lemma affinely_plainly_exist {A} (Φ : A → PROP) : ■ (∃ x, Φ x) ⊣⊢ ∃ x, ■ Φ x.
+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 `{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.
@@ -1415,9 +1423,17 @@ Lemma plainly_if_pure p φ : bi_plainly_if p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. destruct p; simpl; auto using plainly_pure. Qed.
 Lemma plainly_if_and 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_and. Qed.
-Lemma plainly_if_or p P Q : bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P ∨ bi_plainly_if p Q.
+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 `{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 {A} p (Ψ : A → PROP) : (bi_plainly_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_plainly_if p (Ψ a).
+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 `{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 `{BiPositive PROP} p P Q :
   bi_plainly_if p (P ∗ Q) ⊣⊢ bi_plainly_if p P ∗ bi_plainly_if p Q.
@@ -1442,9 +1458,15 @@ Lemma affinely_plainly_if_emp p : ■?p emp ⊣⊢ emp.
 Proof. destruct p; simpl; auto using affinely_plainly_emp. Qed.
 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 p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
+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 `{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 {A} p (Ψ : A → PROP) :
+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 `{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).
@@ -1683,7 +1705,7 @@ Proof. apply plainly_emp_intro. Qed.
 Global Instance and_plain P Q : Plain P → Plain Q → Plain (P ∧ Q).
 Proof. intros. by rewrite /Plain plainly_and -!plain. Qed.
 Global Instance or_plain P Q : Plain P → Plain Q → Plain (P ∨ Q).
-Proof. intros. by rewrite /Plain plainly_or -!plain. Qed.
+Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed.
 Global Instance forall_plain {A} (Ψ : A → PROP) :
   (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
 Proof.
@@ -1692,7 +1714,7 @@ Qed.
 Global Instance exist_plain {A} (Ψ : A → PROP) :
   (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
 Proof.
-  intros. rewrite /Plain plainly_exist. apply exist_mono=> x. by rewrite -plain.
+  intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
 Qed.
 
 Global Instance internal_eq_plain {A : ofeT} (a b : A) :
@@ -1744,7 +1766,7 @@ Proof.
   split; [split|]; try apply _. apply plainly_and. apply plainly_pure.
 Qed.
 
-Global Instance bi_plainly_or_homomorphism :
+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.
@@ -2053,7 +2075,10 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
-Lemma except_0_plainly P : ◇ bi_plainly P ⊣⊢ bi_plainly (◇ P).
+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 `{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).
 Proof.
@@ -2061,11 +2086,12 @@ 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 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 p P : ■?p ◇ P ⊢ ◇ ■?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.
 Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed.
@@ -2142,7 +2168,8 @@ Proof.
   - rewrite /bi_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
-Global Instance plainly_timeless P : Timeless P → Timeless (bi_plainly P).
+Global Instance plainly_timeless P  `{BiPlainlyExist PROP} :
+  Timeless P → Timeless (bi_plainly P).
 Proof.
   intros. rewrite /Timeless /bi_except_0 later_plainly_1.
   by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 70ccc5f42572c76e6a8254e8187e0474d8054f37..cd37669c48f9c55d852a1a24f30df76ce7db79de 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -107,8 +107,6 @@ Section bi_mixin.
 
     bi_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
       (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a);
-    bi_mixin_plainly_exist_1 {A} (Ψ : A → PROP) :
-      bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a);
 
     bi_mixin_prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢
       bi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
@@ -449,9 +447,6 @@ Proof. eapply bi_mixin_plainly_idemp_2, bi_bi_mixin. Qed.
 Lemma plainly_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a).
 Proof. eapply bi_mixin_plainly_forall_2, bi_bi_mixin. Qed.
-Lemma plainly_exist_1 {A} (Ψ : A → PROP) :
-  bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a).
-Proof. eapply bi_mixin_plainly_exist_1, bi_bi_mixin. Qed.
 Lemma prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
 Proof. eapply (bi_mixin_prop_ext _ bi_entails), bi_bi_mixin. Qed.
 Lemma persistently_impl_plainly P Q :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 5c350e0199849e94a33c2864880f81f14d86943b..9acab53c39ad388b7a5f0fb7f2725e64be3d345e 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -495,7 +495,7 @@ Global Instance from_or_absorbingly P Q1 Q2 :
 Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
 Global Instance from_or_plainly P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
-Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
+Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
 Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -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 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 :
@@ -534,7 +534,7 @@ Global Instance from_exist_absorbingly {A} P (Φ : A → PROP) :
 Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
 Global Instance from_exist_plainly {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
-Proof. rewrite /FromExist=> <-. by rewrite plainly_exist. Qed.
+Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
@@ -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 {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) :
@@ -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 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 :