diff --git a/_CoqProject b/_CoqProject
index 623fce6cc6d71ffdc1b58419dff44ec34dd083dc..4ddfcad2828c5bac0ccd3d904367d4bc1cd0b650 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,6 +28,7 @@ theories/algebra/proofmode_classes.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
 theories/bi/derived_laws.v
+theories/bi/plainly.v
 theories/bi/big_op.v
 theories/bi/updates.v
 theories/bi/bi.v
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 0972828f21cd098bb28f9c521b88b4f5955de0b5..c126c39334338cf2e5834754ecaeb6bbb9851d17 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -30,11 +30,8 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-Lemma affinely_plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
-Proof.
-  rewrite affine_affinely.
-  apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _.
-Qed.
+Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
 Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
   rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index ca5a5ce2b6e1393220ab640c8c0dd93b04dd52ff..5861c57d92af8c66e13c17ecb848f083dbc49375 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -30,6 +30,16 @@ Proof.
     iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
     iIntros "!> !>". by iApply "HP".
   - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
+Qed.
+Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
+  {| bi_fupd_mixin := uPred_fupd_mixin |}.
+
+Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
+Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
+
+Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
+Proof.
+  split.
   - iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
     rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
     iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
@@ -39,9 +49,4 @@ Proof.
   - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
     iAssert (â–· â—‡ P)%I with "[-]" as "#$"; last by iFrame.
     iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
-Qed.
-Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
-  {| bi_fupd_mixin := uPred_fupd_mixin |}.
-
-Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
-Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
+Qed.
\ No newline at end of file
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 6feffe22fcd7f48eae06b3d8bc490ad73390064f..4284299a89ec8ed6fa7d35fbd43edf706e338f1e 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 derived_connectives updates.
+From iris.bi Require Export derived_connectives updates plainly.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
@@ -278,13 +278,13 @@ Definition uPred_wand_eq :
 (* Equivalently, this could be `∀ y, P n y`.  That's closer to the intuition
    of "embedding the step-indexed logic in Iris", but the two are equivalent
    because Iris is afine.  The following is easier to work with. *)
-Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
+Program Definition uPred_plainly_def {M} : Plainly (uPred M) := λ P,
   {| uPred_holds n x := P n ε |}.
 Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
-Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
-Definition uPred_plainly {M} := unseal uPred_plainly_aux M.
-Definition uPred_plainly_eq :
-  @uPred_plainly = @uPred_plainly_def := seal_eq uPred_plainly_aux.
+Definition uPred_plainly_aux {M} : seal (@uPred_plainly_def M). by eexists. Qed.
+Definition uPred_plainly {M} := unseal (@uPred_plainly_aux M).
+Definition uPred_plainly_eq M :
+  @plainly _ uPred_plainly = @uPred_plainly_def M := seal_eq uPred_plainly_aux.
 
 Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
@@ -347,11 +347,11 @@ Definition unseal_eqs :=
   uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
   uPred_cmra_valid_eq, @uPred_bupd_eq).
 Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
-  unfold bi_emp; simpl;
+  unfold bi_emp; simpl; unfold sbi_emp; simpl;
   unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
-  bi_sep, bi_wand, bi_plainly, bi_persistently, sbi_internal_eq, sbi_later; simpl;
+  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
   unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
-  sbi_internal_eq, sbi_sep, sbi_wand, sbi_plainly, sbi_persistently; simpl;
+  sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
   rewrite !unseal_eqs /=.
 End uPred_unseal.
 Import uPred_unseal.
@@ -361,7 +361,7 @@ Local Arguments uPred_holds {_} !_ _ _ /.
 Lemma uPred_bi_mixin (M : ucmraT) :
   BiMixin
     uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
-    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand uPred_plainly
+    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
     uPred_persistently.
 Proof.
   split.
@@ -398,9 +398,6 @@ Proof.
     intros n P P' HP Q Q' HQ; split=> n' x ??.
     unseal; split; intros HPQ x' n'' ???;
       apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
-  - (* NonExpansive uPred_plainly *)
-    intros n P1 P2 HP.
-    unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
   - (* NonExpansive uPred_persistently *)
     intros n P1 P2 HP.
     unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
@@ -460,32 +457,12 @@ Proof.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
     eapply HPQR; eauto using cmra_validN_op_l.
-  - (* (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q *)
-    intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
-  - (* bi_plainly P ⊢ bi_persistently P *)
-    unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
-  - (* bi_plainly P ⊢ bi_plainly (bi_plainly P) *)
-    unseal; split=> n x ?? //.
-  - (* (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a) *)
-    by unseal.
-  - (* (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q) *)
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  - (* (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q) *)
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  - (* P ⊢ bi_plainly emp (ADMISSIBLE) *)
-    by unseal.
-  - (* bi_plainly P ∗ Q ⊢ bi_plainly P *)
-    intros P Q. move: (uPred_persistently P)=> P'.
-    unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
-      eauto using uPred_mono, cmra_includedN_l.
   - (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
   - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
+  - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
+    by unseal.
   - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
   - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
@@ -499,10 +476,10 @@ Proof.
     exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
 
-Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin uPred_ofe_mixin
-  uPred_entails uPred_pure uPred_and uPred_or uPred_impl
-  (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
-  uPred_plainly uPred_persistently (@uPred_internal_eq M) uPred_later.
+Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
+  uPred_entails uPred_pure uPred_or uPred_impl
+  (@uPred_forall M) (@uPred_exist M) uPred_sep
+  uPred_persistently (@uPred_internal_eq M) uPred_later.
 Proof.
   split.
   - (* Contractive sbi_later *)
@@ -523,10 +500,6 @@ Proof.
     by unseal.
   - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝ *)
     intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
-  - (* bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
-    unseal; split=> n x ? /= HPQ. split=> n' x' ??.
-    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
-    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
   - (* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
     by unseal.
   - (* ▷ (x ≡ y) ⊢ Next x ≡ Next y *)
@@ -550,10 +523,6 @@ Proof.
   - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
     intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
     exists x1, x2; eauto using dist_S.
-  - (* ▷ bi_plainly P ⊢ bi_plainly (▷ P) *)
-    by unseal.
-  - (* bi_plainly (▷ P) ⊢ ▷ bi_plainly P *)
-    by unseal.
   - (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
     by unseal.
   - (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
@@ -575,6 +544,46 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
 (* Latest notation *)
 Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
 
+Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Proof.
+  split.
+  - (* NonExpansive uPred_plainly *)
+    intros n P1 P2 HP.
+    unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
+  - (* (P ⊢ Q) → ■ P ⊢ ■ Q *)
+    intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
+  - (* ■ P ⊢ bi_persistently P *)
+    unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
+  - (* ■ P ⊢ ■ ■ P *)
+    unseal; split=> n x ?? //.
+  - (* (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a) *)
+    by unseal.
+  - (* (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q) *)
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  - (* (■ P → ■ Q) ⊢ ■ (■ P → Q) *)
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  - (* P ⊢ ■ emp (ADMISSIBLE) *)
+    by unseal.
+  - (* ■ P ∗ Q ⊢ ■ P *)
+    intros P Q. move: (uPred_persistently P)=> P'.
+    unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
+      eauto using uPred_mono, cmra_includedN_l.
+  - (* ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
+    unseal; split=> n x ? /= HPQ. split=> n' x' ??.
+    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
+    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
+  - (* ▷ ■ P ⊢ ■ ▷ P *)
+    by unseal.
+  - (* ■ ▷ P ⊢ ▷ ■ P *)
+    by unseal.
+Qed.
+Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+  {| bi_plainly_mixin := uPred_plainly_mixin M |}.
+
 Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
 Proof.
   split.
@@ -593,12 +602,16 @@ Proof.
     { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
     exists (x' â‹… x2); split; first by rewrite -assoc.
     exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
-  - unseal; split => n x Hnx /= Hng.
-    destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
-    eapply uPred_mono; eauto using ucmra_unit_leastN.
 Qed.
 Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
 
+Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
+Proof.
+  rewrite /BiBUpdPlainly. unseal; split => n x Hnx /= Hng.
+  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
+  eapply uPred_mono; eauto using ucmra_unit_leastN.
+Qed.
+
 Module uPred.
 Include uPred_unseal.
 Section uPred.
@@ -630,7 +643,7 @@ Global Instance cmra_valid_proper {A : cmraT} :
 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).
+Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
 Proof. unfold BiPlainlyExist. by unseal. Qed.
 
 (** Limits *)
@@ -684,7 +697,7 @@ Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : u
 Proof.
   intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
 Qed.
-Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ bi_plainly (✓ a : uPred M).
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ (✓ a : uPred M).
 Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ (✓ a : uPred M).
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 4cef163c554776a75c9fd03b053716d240e90d0d..d00050dc4309fbd0a9f0b4f3fbfd6b50001e244c 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_laws big_op updates embedding.
+From iris.bi Require Export derived_laws big_op updates plainly embedding.
 Set Default Proof Using "Type".
 
 Module Import bi.
@@ -16,4 +16,4 @@ Hint Resolve sep_elim_l sep_elim_r sep_mono : BI.
 Hint Immediate True_intro False_elim : BI.
 (*
 Hint Immediate iff_refl internal_eq_refl' : BI.
-*)
\ No newline at end of file
+*)
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 3472d004e2a2af15305b93e0d33de27ba92dbedb..d7648e9287febcd3da580f7b3a9af2a9703d6aa8 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export big_op.
 From iris.bi Require Export derived_laws.
+From iris.bi Require Import plainly.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
 
@@ -125,10 +126,6 @@ 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 `{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 `{BiAffine PROP} Φ l :
     bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢
     [∗ list] k↦x ∈ l, bi_persistently (Φ k x).
@@ -163,16 +160,6 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
-  Global Instance big_sepL_nil_plain Φ :
-    Plain ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. simpl; apply _. Qed.
-  Global Instance big_sepL_plain Φ l :
-    (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-  Global Instance big_sepL_plain_id Ps :
-    TCForall Plain Ps → Plain ([∗] Ps).
-  Proof. induction 1; simpl; apply _. Qed.
-
   Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
@@ -278,10 +265,6 @@ Section and_list.
     ⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x).
   Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_andL_plainly Φ 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_andL_persistently Φ l :
     bi_persistently ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢
     [∧ list] k↦x ∈ l, bi_persistently (Φ k x).
@@ -299,19 +282,13 @@ Section and_list.
     - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
   Qed.
 
-  Global Instance big_andL_nil_plain Φ :
-    Plain ([∧ list] k↦x ∈ [], Φ k x).
-  Proof. simpl; apply _. Qed.
-  Global Instance big_andL_plain Φ l :
-    (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x).
-  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-
   Global Instance big_andL_nil_persistent Φ :
     Persistent ([∧ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_andL_persistent Φ l :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
 End and_list.
 
 (** ** Big ops over finite maps *)
@@ -420,10 +397,6 @@ 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 `{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 `{BiAffine PROP} Φ m :
     (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
       ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
@@ -464,12 +437,6 @@ Section gmap.
       by rewrite pure_True // True_impl.
   Qed.
 
-  Global Instance big_sepM_empty_plain Φ : Plain ([∗ map] k↦x ∈ ∅, Φ k x).
-  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
-  Global Instance big_sepM_plain Φ m :
-    (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x  ∈ m, Φ k x).
-  Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
-
   Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
@@ -596,10 +563,6 @@ 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 `{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 `{BiAffine PROP} Φ X :
     bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y).
   Proof. apply (big_opS_commute _). Qed.
@@ -633,12 +596,6 @@ Section gset.
       by rewrite pure_True ?True_impl; last set_solver.
   Qed.
 
-  Global Instance big_sepS_empty_plain Φ : Plain ([∗ set] x ∈ ∅, Φ x).
-  Proof. rewrite /big_opS elements_empty. apply _. Qed.
-  Global Instance big_sepS_plain Φ X :
-    (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
-  Proof. rewrite /big_opS. apply _. Qed.
-
   Global Instance big_sepS_empty_persistent Φ :
     Persistent ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
@@ -714,21 +671,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 `{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 `{BiAffine PROP} Φ X :
     bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
       [∗ mset] y ∈ X, bi_persistently (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Global Instance big_sepMS_empty_plain Φ : Plain ([∗ mset] x ∈ ∅, Φ x).
-  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
-  Global Instance big_sepMS_plain Φ X :
-    (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
-  Proof. rewrite /big_opMS. apply _. Qed.
-
   Global Instance big_sepMS_empty_persistent Φ :
     Persistent ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
@@ -773,6 +720,34 @@ Section list.
   Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
     TCForall Timeless Ps → Timeless ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepL_plainly `{!BiAffine PROP} Φ l :
+      ■ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, ■ (Φ k x).
+    Proof. apply (big_opL_commute _). Qed.
+
+    Global Instance big_sepL_nil_plain `{!BiAffine PROP} Φ :
+      Plain ([∗ list] k↦x ∈ [], Φ k x).
+    Proof. simpl; apply _. Qed.
+
+    Global Instance big_sepL_plain `{!BiAffine PROP} Φ l :
+      (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
+    Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
+    Lemma big_andL_plainly Φ l :
+      ■ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, ■ (Φ k x).
+    Proof. apply (big_opL_commute _). Qed.
+
+    Global Instance big_andL_nil_plain Φ :
+      Plain ([∧ list] k↦x ∈ [], Φ k x).
+    Proof. simpl; apply _. Qed.
+
+    Global Instance big_andL_plain Φ l :
+      (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x).
+    Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  End plainly.
 End list.
 
 (** ** Big ops over finite maps *)
@@ -795,6 +770,21 @@ Section gmap.
   Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepM_plainly `{BiAffine PROP} Φ m :
+      ■ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■ (Φ k x).
+    Proof. apply (big_opM_commute _). Qed.
+
+    Global Instance big_sepM_empty_plain `{BiAffine PROP} Φ :
+      Plain ([∗ map] k↦x ∈ ∅, Φ k x).
+    Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
+    Global Instance big_sepM_plain `{BiAffine PROP} Φ m :
+      (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x  ∈ m, Φ k x).
+    Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
+  End plainly.
 End gmap.
 
 (** ** Big ops over finite sets *)
@@ -817,6 +807,20 @@ Section gset.
   Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepS_plainly `{BiAffine PROP} Φ X :
+      ■ ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■ (Φ y).
+    Proof. apply (big_opS_commute _). Qed.
+
+    Global Instance big_sepS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ set] x ∈ ∅, Φ x).
+    Proof. rewrite /big_opS elements_empty. apply _. Qed.
+    Global Instance big_sepS_plain `{BiAffine PROP} Φ X :
+      (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
+    Proof. rewrite /big_opS. apply _. Qed.
+  End plainly.
 End gset.
 
 (** ** Big ops over finite multisets *)
@@ -839,6 +843,20 @@ Section gmultiset.
   Global Instance big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepMS_plainly `{BiAffine PROP} Φ X :
+      ■ ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, ■ (Φ y).
+    Proof. apply (big_opMS_commute _). Qed.
+
+    Global Instance big_sepMS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ mset] x ∈ ∅, Φ x).
+    Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
+    Global Instance big_sepMS_plain `{BiAffine PROP} Φ X :
+      (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
+    Proof. rewrite /big_opMS. apply _. Qed.
+  End plainly.
 End gmultiset.
 End sbi_big_op.
 End bi.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 1ad05c3aaab07f29ac29662081209db05559bb61..fbd3213ec5da0785ce67333a1f60fa5836f0bbc4 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -13,12 +13,6 @@ 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 {_}.
@@ -31,8 +25,6 @@ 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.
@@ -45,11 +37,6 @@ 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.
@@ -59,12 +46,6 @@ 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 /.
@@ -79,9 +60,6 @@ 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
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 8e99ebd7dbf99dc4f9aed534e10445fd9e3c1762..474bf1bb7c390a79eb113b99730bcf59f5746860 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -68,8 +68,6 @@ Proof.
   intros Φ1 Φ2 HΦ. apply equiv_dist=> n.
   apply exist_ne=> x. apply equiv_dist, HΦ.
 Qed.
-Global Instance plainly_proper :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_plainly PROP) := ne_proper _.
 Global Instance persistently_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently PROP) := ne_proper _.
 
@@ -755,9 +753,6 @@ Proof.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 
-Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
-Proof. by rewrite -plainly_elim_persistently -plainly_emp_intro. Qed.
-
 Lemma persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
 
@@ -941,182 +936,6 @@ Section persistently_affinely_bi.
   Qed.
 End persistently_affinely_bi.
 
-(* Properties of the plainness modality *)
-Hint Resolve plainly_mono.
-Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@bi_plainly PROP).
-Proof. intros P Q; apply plainly_mono. Qed.
-Global Instance plainly_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@bi_plainly PROP).
-Proof. intros P Q; apply plainly_mono. Qed.
-
-Lemma persistently_plainly P : bi_persistently (bi_plainly P) ⊣⊢ bi_plainly P.
-Proof.
-  apply (anti_symm _).
-  - by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorbing.
-  - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
-Qed.
-Lemma plainly_persistently P : bi_plainly (bi_persistently P) ⊣⊢ bi_plainly P.
-Proof.
-  apply (anti_symm _).
-  - rewrite -{1}(left_id True%I bi_and (bi_plainly _)) (plainly_emp_intro True%I).
-    rewrite -{2}(persistently_and_emp_elim P).
-    rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
-  - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
-Qed.
-
-Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) ⊣⊢ bi_plainly P.
-Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed.
-
-Lemma plainly_and_sep_elim P Q : bi_plainly P ∧ Q -∗ (emp ∧ P) ∗ Q.
-Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
-Lemma plainly_and_sep_assoc P Q R :
-  bi_plainly P ∧ (Q ∗ R) ⊣⊢ (bi_plainly P ∧ Q) ∗ R.
-Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed.
-Lemma plainly_and_emp_elim P : emp ∧ bi_plainly P ⊢ P.
-Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
-Lemma plainly_elim_absorbingly P : bi_plainly P ⊢ bi_absorbingly P.
-Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed.
-Lemma plainly_elim P `{!Absorbing P} : bi_plainly P ⊢ P.
-Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
-
-Lemma plainly_idemp_1 P : bi_plainly (bi_plainly P) ⊢ bi_plainly P.
-Proof. by rewrite plainly_elim_absorbingly absorbingly_plainly. Qed.
-Lemma plainly_idemp P : bi_plainly (bi_plainly P) ⊣⊢ bi_plainly P.
-Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
-
-Lemma plainly_intro' P Q : (bi_plainly P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q.
-Proof. intros <-. apply plainly_idemp_2. Qed.
-
-Lemma plainly_pure φ : bi_plainly ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof.
-  apply (anti_symm _); auto.
-  - by rewrite plainly_elim_persistently persistently_pure.
-  - apply pure_elim'=> Hφ.
-    trans (∀ x : False, bi_plainly True : PROP)%I; [by apply forall_intro|].
-    rewrite plainly_forall_2. by rewrite -(pure_intro _ φ).
-Qed.
-Lemma plainly_forall {A} (Ψ : A → PROP) :
-  bi_plainly (∀ a, Ψ a) ⊣⊢ ∀ a, bi_plainly (Ψ a).
-Proof.
-  apply (anti_symm _); auto using plainly_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-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 `{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 `{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.
-  apply impl_intro_l; rewrite -plainly_and.
-  apply plainly_mono, impl_elim with P; auto.
-Qed.
-
-Lemma plainly_sep_dup P : bi_plainly P ⊣⊢ bi_plainly P ∗ bi_plainly P.
-Proof.
-  apply (anti_symm _).
-  - rewrite -{1}(idemp bi_and (bi_plainly _)).
-    by rewrite -{2}(left_id emp%I _ (bi_plainly _)) plainly_and_sep_assoc and_elim_l.
-  - by rewrite plainly_absorbing.
-Qed.
-
-Lemma plainly_and_sep_l_1 P Q : bi_plainly P ∧ Q ⊢ bi_plainly P ∗ Q.
-Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qed.
-Lemma plainly_and_sep_r_1 P Q : P ∧ bi_plainly Q ⊢ P ∗ bi_plainly Q.
-Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
-
-Lemma plainly_True_emp : bi_plainly True ⊣⊢ bi_plainly emp.
-Proof. apply (anti_symm _); auto using plainly_emp_intro. Qed.
-Lemma plainly_and_sep P Q : bi_plainly (P ∧ Q) ⊢ bi_plainly (P ∗ Q).
-Proof.
-  rewrite plainly_and.
-  rewrite -{1}plainly_idemp -plainly_and -{1}(left_id emp%I _ Q%I).
-  by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
-Qed.
-
-Lemma plainly_affinely P : bi_plainly (bi_affinely P) ⊣⊢ bi_plainly P.
-Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
-
-Lemma and_sep_plainly P Q :
-  bi_plainly P ∧ bi_plainly Q ⊣⊢ bi_plainly P ∗ bi_plainly Q.
-Proof.
-  apply (anti_symm _); auto using plainly_and_sep_l_1.
-  apply and_intro.
-  - by rewrite plainly_absorbing.
-  - by rewrite comm plainly_absorbing.
-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 `{BiPositive PROP} P Q :
-  bi_plainly (P ∗ Q) ⊣⊢ bi_plainly P ∗ bi_plainly Q.
-Proof.
-  apply (anti_symm _); auto using plainly_sep_2.
-  rewrite -plainly_affinely affinely_sep -and_sep_plainly. apply and_intro.
-  - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
-  - by rewrite (affinely_elim_emp P) left_id affinely_elim.
-Qed.
-
-Lemma plainly_wand P Q : bi_plainly (P -∗ Q) ⊢ bi_plainly P -∗ bi_plainly Q.
-Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed.
-
-Lemma plainly_entails_l P Q : (P ⊢ bi_plainly Q) → P ⊢ bi_plainly Q ∗ P.
-Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed.
-Lemma plainly_entails_r P Q : (P ⊢ bi_plainly Q) → P ⊢ P ∗ bi_plainly Q.
-Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.
-
-Lemma plainly_impl_wand_2 P Q : bi_plainly (P -∗ Q) ⊢ bi_plainly (P → Q).
-Proof.
-  apply plainly_intro', impl_intro_r.
-  rewrite -{2}(left_id emp%I _ P%I) plainly_and_sep_assoc.
-  by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
-Qed.
-
-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.
-
-Lemma valid_plainly P : bi_valid (bi_plainly P) ↔ bi_valid P.
-Proof.
-  rewrite /bi_valid. split; intros HP.
-  - by rewrite -(idemp bi_and emp%I) {2}HP plainly_and_emp_elim.
-  - by rewrite (plainly_emp_intro emp%I) HP.
-Qed.
-
-Section plainly_affinely_bi.
-  Context `{BiAffine PROP}.
-
-  Lemma plainly_emp : bi_plainly emp ⊣⊢ emp.
-  Proof. by rewrite -!True_emp plainly_pure. Qed.
-
-  Lemma plainly_and_sep_l P Q : bi_plainly P ∧ Q ⊣⊢ bi_plainly P ∗ Q.
-  Proof.
-    apply (anti_symm (⊢));
-      eauto using plainly_and_sep_l_1, sep_and with typeclass_instances.
-  Qed.
-  Lemma plainly_and_sep_r P Q : P ∧ bi_plainly Q ⊣⊢ P ∗ bi_plainly Q.
-  Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed.
-
-  Lemma plainly_impl_wand P Q : bi_plainly (P → Q) ⊣⊢ bi_plainly (P -∗ Q).
-  Proof.
-    apply (anti_symm (⊢)); auto using plainly_impl_wand_2.
-    apply plainly_intro', wand_intro_l.
-    by rewrite -plainly_and_sep_r plainly_elim impl_elim_r.
-  Qed.
-
-  Lemma impl_wand_plainly P Q : (bi_plainly P → Q) ⊣⊢ (bi_plainly P -∗ Q).
-  Proof.
-    apply (anti_symm (⊢)). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2.
-  Qed.
-End plainly_affinely_bi.
-
 (* The combined affinely persistently modality *)
 Lemma affinely_persistently_elim P : □ P ⊢ P.
 Proof. apply persistently_and_emp_elim. Qed.
@@ -1170,52 +989,6 @@ Proof.
   - apply impl_intro_l. by rewrite persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 
-(* The combined affinely plainly modality *)
-Lemma affinely_plainly_elim P : ■ P ⊢ P.
-Proof. apply plainly_and_emp_elim. Qed.
-Lemma affinely_plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
-Proof. intros <-. by rewrite plainly_affinely plainly_idemp. Qed.
-
-Lemma affinely_plainly_emp : ■ emp ⊣⊢ emp.
-Proof.
-  by rewrite -plainly_True_emp plainly_pure affinely_True_emp affinely_emp.
-Qed.
-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 `{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 `{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 `{BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
-Proof. by rewrite -affinely_sep -plainly_sep. Qed.
-
-Lemma affinely_plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
-Proof. by rewrite plainly_affinely plainly_idemp. Qed.
-
-Lemma plainly_and_affinely_sep_l P Q : bi_plainly P ∧ Q ⊣⊢ ■ P ∗ Q.
-Proof. by rewrite -(persistently_plainly P) persistently_and_affinely_sep_l. Qed.
-Lemma plainly_and_affinely_sep_r P Q : P ∧ bi_plainly Q ⊣⊢ P ∗ ■ Q.
-Proof. by rewrite !(comm _ P) plainly_and_affinely_sep_l. Qed.
-Lemma and_sep_affinely_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
-Proof.
-  by rewrite -plainly_and_affinely_sep_l -affinely_and affinely_and_r.
-Qed.
-
-Lemma affinely_plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ P.
-Proof.
-  by rewrite -plainly_and_affinely_sep_l affinely_and_r affinely_and idemp.
-Qed.
-
-Lemma impl_wand_affinely_plainly P Q : (bi_plainly P → Q) ⊣⊢ (■ P -∗ Q).
-Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed.
-
 (* Conditional affinely modality *)
 Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
@@ -1334,81 +1107,6 @@ Proof. destruct p; simpl; auto using affinely_persistently_sep. Qed.
 Lemma affinely_persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
 Proof. destruct p; simpl; auto using affinely_persistently_idemp. Qed.
 
-(* Conditional plainly *)
-Global Instance plainly_if_ne p : NonExpansive (@bi_plainly_if PROP p).
-Proof. solve_proper. Qed.
-Global Instance plainly_if_proper p :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_plainly_if PROP p).
-Proof. solve_proper. Qed.
-Global Instance plainly_if_mono' p :
-  Proper ((⊢) ==> (⊢)) (@bi_plainly_if PROP p).
-Proof. solve_proper. Qed.
-Global Instance plainly_if_flip_mono' p :
-  Proper (flip (⊢) ==> flip (⊢)) (@bi_plainly_if PROP p).
-Proof. solve_proper. Qed.
-
-Lemma plainly_if_mono p P Q : (P ⊢ Q) → bi_plainly_if p P ⊢ bi_plainly_if p Q.
-Proof. by intros ->. Qed.
-
-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_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_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.
-Proof. destruct p; simpl; auto using plainly_sep. Qed.
-
-Lemma plainly_if_idemp p P :
-  bi_plainly_if p (bi_plainly_if p P) ⊣⊢ bi_plainly_if p P.
-Proof. destruct p; simpl; auto using plainly_idemp. Qed.
-
-(* Conditional affinely plainly *)
-Lemma affinely_plainly_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
-Proof. by intros ->. Qed.
-
-Lemma affinely_plainly_if_elim p P : ■?p P ⊢ P.
-Proof. destruct p; simpl; auto using affinely_plainly_elim. Qed.
-Lemma affinely_plainly_affinely_plainly_if p P : ■ P ⊢ ■?p P.
-Proof. destruct p; simpl; auto using affinely_plainly_elim. Qed.
-Lemma affinely_plainly_if_intro' p P Q : (■?p P ⊢ Q) → ■?p P ⊢ ■?p Q.
-Proof. destruct p; simpl; auto using affinely_plainly_intro'. Qed.
-
-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_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_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).
-Proof. destruct p; simpl; auto using affinely_plainly_sep_2. Qed.
-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.
-
-Lemma affinely_plainly_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
-Proof. destruct p; simpl; auto using affinely_plainly_idemp. Qed.
-
 (* Properties of persistent propositions *)
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
 Proof. solve_proper. Qed.
@@ -1485,17 +1183,6 @@ Section persistent_bi_absorbing.
   Proof. apply (anti_symm _); auto using impl_wand_1, impl_wand_2. Qed.
 End persistent_bi_absorbing.
 
-(* Properties of plain propositions *)
-Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain PROP).
-Proof. solve_proper. Qed.
-
-Lemma plain_plainly_2 P `{!Plain P} : P ⊢ bi_plainly P.
-Proof. done. Qed.
-Lemma plain_plainly P `{!Plain P, !Absorbing P} : bi_plainly P ⊣⊢ P.
-Proof. apply (anti_symm _), plain_plainly_2, _. apply plainly_elim, _. Qed.
-Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ bi_plainly Q.
-Proof. by intros <-. Qed.
-
 (* Affine instances *)
 Global Instance emp_affine_l : Affine (emp%I : PROP).
 Proof. by rewrite /Affine. Qed.
@@ -1555,16 +1242,13 @@ Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_in
 
 Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance plainly_absorbing P : Absorbing (bi_plainly P).
-Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorbing. Qed.
 Global Instance persistently_absorbing P : Absorbing (bi_persistently P).
 Proof. by rewrite /Absorbing absorbingly_persistently. Qed.
+Global Instance persistently_if_absorbing P p :
+  Absorbing P → Absorbing (bi_persistently_if p P).
+Proof. intros; destruct p; simpl; apply _. Qed.
 
 (* Persistence instances *)
-(* Not an instance, see the bottom of this file *)
-Lemma plain_persistent P : Plain P → Persistent P.
-Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
-
 Global Instance pure_persistent φ : Persistent (⌜φ⌝%I : PROP).
 Proof. by rewrite /Persistent persistently_pure. Qed.
 Global Instance emp_persistent : Persistent (emp%I : PROP).
@@ -1588,19 +1272,10 @@ Proof.
   apply exist_mono=> x. by rewrite -!persistent.
 Qed.
 
-Global Instance impl_persistent P Q :
-  Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
-Proof.
-  intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
-                     -(persistent Q) (plainly_elim_absorbingly P) absorbing.
-Qed.
-
 Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
 Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
 
-Global Instance plainly_persistent P : Persistent (bi_plainly P).
-Proof. by rewrite /Persistent persistently_plainly. Qed.
 Global Instance persistently_persistent P : Persistent (bi_persistently P).
 Proof. by rewrite /Persistent persistently_idemp. Qed.
 Global Instance affinely_persistent P : Persistent P → Persistent (bi_affinely P).
@@ -1611,66 +1286,6 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
-Global Instance wand_persistent P Q :
-  Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
-Proof.
-  intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (bi_plainly P → Q)).
-  - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
-    by rewrite affinely_plainly_elim.
-  - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
-Qed.
-
-(* Plainness instances *)
-Global Instance pure_plain φ : Plain (⌜φ⌝%I : PROP).
-Proof. by rewrite /Plain plainly_pure. Qed.
-Global Instance emp_plain : Plain (emp%I : PROP).
-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_2 -!plain. Qed.
-Global Instance forall_plain {A} (Ψ : A → PROP) :
-  (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
-Proof.
-  intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain.
-Qed.
-Global Instance exist_plain {A} (Ψ : A → PROP) :
-  (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
-Proof.
-  intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
-Qed.
-
-Global Instance impl_plain P Q :
-  Absorbing P → Plain P → Plain Q → Plain (P → Q).
-Proof.
-  intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
-                     (plainly_elim_absorbingly P) absorbing.
-Qed.
-Global Instance wand_plain P Q :
-  Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q).
-Proof.
-  intros. rewrite /Plain {2}(plain P). trans (bi_plainly (bi_plainly P → Q)).
-  - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q).
-    by rewrite affinely_plainly_elim.
-  - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
-Qed.
-Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q).
-Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
-
-Global Instance plainly_plain P : Plain (bi_plainly P).
-Proof. by rewrite /Plain plainly_idemp. Qed.
-Global Instance persistently_plain P : Plain P → Plain (bi_persistently P).
-Proof.
-  rewrite /Plain=> HP. by rewrite {1}HP plainly_persistently persistently_plainly.
-Qed.
-Global Instance affinely_plain P : Plain P → Plain (bi_affinely P).
-Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_plain P : Plain P → Plain (bi_absorbingly P).
-Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance from_option_palin {A} P (Ψ : A → PROP) (mx : option A) :
-  (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
-Proof. destruct mx; apply _. Qed.
-
 (* For big ops *)
 Global Instance bi_and_monoid : Monoid (@bi_and PROP) :=
   {| monoid_unit := True%I |}.
@@ -1679,34 +1294,6 @@ Global Instance bi_or_monoid : Monoid (@bi_or PROP) :=
 Global Instance bi_sep_monoid : Monoid (@bi_sep PROP) :=
   {| monoid_unit := emp%I |}.
 
-Global Instance bi_plainly_and_homomorphism :
-  MonoidHomomorphism bi_and bi_and (≡) (@bi_plainly PROP).
-Proof.
-  split; [split|]; try apply _. apply plainly_and. apply plainly_pure.
-Qed.
-
-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 `{BiPositive PROP} :
-  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP).
-Proof. split; try apply _. apply plainly_sep. Qed.
-
-Global Instance bi_plainly_sep_homomorphism `{BiAffine PROP} :
-  MonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP).
-Proof. split. apply _. apply plainly_emp. Qed.
-
-Global Instance bi_plainly_sep_entails_weak_homomorphism :
-  WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_plainly PROP).
-Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed.
-
-Global Instance bi_plainly_sep_entails_homomorphism :
-  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_plainly PROP).
-Proof. split. apply _. simpl. apply plainly_emp_intro. Qed.
-
 Global Instance bi_persistently_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@bi_persistently PROP).
 Proof.
@@ -1779,9 +1366,6 @@ Proof.
   { intros x. symmetry; apply equiv_spec. }
   apply limit_preserving_and; by apply limit_preserving_entails.
 Qed.
-Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) :
-  NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
-Proof. intros. apply limit_preserving_entails; solve_proper. 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.
@@ -1908,48 +1492,10 @@ Proof.
   apply (internal_eq_rewrite' a b (λ b, bi_persistently (a ≡ b))%I); auto.
   rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
 Qed.
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : bi_plainly (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
-  apply (anti_symm (⊢)).
-  { by rewrite plainly_elim_absorbingly absorbingly_internal_eq. }
-  apply (internal_eq_rewrite' a b (λ  b, bi_plainly (a ≡ b))%I); [solve_proper|done|].
-  rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
-Qed.
-
-Lemma plainly_alt P : bi_plainly P ⊣⊢ bi_affinely P ≡ emp.
-Proof.
-  rewrite -plainly_affinely. apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
-    + by rewrite affinely_elim_emp left_id.
-    + by rewrite left_id.
-  - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
-    by rewrite -plainly_True_emp plainly_pure True_impl.
-Qed.
-
-Lemma plainly_alt_absorbing P `{!Absorbing P} : bi_plainly P ⊣⊢ P ≡ True.
-Proof.
-  apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
-  - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly).
-    by rewrite plainly_pure True_impl.
-Qed.
-
-Lemma plainly_True_alt P : bi_plainly (True -∗ P) ⊣⊢ P ≡ True.
-Proof.
-  apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
-    by rewrite wand_elim_r.
-  - rewrite internal_eq_sym (internal_eq_rewrite _ _
-      (λ Q, bi_plainly (True -∗ Q)) ltac:(solve_proper)).
-    by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
-Qed.
 
 Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
   Absorbing (x ≡ y : PROP)%I.
 Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-Global Instance internal_eq_plain {A : ofeT} (a b : A) :
-  Plain (a ≡ b : PROP)%I.
-Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
 Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
   Persistent (a ≡ b : PROP)%I.
 Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
@@ -2014,25 +1560,17 @@ Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q.
 Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /bi_iff later_and !later_impl. Qed.
-Lemma later_plainly P : ▷ bi_plainly P ⊣⊢ bi_plainly (▷ P).
-Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed.
 Lemma later_persistently P : ▷ bi_persistently P ⊣⊢ bi_persistently (▷ P).
 Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
 Lemma later_affinely_2 P : bi_affinely (▷ P) ⊢ ▷ bi_affinely P.
 Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
-Lemma later_affinely_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
-Proof. by rewrite -later_plainly later_affinely_2. Qed.
 Lemma later_affinely_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
 Proof. by rewrite -later_persistently later_affinely_2. Qed.
-Lemma later_affinely_plainly_if_2 p P : ■?p ▷ P ⊢ ▷ ■?p P.
-Proof. destruct p; simpl; auto using later_affinely_plainly_2. Qed.
 Lemma later_affinely_persistently_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
 Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed.
 Lemma later_absorbingly P : ▷ bi_absorbingly P ⊣⊢ bi_absorbingly (▷ P).
 Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
 
-Global Instance later_plain P : Plain P → Plain (▷ P).
-Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
 Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed.
 Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
@@ -2089,25 +1627,17 @@ Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
 Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed.
 Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
-Lemma laterN_plainly n P : ▷^n bi_plainly P ⊣⊢ bi_plainly (▷^n P).
-Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed.
 Lemma laterN_persistently n P : ▷^n bi_persistently P ⊣⊢ bi_persistently (▷^n P).
 Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
 Lemma laterN_affinely_2 n P : bi_affinely (▷^n P) ⊢ ▷^n bi_affinely P.
 Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
-Lemma laterN_affinely_plainly_2 n P : ■ ▷^n P ⊢ ▷^n ■ P.
-Proof. by rewrite -laterN_plainly laterN_affinely_2. Qed.
 Lemma laterN_affinely_persistently_2 n P : □ ▷^n P ⊢ ▷^n □ P.
 Proof. by rewrite -laterN_persistently laterN_affinely_2. Qed.
-Lemma laterN_affinely_plainly_if_2 n p P : ■?p ▷^n P ⊢ ▷^n ■?p P.
-Proof. destruct p; simpl; auto using laterN_affinely_plainly_2. Qed.
 Lemma laterN_affinely_persistently_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
 Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed.
 Lemma laterN_absorbingly n P : ▷^n (bi_absorbingly P) ⊣⊢ bi_absorbingly (▷^n P).
 Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
 
-Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
-Proof. induction n; apply _. Qed.
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
 Proof. induction n; apply _. Qed.
 Global Instance laterN_absorbing n P : Absorbing P → Absorbing (▷^n P).
@@ -2170,24 +1700,14 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
-Lemma except_0_plainly_1 P : ◇ bi_plainly P ⊢ bi_plainly (◇ P).
-Proof. by rewrite /sbi_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 /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed.
 Lemma except_0_persistently P : ◇ bi_persistently P ⊣⊢ bi_persistently (◇ P).
 Proof.
   by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure.
 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 `{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  `{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.
 Lemma except_0_absorbingly P : ◇ (bi_absorbingly P) ⊣⊢ bi_absorbingly (◇ P).
@@ -2205,8 +1725,6 @@ Proof.
   by apply and_mono, except_0_intro.
 Qed.
 
-Global Instance except_0_plain P : Plain P → Plain (◇ P).
-Proof. rewrite /sbi_except_0; apply _. Qed.
 Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
 Proof. rewrite /sbi_except_0; apply _. Qed.
 Global Instance except_0_absorbing P : Absorbing P → Absorbing (◇ P).
@@ -2263,12 +1781,6 @@ Proof.
   - rewrite /sbi_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
-Global Instance plainly_timeless P  `{BiPlainlyExist PROP} :
-  Timeless P → Timeless (bi_plainly P).
-Proof.
-  intros. rewrite /Timeless /sbi_except_0 later_plainly_1.
-  by rewrite (timeless P) /sbi_except_0 plainly_or {1}plainly_elim.
-Qed.
 Global Instance persistently_timeless P : Timeless P → Timeless (bi_persistently P).
 Proof.
   intros. rewrite /Timeless /sbi_except_0 later_persistently_1.
@@ -2350,12 +1862,3 @@ Global Instance sbi_except_0_sep_entails_homomorphism :
 Proof. split; try apply _. apply except_0_intro. Qed.
 End sbi_derived.
 End bi.
-
-(* When declared as an actual instance, [plain_persistent] will cause
-failing proof searches to take exponential time, as Coq will try to
-apply it the instance at any node in the proof search tree.
-
-To avoid that, we declare it using a [Hint Immediate], so that it will
-only be used at the leaves of the proof search tree, i.e. when the
-premise of the hint can be derived from just the current context. *)
-Hint Immediate bi.plain_persistent : typeclass_instances.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 957a827d902cd0fd9488d5f2a4f36dc081bcac3a..9e87934026878d873b99824805952bc4b7c11274 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import monoid.
-From iris.bi Require Import interface derived_laws big_op.
+From iris.bi Require Import interface derived_laws big_op plainly.
 From stdpp Require Import hlist.
 
 Class Embed (A B : Type) := embed : A → B.
@@ -21,7 +21,6 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
   bi_embed_mixin_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
   bi_embed_mixin_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
-  bi_embed_mixin_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤;
   bi_embed_mixin_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
 }.
 
@@ -35,7 +34,8 @@ Arguments bi_embed_embed : simpl never.
 
 Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
   embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
-  embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
+  embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤;
+  embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢ (P ≡ Q : PROP');
 }.
 
 Section embed_laws.
@@ -62,8 +62,6 @@ Section embed_laws.
   Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
   Lemma embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤.
   Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
-  Lemma embed_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤.
-  Proof. eapply bi_embed_mixin_plainly, bi_embed_mixin. Qed.
   Lemma embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤.
   Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
 End embed_laws.
@@ -121,6 +119,7 @@ Section embed.
       last apply bi.True_intro.
     apply bi.impl_intro_l. by rewrite right_id.
   Qed.
+
   Lemma embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤).
   Proof. by rewrite embed_and !embed_impl. Qed.
   Lemma embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
@@ -129,8 +128,6 @@ Section embed.
   Proof. by rewrite embed_and embed_emp. Qed.
   Lemma embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
   Proof. by rewrite embed_sep embed_pure. Qed.
-  Lemma embed_plainly_if P b : ⎡bi_plainly_if b P⎤ ⊣⊢ bi_plainly_if b ⎡P⎤.
-  Proof. destruct b; simpl; auto using embed_plainly. Qed.
   Lemma embed_persistently_if P b :
     ⎡bi_persistently_if b P⎤ ⊣⊢ bi_persistently_if b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_persistently. Qed.
@@ -143,8 +140,6 @@ Section embed.
     ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose embed Φ).
   Proof. induction As=>//. rewrite /= embed_exist. by do 2 f_equiv. Qed.
 
-  Global Instance embed_plain P : Plain P → Plain ⎡P⎤.
-  Proof. intros ?. by rewrite /Plain -embed_plainly -plain. Qed.
   Global Instance embed_persistent P : Persistent P → Persistent ⎡P⎤.
   Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed.
   Global Instance embed_affine P : Affine P → Affine ⎡P⎤.
@@ -201,8 +196,26 @@ Section sbi_embed.
   Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
   Proof. by rewrite embed_or embed_later embed_pure. Qed.
 
+  Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
+  Proof.
+    rewrite !plainly_alt embed_internal_eq. apply (anti_symm _).
+    - rewrite -embed_affinely -embed_emp. apply bi.f_equiv, _.
+    - by rewrite -embed_affinely -embed_emp embed_interal_inj.
+  Qed.
+  Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
+  Proof. destruct p; simpl; auto using embed_plainly. Qed.
+
+  Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} P : Plain P → Plain ⎡P⎤.
+  Proof. intros ?. by rewrite /Plain -embed_plainly -plain. Qed.
+
   Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
   Proof.
     intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
   Qed.
 End sbi_embed.
+
+(* Not defined using an ordinary [Instance] because the default
+[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
+search for the other premises fail. See the proof of [monPred_absolutely_plain]
+for an example where it would fail with a regular [Instance].*)
+Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 56ef28240860537cdbcf442ddaf8f89b986742b5..5fd4fa0e9276b76487da0cfcda71b188aac3e68b 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -9,7 +9,7 @@ Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "â–· P" (at level 20, right associativity).
 
 Section bi_mixin.
-  Context {PROP : Type} `{Dist PROP, Equiv PROP} (prop_ofe_mixin : OfeMixin PROP).
+  Context {PROP : Type} `{Dist PROP, Equiv PROP}.
   Context (bi_entails : PROP → PROP → Prop).
   Context (bi_emp : PROP).
   Context (bi_pure : Prop → PROP).
@@ -20,7 +20,6 @@ Section bi_mixin.
   Context (bi_exist : ∀ A, (A → PROP) → PROP).
   Context (bi_sep : PROP → PROP → PROP).
   Context (bi_wand : PROP → PROP → PROP).
-  Context (bi_plainly : PROP → PROP).
   Context (bi_persistently : PROP → PROP).
   Context (sbi_internal_eq : ∀ A : ofeT, A → A → PROP).
   Context (sbi_later : PROP → PROP).
@@ -68,7 +67,6 @@ Section bi_mixin.
       Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
     bi_mixin_sep_ne : NonExpansive2 bi_sep;
     bi_mixin_wand_ne : NonExpansive2 bi_wand;
-    bi_mixin_plainly_ne : NonExpansive bi_plainly;
     bi_mixin_persistently_ne : NonExpansive bi_persistently;
 
     (* Higher-order logic *)
@@ -102,26 +100,6 @@ Section bi_mixin.
     bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R;
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
 
-    (* Plainly *)
-    (* Note: plainly is about to be removed from this interface *)
-    bi_mixin_plainly_mono P Q : (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q;
-    bi_mixin_plainly_elim_persistently P : bi_plainly P ⊢ bi_persistently P;
-    bi_mixin_plainly_idemp_2 P : bi_plainly P ⊢ bi_plainly (bi_plainly P);
-
-    bi_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
-      (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a);
-
-    (* The following two laws are very similar, and indeed they hold not just
-       for persistently and plainly, but for any modality defined as `M P n x :=
-       ∀ y, R x y → P n y`. *)
-    bi_mixin_persistently_impl_plainly P Q :
-      (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q);
-    bi_mixin_plainly_impl_plainly P Q :
-      (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q);
-
-    bi_mixin_plainly_emp_intro P : P ⊢ bi_plainly emp;
-    bi_mixin_plainly_absorbing P Q : bi_plainly P ∗ Q ⊢ bi_plainly P;
-
     (* Persistently *)
     (* In the ordered RA model: Holds without further assumptions. *)
     bi_mixin_persistently_mono P Q :
@@ -130,8 +108,8 @@ Section bi_mixin.
     bi_mixin_persistently_idemp_2 P :
       bi_persistently P ⊢ bi_persistently (bi_persistently P);
 
-    (* In the ordered RA model [P ⊢ persisently emp] (which can currently still
-    be derived from the plainly axioms, which will be removed): `ε ≼ core x` *)
+    (* In the ordered RA model: `ε ≼ core x` *)
+    bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
       (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
@@ -158,8 +136,6 @@ Section bi_mixin.
     sbi_mixin_fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g;
     sbi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y;
     sbi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝;
-    sbi_mixin_prop_ext P Q : bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢
-      sbi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
 
     (* Later *)
     sbi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y);
@@ -173,8 +149,6 @@ Section bi_mixin.
       (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
     sbi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
     sbi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
-    sbi_mixin_later_plainly_1 P : ▷ bi_plainly P ⊢ bi_plainly (▷ P);
-    sbi_mixin_later_plainly_2 P : bi_plainly (▷ P) ⊢ ▷ bi_plainly P;
     sbi_mixin_later_persistently_1 P :
       ▷ bi_persistently P ⊢ bi_persistently (▷ P);
     sbi_mixin_later_persistently_2 P :
@@ -198,11 +172,10 @@ Structure bi := Bi {
   bi_exist : ∀ A, (A → bi_car) → bi_car;
   bi_sep : bi_car → bi_car → bi_car;
   bi_wand : bi_car → bi_car → bi_car;
-  bi_plainly : bi_car → bi_car;
   bi_persistently : bi_car → bi_car;
   bi_ofe_mixin : OfeMixin bi_car;
   bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
-                        bi_exist bi_sep bi_wand bi_plainly bi_persistently;
+                        bi_exist bi_sep bi_wand bi_persistently;
 }.
 
 Coercion bi_ofeC (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
@@ -218,7 +191,6 @@ Instance: Params (@bi_forall) 2.
 Instance: Params (@bi_exist) 2.
 Instance: Params (@bi_sep) 1.
 Instance: Params (@bi_wand) 1.
-Instance: Params (@bi_plainly) 1.
 Instance: Params (@bi_persistently) 1.
 
 Delimit Scope bi_scope with I.
@@ -235,7 +207,6 @@ Arguments bi_forall {PROP _} _%I : simpl never, rename.
 Arguments bi_exist {PROP _} _%I : simpl never, rename.
 Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
 Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
-Arguments bi_plainly {PROP} _%I : simpl never, rename.
 Arguments bi_persistently {PROP} _%I : simpl never, rename.
 
 Structure sbi := Sbi {
@@ -252,17 +223,15 @@ Structure sbi := Sbi {
   sbi_exist : ∀ A, (A → sbi_car) → sbi_car;
   sbi_sep : sbi_car → sbi_car → sbi_car;
   sbi_wand : sbi_car → sbi_car → sbi_car;
-  sbi_plainly : sbi_car → sbi_car;
   sbi_persistently : sbi_car → sbi_car;
   sbi_internal_eq : ∀ A : ofeT, A → A → sbi_car;
   sbi_later : sbi_car → sbi_car;
   sbi_ofe_mixin : OfeMixin sbi_car;
   sbi_bi_mixin : BiMixin sbi_entails sbi_emp sbi_pure sbi_and sbi_or sbi_impl
-                         sbi_forall sbi_exist sbi_sep sbi_wand sbi_plainly
-                         sbi_persistently;
-  sbi_sbi_mixin : SbiMixin sbi_ofe_mixin sbi_entails sbi_pure sbi_and sbi_or
-                           sbi_impl sbi_forall sbi_exist sbi_sep sbi_wand
-                           sbi_plainly sbi_persistently sbi_internal_eq sbi_later;
+                         sbi_forall sbi_exist sbi_sep sbi_wand sbi_persistently;
+  sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl
+                           sbi_forall sbi_exist sbi_sep
+                           sbi_persistently sbi_internal_eq sbi_later;
 }.
 
 Instance: Params (@sbi_later) 1.
@@ -290,7 +259,6 @@ Arguments sbi_forall {PROP _} _%I : simpl never, rename.
 Arguments sbi_exist {PROP _} _%I : simpl never, rename.
 Arguments sbi_sep {PROP} _%I _%I : simpl never, rename.
 Arguments sbi_wand {PROP} _%I _%I : simpl never, rename.
-Arguments sbi_plainly {PROP} _%I : simpl never, rename.
 Arguments sbi_persistently {PROP} _%I : simpl never, rename.
 Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
 Arguments sbi_later {PROP} _%I : simpl never, rename.
@@ -366,8 +334,6 @@ Global Instance sep_ne : NonExpansive2 (@bi_sep PROP).
 Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed.
 Global Instance wand_ne : NonExpansive2 (@bi_wand PROP).
 Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed.
-Global Instance plainly_ne : NonExpansive (@bi_plainly PROP).
-Proof. eapply bi_mixin_plainly_ne, bi_bi_mixin. Qed.
 Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
 Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed.
 
@@ -424,27 +390,6 @@ Proof. eapply bi_mixin_wand_intro_r, bi_bi_mixin. Qed.
 Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
 Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
-(* Plainly *)
-Lemma plainly_mono P Q : (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q.
-Proof. eapply bi_mixin_plainly_mono, bi_bi_mixin. Qed.
-Lemma plainly_elim_persistently P : bi_plainly P ⊢ bi_persistently P.
-Proof. eapply bi_mixin_plainly_elim_persistently, bi_bi_mixin. Qed.
-Lemma plainly_idemp_2 P : bi_plainly P ⊢ bi_plainly (bi_plainly P).
-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 persistently_impl_plainly P Q :
-  (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q).
-Proof. eapply bi_mixin_persistently_impl_plainly, bi_bi_mixin. Qed.
-Lemma plainly_impl_plainly P Q :
-  (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q).
-Proof. eapply bi_mixin_plainly_impl_plainly, bi_bi_mixin. Qed.
-Lemma plainly_absorbing P Q : bi_plainly P ∗ Q ⊢ bi_plainly P.
-Proof. eapply (bi_mixin_plainly_absorbing bi_entails), bi_bi_mixin. Qed.
-Lemma plainly_emp_intro P : P ⊢ bi_plainly emp.
-Proof. eapply bi_mixin_plainly_emp_intro, bi_bi_mixin. Qed.
-
 (* Persistently *)
 Lemma persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
 Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
@@ -452,6 +397,9 @@ Lemma persistently_idemp_2 P :
   bi_persistently P ⊢ bi_persistently (bi_persistently P).
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
+Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
+Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
+
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
 Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
@@ -488,9 +436,6 @@ Lemma discrete_eq_1 {A : ofeT} (a b : A) :
   Discrete a → a ≡ b ⊢ (⌜a ≡ b⌝ : PROP).
 Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
 
-Lemma prop_ext P Q : bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
-Proof. eapply (sbi_mixin_prop_ext _ bi_entails), sbi_sbi_mixin. Qed.
-
 (* Later *)
 Global Instance later_contractive : Contractive (@sbi_later PROP).
 Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed.
@@ -514,14 +459,10 @@ Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
 Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
 Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
 Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
-Lemma later_plainly_1 P : ▷ bi_plainly P ⊢ bi_plainly (▷ P).
-Proof. eapply (sbi_mixin_later_plainly_1 _ bi_entails), sbi_sbi_mixin. Qed.
-Lemma later_plainly_2 P : bi_plainly (▷ P) ⊢ ▷ bi_plainly P.
-Proof. eapply (sbi_mixin_later_plainly_2 _ bi_entails), sbi_sbi_mixin. Qed.
 Lemma later_persistently_1 P : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
-Proof. eapply (sbi_mixin_later_persistently_1 _ bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
 Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
-Proof. eapply (sbi_mixin_later_persistently_2 _ bi_entails), sbi_sbi_mixin. Qed.
+Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
 
 Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
 Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 3e37b6d53609fd6e5c20863818898804a8a7347a..606cc00260d7004cc6f26adc5939a6635da23d38 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -140,11 +140,6 @@ Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
 Definition monPred_pure := unseal monPred_pure_aux.
 Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _.
 
-Definition monPred_plainly_def P : monPred := MonPred (λ _, ∀ i, bi_plainly (P i))%I _.
-Definition monPred_plainly_aux : seal (@monPred_plainly_def). by eexists. Qed.
-Definition monPred_plainly := unseal monPred_plainly_aux.
-Definition monPred_plainly_eq : @monPred_plainly = _ := seal_eq _.
-
 Definition monPred_absolutely_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
 Definition monPred_absolutely_aux : seal (@monPred_absolutely_def). by eexists. Qed.
 Definition monPred_absolutely := unseal monPred_absolutely_aux.
@@ -238,6 +233,11 @@ Implicit Types i : I.
 Notation monPred := (monPred I PROP).
 Implicit Types P Q : monPred.
 
+Definition monPred_plainly_def `{BiPlainly PROP} P : monPred := MonPred (λ _, ∀ i, ■ (P i))%I _.
+Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. by eexists. Qed.
+Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := unseal monPred_plainly_aux.
+Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := seal_eq _.
+
 Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _.
 Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
 Definition monPred_internal_eq := unseal monPred_internal_eq_aux.
@@ -272,10 +272,10 @@ Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
          monPred_upclosed, bi_and, bi_or,
          bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
-         bi_persistently, bi_affinely, bi_plainly, sbi_later;
+         bi_persistently, bi_affinely, sbi_later;
   simpl;
   unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
-         sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly;
+         sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently;
   simpl;
   rewrite !unseal_eqs /=.
 End MonPred.
@@ -287,7 +287,7 @@ Context (I : biIndex) (PROP : bi).
 Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
   monPred_entails monPred_emp monPred_pure monPred_and monPred_or
   monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
-  monPred_plainly monPred_persistently.
+  monPred_persistently.
 Proof.
   split; try unseal; try by (split=> ? /=; repeat f_equiv).
   - split.
@@ -325,26 +325,9 @@ Proof.
     apply bi.wand_intro_r. by rewrite -HR /= !Hij.
   - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'.
     rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
-  - intros P Q [?]. split=> i /=. by do 3 f_equiv.
-  - intros P. split=> i /=. by rewrite bi.forall_elim bi.plainly_elim_persistently.
-  - intros P. split=> i /=. repeat setoid_rewrite <-bi.plainly_forall.
-    rewrite -bi.plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
-  - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
-    rewrite bi.plainly_forall. apply bi.forall_intro=> a.
-    by rewrite !bi.forall_elim.
-  - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
-    repeat setoid_rewrite <-bi.plainly_forall.
-    repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv.
-    apply bi.persistently_impl_plainly.
-  - intros P Q. split=> i /=.
-    repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
-    repeat setoid_rewrite <-bi.plainly_forall.
-    setoid_rewrite bi.plainly_impl_plainly. f_equiv.
-    do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
-  - intros P. split=> i /=. apply bi.forall_intro=>_. by apply bi.plainly_emp_intro.
-  - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
+  - intros P. split=> i. by apply bi.persistently_emp_intro.
   - intros A Ψ. split=> i. by apply bi.persistently_forall_2.
   - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
@@ -352,20 +335,16 @@ Proof.
 Qed.
 
 Canonical Structure monPredI : bi :=
-  Bi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
-     monPred_pure monPred_and monPred_or monPred_impl monPred_forall
-     monPred_exist monPred_sep monPred_wand monPred_plainly monPred_persistently
-     monPred_ofe_mixin monPred_bi_mixin.
+  {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin |}.
 End canonical_bi.
 
 Section canonical_sbi.
 Context (I : biIndex) (PROP : sbi).
 
 Lemma monPred_sbi_mixin :
-  SbiMixin (PROP:=monPred I PROP) monPred_ofe_mixin monPred_entails monPred_pure
-           monPred_and monPred_or monPred_impl monPred_forall monPred_exist
-           monPred_sep monPred_wand monPred_plainly monPred_persistently
-           monPred_internal_eq monPred_later.
+  SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
+           monPred_or monPred_impl monPred_forall monPred_exist
+           monPred_sep monPred_persistently monPred_internal_eq monPred_later.
 Proof.
   split; unseal.
   - intros n P Q HPQ. split=> i /=.
@@ -378,11 +357,6 @@ Proof.
   - intros A1 A2 f g. split=> i. by apply bi.fun_ext.
   - intros A P x y. split=> i. by apply bi.sig_eq.
   - intros A a b ?. split=> i. by apply bi.discrete_eq_1.
-  - intros P Q. split=> i /=.
-    rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _).
-    rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j.
-    rewrite -bi.prop_ext !(bi.forall_elim j) !bi.pure_impl_forall
-            !bi.forall_elim //.
   - intros A x y. split=> i. by apply bi.later_eq_1.
   - intros A x y. split=> i. by apply bi.later_eq_2.
   - intros P Q [?]. split=> i. by apply bi.later_mono.
@@ -392,10 +366,6 @@ Proof.
   - intros A Ψ. split=> i. by apply bi.later_exist_false.
   - intros P Q. split=> i. by apply bi.later_sep_1.
   - intros P Q. split=> i. by apply bi.later_sep_2.
-  - intros P. split=> i /=.
-    rewrite bi.later_forall. f_equiv=> j. by rewrite -bi.later_plainly_1.
-  - intros P. split=> i /=.
-    rewrite bi.later_forall. f_equiv=> j. by rewrite -bi.later_plainly_2.
   - intros P. split=> i. by apply bi.later_persistently_1.
   - intros P. split=> i. by apply bi.later_persistently_2.
   - intros P. split=> i /=. rewrite -bi.forall_intro. apply bi.later_false_em.
@@ -403,12 +373,50 @@ Proof.
 Qed.
 
 Canonical Structure monPredSI : sbi :=
-  Sbi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp
-      monPred_pure monPred_and monPred_or monPred_impl monPred_forall
-      monPred_exist monPred_sep monPred_wand monPred_plainly
-      monPred_persistently monPred_internal_eq monPred_later monPred_ofe_mixin
-      (bi_bi_mixin _) monPred_sbi_mixin.
+  {| sbi_ofe_mixin := monPred_ofe_mixin; sbi_bi_mixin := monPred_bi_mixin I PROP;
+     sbi_sbi_mixin := monPred_sbi_mixin |}.
 
+Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredSI monPred_plainly.
+Proof.
+  split; unseal.
+  - by (split=> ? /=; repeat f_equiv).
+  - intros P Q [?]. split=> i /=. by do 3 f_equiv.
+  - intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently.
+  - intros P. split=> i /=. repeat setoid_rewrite <-plainly_forall.
+    rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
+  - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
+    rewrite plainly_forall. apply bi.forall_intro=> a.
+    by rewrite !bi.forall_elim.
+  - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
+    repeat setoid_rewrite <-plainly_forall.
+    repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv.
+    apply persistently_impl_plainly.
+  - intros P Q. split=> i /=.
+    repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
+    repeat setoid_rewrite <-plainly_forall.
+    setoid_rewrite plainly_impl_plainly. f_equiv.
+    do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
+  - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
+  - intros P Q. split=> i. apply bi.sep_elim_l, _.
+  - intros P Q. split=> i /=.
+    rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _).
+    rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j.
+    rewrite -prop_ext !(bi.forall_elim j) !bi.pure_impl_forall
+            !bi.forall_elim //.
+  - intros P. split=> i /=.
+    rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
+  - intros P. split=> i /=.
+    rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
+Qed.
+Global Instance monPred_plainlyC `{BiPlainly PROP} : BiPlainly monPredSI :=
+  {| bi_plainly_mixin := monPred_plainly_mixin |}.
+
+Global Instance monPred_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
+  BiPlainlyExist PROP → BiPlainlyExist monPredSI.
+Proof.
+  split=>?/=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
+  apply bi.forall_intro=>?. by do 2 f_equiv.
+Qed.
 End canonical_sbi.
 
 Class Absolute {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
@@ -451,17 +459,8 @@ Proof. split => ?. unseal. apply bi_positive. Qed.
 Global Instance monPred_affine : BiAffine PROP → BiAffine monPredI.
 Proof. split => ?. unseal. by apply affine. Qed.
 
-Global Instance monPred_plainly_exist `{BiIndexBottom bot} :
-  BiPlainlyExist PROP → BiPlainlyExist monPredI.
-Proof.
-  split=>?/=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
-  apply bi.forall_intro=>?. by do 2 f_equiv.
-Qed.
-
 Global Instance monPred_at_persistent P i : Persistent P → Persistent (P i).
 Proof. move => [] /(_ i). by unseal. Qed.
-Global Instance monPred_at_plain P i : Plain P → Plain (P i).
-Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed.
 Global Instance monPred_at_absorbing P i : Absorbing P → Absorbing (P i).
 Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
 Global Instance monPred_at_affine P i : Affine P → Affine (P i).
@@ -484,8 +483,6 @@ Proof.
     by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
   - split=>? /=.
     by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
-  - intros ?. split => ? /=. apply bi.equiv_spec; split.
-    by apply bi.forall_intro. by rewrite bi.forall_elim.
 Qed.
 Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
   {| bi_embed_mixin := monPred_embedding_mixin |}.
@@ -494,8 +491,6 @@ Lemma monPred_emp_unfold : emp%I = ⎡emp : PROP⎤%I.
 Proof. by unseal. Qed.
 Lemma monPred_pure_unfold : bi_pure = λ φ, ⎡ ⌜ φ ⌝ : PROP⎤%I.
 Proof. by unseal. Qed.
-Lemma monPred_plainly_unfold : bi_plainly = λ P, ⎡ ∀ i, bi_plainly (P i) ⎤%I.
-Proof. by unseal. Qed.
 Lemma monPred_absolutely_unfold : monPred_absolutely = λ P, ⎡∀ i, P i⎤%I.
 Proof. by unseal. Qed.
 Lemma monPred_relatively_unfold : monPred_relatively = λ P, ⎡∃ i, P i⎤%I.
@@ -513,8 +508,6 @@ Global Instance monPred_absolutely_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@monPred_absolutely I PROP).
 Proof. intros ???. by apply monPred_absolutely_mono. Qed.
 
-Global Instance monPred_absolutely_plain P : Plain P → Plain (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
 Global Instance monPred_absolutely_persistent P : Persistent P → Persistent (∀ᵢ P).
 Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
 Global Instance monPred_absolutely_absorbing P : Absorbing P → Absorbing (∀ᵢ P).
@@ -534,8 +527,6 @@ Global Instance monPred_relatively_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@monPred_relatively I PROP).
 Proof. intros ???. by apply monPred_relatively_mono. Qed.
 
-Global Instance monPred_relatively_plain P : Plain P → Plain (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
 Global Instance monPred_relatively_persistent P : Persistent P → Persistent (∃ᵢ P).
 Proof. rewrite monPred_relatively_unfold. apply _. Qed.
 Global Instance monPred_relatively_absorbing P : Absorbing P → Absorbing (∃ᵢ P).
@@ -550,8 +541,6 @@ Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i ⊣⊢ ⌜φ⌝.
 Proof. by unseal. Qed.
 Lemma monPred_at_emp i : monPred_at emp i ⊣⊢ emp.
 Proof. by unseal. Qed.
-Lemma monPred_at_plainly i P : bi_plainly P i ⊣⊢ ∀ j, bi_plainly (P j).
-Proof. by unseal. Qed.
 Lemma monPred_at_and i P Q : (P ∧ Q) i ⊣⊢ P i ∧ Q i.
 Proof. by unseal. Qed.
 Lemma monPred_at_or i P Q : (P ∨ Q) i ⊣⊢ P i ∨ Q i.
@@ -679,8 +668,6 @@ Global Instance pure_absolute φ : @Absolute I PROP ⌜φ⌝.
 Proof. intros ??. by unseal. Qed.
 Global Instance emp_absolute : @Absolute I PROP emp.
 Proof. intros ??. by unseal. Qed.
-Global Instance plainly_absolute P : Absolute (bi_plainly P).
-Proof. intros ??. by unseal. Qed.
 Global Instance absolutely_absolute P : Absolute (∀ᵢ P).
 Proof. intros ??. by unseal. Qed.
 Global Instance relatively_absolute P : Absolute (∃ᵢ P).
@@ -722,9 +709,6 @@ Proof. rewrite /bi_affinely. apply _. Qed.
 Global Instance absorbingly_absolute P `{!Absolute P} :
   Absolute (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance plainly_if_absolute P p `{!Absolute P} :
-  Absolute (bi_plainly_if p P).
-Proof. rewrite /bi_plainly_if. destruct p; apply _. Qed.
 Global Instance persistently_if_absolute P p `{!Absolute P} :
   Absolute (bi_persistently_if p P).
 Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
@@ -847,8 +831,6 @@ Proof.
   - intros P Q. split=> /= i. apply bi.forall_intro=>?.
     rewrite bi.pure_impl_forall. apply bi.forall_intro=><-.
     rewrite -bupd_frame_r bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
-  - intros P. split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall
-      bi.forall_elim // -bi.plainly_forall bupd_plainly bi.forall_elim //.
 Qed.
 Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
   {| bi_bupd_mixin := monPred_bupd_mixin |}.
@@ -895,8 +877,13 @@ Proof.
 Qed.
 
 Global Instance monPred_sbi_embed : SbiEmbed PROP monPredSI.
-Proof. split; try apply _; by unseal. Qed.
+Proof.
+  split; unseal=> //. intros ? P Q.
+  apply (@bi.f_equiv _ _ _ (λ P, monPred_at P inhabitant)); solve_proper.
+Qed.
 
+Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■ (P i) ⎤%I.
+Proof. by unseal. Qed.
 Lemma monPred_internal_eq_unfold : @sbi_internal_eq monPredSI = λ A x y, ⎡ x ≡ y ⎤%I.
 Proof. by unseal. Qed.
 
@@ -920,12 +907,6 @@ Proof.
   - intros E1 E2 P Q. split=>/= i. setoid_rewrite bi.pure_impl_forall.
     do 2 setoid_rewrite bi.sep_forall_r. setoid_rewrite fupd_frame_r.
     by repeat f_equiv.
-  - intros E1 E2 E2' P Q ? HE12. split=>/= i. repeat setoid_rewrite bi.pure_impl_forall.
-    do 4 f_equiv. rewrite 4?bi.forall_elim // fupd_plain' //.
-    apply bi.wand_intro_r. rewrite bi.wand_elim_l. do 2 apply bi.forall_intro=>?.
-    repeat f_equiv=>//. do 2 apply bi.forall_intro=>?. repeat f_equiv. by etrans.
-  - intros E P ?. split=>/= i. setoid_rewrite bi.pure_impl_forall.
-    do 2 setoid_rewrite bi.later_forall. do 4 f_equiv. apply later_fupd_plain, _.
 Qed.
 Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredSI :=
   {| bi_fupd_mixin := monPred_fupd_mixin |}.
@@ -935,7 +916,30 @@ Proof.
   intros E P. split=>/= i. by setoid_rewrite bupd_fupd.
 Qed.
 
+Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredSI.
+Proof.
+  rewrite /BiBUpdPlainly=> P; unseal.
+  split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall.
+  by rewrite bi.forall_elim // -plainly_forall bupd_plainly bi.forall_elim.
+Qed.
+
+Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i).
+Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed.
+
+Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
+Proof.
+  split; unseal.
+  - intros E1 E2 E2' P Q ? HE12. split=>/= i. repeat setoid_rewrite bi.pure_impl_forall.
+    do 4 f_equiv. rewrite 4?bi.forall_elim // fupd_plain' //.
+    apply bi.wand_intro_r. rewrite bi.wand_elim_l. do 2 apply bi.forall_intro=>?.
+    repeat f_equiv=>//. do 2 apply bi.forall_intro=>?. repeat f_equiv. by etrans.
+  - intros E P ?. split=>/= i. setoid_rewrite bi.pure_impl_forall.
+    do 2 setoid_rewrite bi.later_forall. do 4 f_equiv. apply later_fupd_plain, _.
+Qed.
+
 (** Unfolding lemmas *)
+Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
+Proof. by unseal. Qed.
 Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
   @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
 Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
@@ -968,7 +972,18 @@ Proof.
                -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI.
 Qed.
 
+Global Instance monPred_absolutely_plain `{BiPlainly PROP} P : Plain P → Plain (∀ᵢ P).
+Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
+Global Instance monPred_relatively_plain `{BiPlainly PROP} P : Plain P → Plain (∃ᵢ P).
+Proof. rewrite monPred_relatively_unfold. apply _. Qed.
+
 (** Absolute  *)
+Global Instance plainly_absolute `{BiPlainly PROP} P : Absolute (â–  P).
+Proof. intros ??. by unseal. Qed.
+Global Instance plainly_if_absolute `{BiPlainly PROP} P p `{!Absolute P} :
+  Absolute (â– ?p P).
+Proof. rewrite /plainly_if. destruct p; apply _. Qed.
+
 Global Instance internal_eq_absolute {A : ofeT} (x y : A) :
   @Absolute I PROP (x ≡ y)%I.
 Proof. intros ??. by unseal. Qed.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
new file mode 100644
index 0000000000000000000000000000000000000000..0a553169f3d9abdcc4ff6ca1f4bb817916257ef9
--- /dev/null
+++ b/theories/bi/plainly.v
@@ -0,0 +1,527 @@
+From iris.bi Require Export derived_laws.
+From iris.algebra Require Import monoid.
+Import interface.bi derived_laws.bi.
+
+Class Plainly (A : Type) := plainly : A → A.
+Hint Mode Plainly ! : typeclass_instances.
+Instance: Params (@plainly) 2.
+Notation "â–  P" := (plainly P)%I
+  (at level 20, right associativity) : bi_scope.
+
+Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
+  bi_plainly_mixin_plainly_ne : NonExpansive plainly;
+
+  bi_plainly_mixin_plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q;
+  bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ bi_persistently P;
+  bi_plainly_mixin_plainly_idemp_2 P : ■ P ⊢ ■ ■ P;
+
+  bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
+    (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a);
+
+  (* The following two laws are very similar, and indeed they hold not just
+     for persistently and plainly, but for any modality defined as `M P n x :=
+     ∀ y, R x y → P n y`. *)
+  bi_plainly_mixin_persistently_impl_plainly P Q :
+    (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q);
+  bi_plainly_mixin_plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q);
+
+  bi_plainly_mixin_plainly_emp_intro P : P ⊢ ■ emp;
+  bi_plainly_mixin_plainly_absorb P Q : ■ P ∗ Q ⊢ ■ P;
+
+  bi_plainly_mixin_prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
+
+  bi_plainly_mixin_later_plainly_1 P : ▷ ■ P ⊢ ■ ▷ P;
+  bi_plainly_mixin_later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P;
+}.
+
+Class BiPlainly (PROP : sbi) := {
+  bi_plainly_plainly :> Plainly PROP;
+  bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
+}.
+Hint Mode BiPlainly ! : typeclass_instances.
+Arguments bi_plainly_plainly : simpl never.
+
+Class BiPlainlyExist `{!BiPlainly PROP} :=
+  plainly_exist_1 A (Ψ : A → PROP) :
+    ■ (∃ a, Ψ a) ⊢ ∃ a, ■ (Ψ a).
+Arguments BiPlainlyExist : clear implicits.
+Arguments BiPlainlyExist _ {_}.
+Arguments plainly_exist_1 _ {_ _} _.
+Hint Mode BiPlainlyExist + ! : typeclass_instances.
+
+Section plainly_laws.
+  Context `{BiPlainly PROP}.
+  Implicit Types P Q : PROP.
+
+  Global Instance plainly_ne : NonExpansive (@plainly PROP _).
+  Proof. eapply bi_plainly_mixin_plainly_ne, bi_plainly_mixin. Qed.
+
+  Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
+  Proof. eapply bi_plainly_mixin_plainly_mono, bi_plainly_mixin. Qed.
+  Lemma plainly_elim_persistently P : ■ P ⊢ bi_persistently P.
+  Proof. eapply bi_plainly_mixin_plainly_elim_persistently, bi_plainly_mixin. Qed.
+  Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
+  Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed.
+  Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a).
+  Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed.
+  Lemma persistently_impl_plainly P Q :
+    (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q).
+  Proof. eapply bi_plainly_mixin_persistently_impl_plainly, bi_plainly_mixin. Qed.
+  Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
+  Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed.
+  Lemma plainly_absorb P Q : ■ P ∗ Q ⊢ ■ P.
+  Proof. eapply bi_plainly_mixin_plainly_absorb, bi_plainly_mixin. Qed.
+  Lemma plainly_emp_intro P : P ⊢ ■ emp.
+  Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed.
+
+  Lemma prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+  Proof. eapply bi_plainly_mixin_prop_ext, bi_plainly_mixin. Qed.
+
+  Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ (▷ P).
+  Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed.
+  Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
+  Proof. eapply bi_plainly_mixin_later_plainly_2, bi_plainly_mixin. Qed.
+End plainly_laws.
+
+(* Derived properties and connectives *)
+Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
+Arguments Plain {_ _} _%I : simpl never.
+Arguments plain {_ _} _%I {_}.
+Hint Mode Plain + ! ! : typeclass_instances.
+Instance: Params (@Plain) 1.
+
+Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
+  (if p then â–  P else P)%I.
+Arguments plainly_if {_ _} !_ _%I /.
+Instance: Params (@plainly_if) 2.
+Typeclasses Opaque plainly_if.
+
+Notation "â– ? p P" := (plainly_if p P)%I
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "â– ? p  P") : bi_scope.
+
+(* Derived laws *)
+Section plainly_derived.
+Context `{BiPlainly PROP}.
+Implicit Types P : PROP.
+
+Hint Resolve pure_intro forall_intro.
+Hint Resolve or_elim or_intro_l' or_intro_r'.
+Hint Resolve and_intro and_elim_l' and_elim_r'.
+
+Global Instance plainly_proper :
+  Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _) := ne_proper _.
+
+Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@plainly PROP _).
+Proof. intros P Q; apply plainly_mono. Qed.
+Global Instance plainly_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
+Proof. intros P Q; apply plainly_mono. Qed.
+
+Lemma affinely_plainly_elim P : bi_affinely (■ P) ⊢ P.
+Proof. by rewrite plainly_elim_persistently affinely_persistently_elim. Qed.
+
+Lemma persistently_plainly P : bi_persistently (■ P) ⊣⊢ ■ P.
+Proof.
+  apply (anti_symm _).
+  - by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorb.
+  - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
+Qed.
+Lemma persistently_if_plainly P p : bi_persistently_if p (■ P) ⊣⊢ ■ P.
+Proof. destruct p; last done. exact: persistently_plainly. Qed.
+
+Lemma plainly_persistently P : ■ (bi_persistently P) ⊣⊢ ■ P.
+Proof.
+  apply (anti_symm _).
+  - rewrite -{1}(left_id True%I bi_and (â–  _)%I) (plainly_emp_intro True%I).
+    rewrite -{2}(persistently_and_emp_elim P).
+    rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
+  - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
+Qed.
+
+Lemma absorbingly_plainly P : bi_absorbingly (■ P) ⊣⊢ ■ P.
+Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed.
+
+Lemma plainly_and_sep_elim P Q : ■ P ∧ Q -∗ (emp ∧ P) ∗ Q.
+Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
+Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗ R.
+Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed.
+Lemma plainly_and_emp_elim P : emp ∧ ■ P ⊢ P.
+Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
+Lemma plainly_elim_absorbingly P : ■ P ⊢ bi_absorbingly P.
+Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed.
+Lemma plainly_elim P `{!Absorbing P} : ■ P ⊢ P.
+Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
+
+Lemma plainly_idemp_1 P : ■ ■ P ⊢ ■ P.
+Proof. by rewrite plainly_elim_absorbingly absorbingly_plainly. Qed.
+Lemma plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
+Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
+
+Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
+Proof. intros <-. apply plainly_idemp_2. Qed.
+
+Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢ bi_pure (PROP:=PROP) φ.
+Proof.
+  apply (anti_symm _); auto.
+  - by rewrite plainly_elim_persistently persistently_pure.
+  - apply pure_elim'=> Hφ.
+    trans (∀ x : False, ■ True : PROP)%I; [by apply forall_intro|].
+    rewrite plainly_forall_2. by rewrite -(pure_intro _ φ).
+Qed.
+Lemma plainly_forall {A} (Ψ : A → PROP) : ■ (∀ a, Ψ a) ⊣⊢ ∀ a, ■ (Ψ a).
+Proof.
+  apply (anti_symm _); auto using plainly_forall_2.
+  apply forall_intro=> x. by rewrite (forall_elim x).
+Qed.
+Lemma plainly_exist_2 {A} (Ψ : A → PROP) : (∃ a, ■ (Ψ a)) ⊢ ■ (∃ a, Ψ a).
+Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed.
+Lemma plainly_exist `{!BiPlainlyExist PROP} {A} (Ψ : A → PROP) :
+  ■ (∃ a, Ψ a) ⊣⊢ ∃ a, ■ (Ψ a).
+Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed.
+Lemma plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
+Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
+Lemma plainly_or_2 P Q : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q).
+Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed.
+Lemma plainly_or `{!BiPlainlyExist PROP} P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
+Lemma plainly_impl P Q : ■ (P → Q) ⊢ ■ P → ■ Q.
+Proof.
+  apply impl_intro_l; rewrite -plainly_and.
+  apply plainly_mono, impl_elim with P; auto.
+Qed.
+
+Lemma plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ P.
+Proof.
+  apply (anti_symm _).
+  - rewrite -{1}(idemp bi_and (â–  _)%I).
+    by rewrite -{2}(left_id emp%I _ (â–  _)%I) plainly_and_sep_assoc and_elim_l.
+  - by rewrite plainly_absorb.
+Qed.
+
+Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
+Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qed.
+Lemma plainly_and_sep_r_1 P Q : P ∧ ■ Q ⊢ P ∗ ■ Q.
+Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
+
+Lemma plainly_True_emp : ■ True ⊣⊢ ■ (@bi_emp PROP).
+Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
+Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊢ ■ (P ∗ Q).
+Proof.
+  rewrite plainly_and.
+  rewrite -{1}plainly_idemp -plainly_and -{1}(left_id emp%I _ Q%I).
+  by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
+Qed.
+
+Lemma plainly_affinely P : ■ (bi_affinely P) ⊣⊢ ■ P.
+Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
+
+Lemma and_sep_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
+Proof.
+  apply (anti_symm _); auto using plainly_and_sep_l_1.
+  apply and_intro.
+  - by rewrite plainly_absorb.
+  - by rewrite comm plainly_absorb.
+Qed.
+Lemma plainly_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
+Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
+Lemma plainly_sep `{BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Proof.
+  apply (anti_symm _); auto using plainly_sep_2.
+  rewrite -(plainly_affinely (_ ∗ _)%I) affinely_sep -and_sep_plainly. apply and_intro.
+  - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
+  - by rewrite (affinely_elim_emp P) left_id affinely_elim.
+Qed.
+
+Lemma plainly_wand P Q : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q.
+Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed.
+
+Lemma plainly_entails_l P Q : (P ⊢ ■ Q) → P ⊢ ■ Q ∗ P.
+Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed.
+Lemma plainly_entails_r P Q : (P ⊢ ■ Q) → P ⊢ P ∗ ■ Q.
+Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.
+
+Lemma plainly_impl_wand_2 P Q : ■ (P -∗ Q) ⊢ ■ (P → Q).
+Proof.
+  apply plainly_intro', impl_intro_r.
+  rewrite -{2}(left_id emp%I _ P%I) plainly_and_sep_assoc.
+  by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
+Qed.
+
+Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
+Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
+
+Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (bi_affinely (■ P) -∗ Q).
+Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed.
+
+Section plainly_affine_bi.
+  Context `{BiAffine PROP}.
+
+  Lemma plainly_emp : ■ emp ⊣⊢ bi_emp (PROP:=PROP).
+  Proof. by rewrite -!True_emp plainly_pure. Qed.
+
+  Lemma plainly_and_sep_l P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
+  Proof.
+    apply (anti_symm (⊢));
+      eauto using plainly_and_sep_l_1, sep_and with typeclass_instances.
+  Qed.
+  Lemma plainly_and_sep_r P Q : P ∧ ■ Q ⊣⊢ P ∗ ■ Q.
+  Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed.
+
+  Lemma plainly_impl_wand P Q : ■ (P → Q) ⊣⊢ ■ (P -∗ Q).
+  Proof.
+    apply (anti_symm (⊢)); auto using plainly_impl_wand_2.
+    apply plainly_intro', wand_intro_l.
+    by rewrite -plainly_and_sep_r plainly_elim impl_elim_r.
+  Qed.
+
+  Lemma impl_wand_plainly P Q : (■ P → Q) ⊣⊢ (■ P -∗ Q).
+  Proof.
+    apply (anti_symm (⊢)). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2.
+  Qed. 
+End plainly_affine_bi.
+
+(* Conditional plainly *)
+Global Instance plainly_if_ne p : NonExpansive (@plainly_if PROP _ p).
+Proof. solve_proper. Qed.
+Global Instance plainly_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@plainly_if PROP _ p).
+Proof. solve_proper. Qed.
+Global Instance plainly_if_mono' p : Proper ((⊢) ==> (⊢)) (@plainly_if PROP _ p).
+Proof. solve_proper. Qed.
+Global Instance plainly_if_flip_mono' p :
+  Proper (flip (⊢) ==> flip (⊢)) (@plainly_if PROP _ p).
+Proof. solve_proper. Qed.
+
+Lemma plainly_if_mono p P Q : (P ⊢ Q) → ■?p P ⊢ ■?p Q.
+Proof. by intros ->. Qed.
+
+Lemma plainly_if_pure p φ : ■?p ⌜φ⌝ ⊣⊢ bi_pure (PROP:=PROP) φ.
+Proof. destruct p; simpl; auto using plainly_pure. Qed.
+Lemma plainly_if_and p P Q : ■?p (P ∧ Q) ⊣⊢ ■?p P ∧ ■?p Q.
+Proof. destruct p; simpl; auto using plainly_and. Qed.
+Lemma plainly_if_or_2 p P Q : ■?p P ∨ ■?p Q ⊢ ■?p (P ∨ Q).
+Proof. destruct p; simpl; auto using plainly_or_2. Qed.
+Lemma plainly_if_or `{!BiPlainlyExist PROP} p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
+Proof. destruct p; simpl; auto using plainly_or. Qed.
+Lemma plainly_if_exist_2 {A} p (Ψ : A → PROP) : (∃ a, ■?p (Ψ a)) ⊢ ■?p (∃ a, Ψ a).
+Proof. destruct p; simpl; auto using plainly_exist_2. Qed.
+Lemma plainly_if_exist `{!BiPlainlyExist PROP} {A} p (Ψ : A → PROP) :
+  ■?p (∃ a, Ψ a) ⊣⊢ ∃ a, ■?p (Ψ a).
+Proof. destruct p; simpl; auto using plainly_exist. Qed.
+Lemma plainly_if_sep_2 `{!BiPositive PROP} p P Q : ■?p P ∗ ■?p Q  ⊢ ■?p (P ∗ Q).
+Proof. destruct p; simpl; auto using plainly_sep_2. Qed.
+
+Lemma plainly_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
+Proof. destruct p; simpl; auto using plainly_idemp. Qed.
+
+(* Properties of plain propositions *)
+Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain PROP _).
+Proof. solve_proper. Qed.
+
+Lemma plain_plainly_2 P `{!Plain P} : P ⊢ ■ P.
+Proof. done. Qed.
+Lemma plain_plainly P `{!Plain P, !Absorbing P} : ■ P ⊣⊢ P.
+Proof. apply (anti_symm _), plain_plainly_2, _. by apply plainly_elim. Qed.
+Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■ Q.
+Proof. by intros <-. Qed.
+
+(* Typeclass instances *)
+Global Instance plainly_absorbing P : Absorbing (â–  P).
+Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorb. Qed.
+Global Instance plainly_if_absorbing P p :
+  Absorbing P → Absorbing (plainly_if p P).
+Proof. intros; destruct p; simpl; apply _. Qed.
+
+(* Not an instance, see the bottom of this file *)
+Lemma plain_persistent P : Plain P → Persistent P.
+Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
+
+(* Not an instance, see the bottom of this file *)
+Lemma impl_persistent P Q :
+  Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
+Proof.
+  intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
+                     -(persistent Q) (plainly_elim_absorbingly P) absorbing.
+Qed.
+
+Global Instance plainly_persistent P : Persistent (â–  P).
+Proof. by rewrite /Persistent persistently_plainly. Qed.
+
+Global Instance wand_persistent P Q :
+  Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
+Proof.
+  intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (■ P → Q)%I).
+  - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
+    by rewrite affinely_plainly_elim.
+  - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
+Qed.
+
+(* Instances for big operators *)
+Global Instance plainly_and_homomorphism :
+  MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _).
+Proof.
+  split; [split|]; try apply _. apply plainly_and. apply plainly_pure.
+Qed.
+
+Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
+  MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _).
+Proof.
+  split; [split|]; try apply _. apply plainly_or. apply plainly_pure.
+Qed.
+
+Global Instance plainly_sep_weak_homomorphism `{!BiPositive PROP, !BiAffine PROP} :
+  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
+Proof. split; try apply _. apply plainly_sep. Qed.
+
+Global Instance plainly_sep_homomorphism `{BiAffine PROP} :
+  MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _).
+Proof. split. apply _. apply plainly_emp. Qed.
+
+Global Instance plainly_sep_entails_weak_homomorphism :
+  WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
+Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed.
+
+Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} :
+  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _).
+Proof. split. apply _. simpl. rewrite plainly_emp. done. Qed.
+
+Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) :
+  NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
+Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
+
+(* Plainness instances *)
+Global Instance pure_plain φ : Plain (⌜φ⌝%I : PROP).
+Proof. by rewrite /Plain plainly_pure. Qed.
+Global Instance emp_plain : Plain (PROP:=PROP) emp.
+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_2 -!plain. Qed.
+Global Instance forall_plain {A} (Ψ : A → PROP) :
+  (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
+Proof.
+  intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain.
+Qed.
+Global Instance exist_plain {A} (Ψ : A → PROP) :
+  (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
+Proof.
+  intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
+Qed.
+
+Global Instance impl_plain P Q : Absorbing P → Plain P → Plain Q → Plain (P → Q).
+Proof.
+  intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
+                     (plainly_elim_absorbingly P) absorbing.
+Qed.
+Global Instance wand_plain P Q :
+  Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q).
+Proof.
+  intros. rewrite /Plain {2}(plain P). trans (■ (■ P → Q))%I.
+  - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q).
+    by rewrite affinely_plainly_elim.
+  - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
+Qed.
+Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q).
+Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
+
+Global Instance plainly_plain P : Plain (â–  P).
+Proof. by rewrite /Plain plainly_idemp. Qed.
+Global Instance persistently_plain P : Plain P → Plain (bi_persistently P).
+Proof.
+  rewrite /Plain=> HP. rewrite {1}HP plainly_persistently persistently_plainly //.
+Qed.
+Global Instance affinely_plain P : Plain P → Plain (bi_affinely P).
+Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance absorbingly_plain P : Plain P → Plain (bi_absorbingly P).
+Proof. rewrite /bi_absorbingly. apply _. Qed.
+Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
+  (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
+Proof. destruct mx; apply _. Qed.
+
+(* Interaction with equality *)
+Lemma plainly_internal_eq {A:ofeT} (a b : A) : plainly (A:=PROP) (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+  apply (anti_symm (⊢)).
+  { by rewrite plainly_elim. }
+  apply (internal_eq_rewrite' a b (λ  b, ■ (a ≡ b))%I); [solve_proper|done|].
+  rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
+Qed.
+
+Lemma plainly_alt P : ■ P ⊣⊢ bi_affinely P ≡ emp.
+Proof.
+  rewrite -plainly_affinely. apply (anti_symm (⊢)).
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+    + by rewrite affinely_elim_emp left_id.
+    + by rewrite left_id.
+  - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+    by rewrite -plainly_True_emp plainly_pure True_impl.
+Qed.
+
+Lemma plainly_alt_absorbing P `{!Absorbing P} : ■ P ⊣⊢ P ≡ True.
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+  - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
+    by rewrite plainly_pure True_impl.
+Qed.
+
+Lemma plainly_True_alt P : ■ (True -∗ P) ⊣⊢ P ≡ True.
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+    by rewrite wand_elim_r.
+  - rewrite internal_eq_sym (internal_eq_rewrite _ _
+      (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.
+    by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
+Qed.
+
+(* Interaction with â–· *)
+Lemma later_plainly P : ▷ ■ P ⊣⊢ ■ ▷ P.
+Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed.
+Lemma laterN_plainly n P : ▷^n ■ P ⊣⊢ ■ ▷^n P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed.
+
+Lemma later_plainly_if p P : ▷ ■?p P ⊣⊢ ■?p ▷ P.
+Proof. destruct p; simpl; auto using later_plainly. Qed.
+Lemma laterN_plainly_if n p P : ▷^n ■?p P ⊣⊢ ■?p (▷^n P).
+Proof. destruct p; simpl; auto using laterN_plainly. Qed.
+
+Lemma except_0_plainly_1 P : ◇ ■ P ⊢ ■ ◇ P.
+Proof. by rewrite /sbi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
+Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■ P ⊣⊢ ■ ◇ P.
+Proof. by rewrite /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed.
+
+Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+  Plain (a ≡ b : PROP)%I.
+Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+
+Global Instance later_plain P : Plain P → Plain (▷ P).
+Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
+Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
+Proof. induction n; apply _. Qed.
+Global Instance except_0_plain P : Plain P → Plain (◇ P).
+Proof. rewrite /sbi_except_0; apply _. Qed.
+
+Global Instance plainly_timeless P  `{!BiPlainlyExist PROP} :
+  Timeless P → Timeless (■ P).
+Proof.
+  intros. rewrite /Timeless /sbi_except_0 later_plainly_1.
+  by rewrite (timeless P) /sbi_except_0 plainly_or {1}plainly_elim.
+Qed.
+End plainly_derived.
+
+(* When declared as an actual instance, [plain_persistent] will cause
+failing proof searches to take exponential time, as Coq will try to
+apply it the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will
+only be used at the leaves of the proof search tree, i.e. when the
+premise of the hint can be derived from just the current context. *)
+Hint Immediate plain_persistent : typeclass_instances.
+
+(* Not defined using an ordinary [Instance] because the default
+[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
+search for the other premises fail. See the proof of [coreP_persistent] for an
+example where it would fail with a regular [Instance].*)
+Hint Extern 4 (Persistent (_ → _)) => eapply @impl_persistent : typeclass_instances.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index a7dbac7dac09d112d0c1ca0d4c9333f1e36ff572..821f849f65f48333ffc4b94eff2ba76ab131c1ce 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,5 +1,5 @@
 From stdpp Require Import coPset.
-From iris.bi Require Import interface derived_laws big_op.
+From iris.bi Require Import interface derived_laws big_op plainly.
 
 (* We first define operational type classes for the notations, and then later
 bundle these operational type classes with the laws. *)
@@ -57,7 +57,6 @@ Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
   bi_bupd_mixin_bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
   bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) ==∗ P;
   bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
-  bi_bupd_mixin_bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P;
 }.
 
 Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
@@ -69,10 +68,6 @@ Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
   bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
   bi_fupd_mixin_fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
-  bi_fupd_mixin_fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
-    E1 ⊆ E2 →
-    (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
-  bi_fupd_mixin_later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
 }.
 
 Class BiBUpd (PROP : bi) := {
@@ -92,6 +87,17 @@ Arguments bi_fupd_fupd : simpl never.
 Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
   bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
 
+Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
+  bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
+
+Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
+  fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
+    E1 ⊆ E2 →
+    (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
+  later_fupd_plain E (P : PROP) `{!Plain P} :
+    (▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
+}.
+
 Section bupd_laws.
   Context `{BiBUpd PROP}.
   Implicit Types P : PROP.
@@ -106,8 +112,6 @@ Section bupd_laws.
   Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed.
   Lemma bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R.
   Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed.
-  Lemma bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P.
-  Proof. eapply bi_bupd_mixin_bupd_plainly, bi_bupd_mixin. Qed.
 End bupd_laws.
 
 Section fupd_laws.
@@ -129,12 +133,6 @@ Section fupd_laws.
   Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
   Lemma fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
   Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
-  Lemma fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
-    E1 ⊆ E2 →
-    (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
-  Proof. eapply bi_fupd_mixin_fupd_plain'; eauto using bi_fupd_mixin. Qed.
-  Lemma later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
-  Proof. eapply bi_fupd_mixin_later_fupd_plain; eauto using bi_fupd_mixin. Qed.
 End fupd_laws.
 
 Section bupd_derived.
@@ -159,10 +157,6 @@ Section bupd_derived.
   Proof. by rewrite bupd_frame_r bi.wand_elim_r. Qed.
   Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q.
   Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
-  Lemma bupd_affinely_plainly `{BiAffine PROP} P : (|==> ■ P) ⊢ P.
-  Proof. by rewrite bi.affine_affinely bupd_plainly. Qed.
-  Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
-  Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
 End bupd_derived.
 
 Section bupd_derived_sbi.
@@ -174,6 +168,9 @@ Section bupd_derived_sbi.
     rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r.
     by rewrite -bupd_intro -bi.or_intro_l.
   Qed.
+
+  Lemma bupd_plain P `{BiBUpdPlainly PROP, !Plain P} : (|==> P) ⊢ P.
+  Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
 End bupd_derived_sbi.
 
 Section fupd_derived.
@@ -243,7 +240,7 @@ Section fupd_derived.
     intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
   Qed.
 
-  Lemma fupd_plain E1 E2 P Q `{!Plain P} :
+  Lemma fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P Q `{!Plain P} :
     E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
   Proof.
     intros HE. rewrite -(fupd_plain' _ _ E1) //. apply bi.wand_intro_l.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 7527d0f7a67bdaadb63d84f987373d12a15616d6..f1fe442394ac9951801c8d78800f44177b3e655c 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -39,24 +39,6 @@ Global Instance from_assumption_absorbingly_r p P Q :
   FromAssumption p P Q → FromAssumption p P (bi_absorbingly Q).
 Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
 
-Global Instance from_assumption_affinely_plainly_l p P Q :
-  FromAssumption true P Q → FromAssumption p (■ P) Q.
-Proof.
-  rewrite /FromAssumption /= =><-.
-  by rewrite affinely_persistently_if_elim plainly_elim_persistently.
-Qed.
-Global Instance from_assumption_plainly_l_true P Q :
-  FromAssumption true P Q → FromAssumption true (bi_plainly P) Q.
-Proof.
-  rewrite /FromAssumption /= =><-.
-  by rewrite persistently_elim plainly_elim_persistently.
-Qed.
-Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
-  FromAssumption true P Q → FromAssumption false (bi_plainly P) Q.
-Proof.
-  rewrite /FromAssumption /= =><-.
-  by rewrite affine_affinely plainly_elim_persistently.
-Qed.
 Global Instance from_assumption_affinely_persistently_l p P Q :
   FromAssumption true P Q → FromAssumption p (□ P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
@@ -112,8 +94,6 @@ Global Instance into_pure_affinely P φ :
 Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
 Global Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (bi_absorbingly P) φ.
 Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
-Global Instance into_pure_plainly P φ : IntoPure P φ → IntoPure (bi_plainly P) φ.
-Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
 Global Instance into_pure_persistently P φ :
   IntoPure P φ → IntoPure (bi_persistently P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
@@ -173,9 +153,6 @@ Proof.
   by rewrite bi.affinely_if_elim pure_wand_forall pure_impl pure_impl_forall.
 Qed.
 
-Global Instance from_pure_plainly P φ :
-  FromPure false P φ → FromPure false (bi_plainly P) φ.
-Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
 Global Instance from_pure_persistently P a φ :
   FromPure true P φ → FromPure a (bi_persistently P) φ.
 Proof.
@@ -232,16 +209,6 @@ Global Instance from_modal_affinely_persistently_affine_bi P :
   BiAffine PROP → FromModal modality_persistently (□ P) (□ P) P | 0.
 Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
 
-Global Instance from_modal_plainly P :
-  FromModal modality_plainly (bi_plainly P) (bi_plainly P) P | 2.
-Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_affinely_plainly P :
-  FromModal modality_affinely_plainly (â–  P) (â–  P) P | 1.
-Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_affinely_plainly_affine_bi P :
-  BiAffine PROP → FromModal modality_plainly (■ P) (■ P) P | 0.
-Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
-
 Global Instance from_modal_absorbingly P :
   FromModal modality_id (bi_absorbingly P) (bi_absorbingly P) P.
 Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
@@ -271,16 +238,6 @@ Global Instance from_modal_affinely_persistently_embed `{BiEmbed PROP PROP'} `(s
 Proof.
   rewrite /FromModal /= =><-. by rewrite embed_affinely embed_persistently.
 Qed.
-Global Instance from_modal_plainly_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
-  FromModal modality_plainly sel P Q →
-  FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
-Global Instance from_modal_affinely_plainly_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
-  FromModal modality_affinely_plainly sel P Q →
-  FromModal modality_affinely_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof.
-  rewrite /FromModal /= =><-. by rewrite embed_affinely embed_plainly.
-Qed.
 
 (* IntoWand *)
 Global Instance into_wand_wand p q P Q P' :
@@ -344,16 +301,6 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
   IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
 
-Global Instance into_wand_affinely_plainly p q R P Q :
-  IntoWand p q R P Q → IntoWand p q (■ R) P Q.
-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 `{!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.
-
 Global Instance into_wand_affinely_persistently p q R P Q :
   IntoWand p q R P Q → IntoWand p q (□ R) P Q.
 Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
@@ -406,15 +353,6 @@ Qed.
 Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /FromAnd pure_and. Qed.
 
-Global Instance from_and_plainly P Q1 Q2 :
-  FromAnd P Q1 Q2 →
-  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
-Global Instance from_and_plainly_sep P Q1 Q2 :
-  FromSep P Q1 Q2 →
-  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2) | 11.
-Proof. rewrite /FromAnd=> <-. by rewrite -plainly_and plainly_and_sep. Qed.
-
 Global Instance from_and_persistently P Q1 Q2 :
   FromAnd P Q1 Q2 →
   FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -455,10 +393,6 @@ Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
 Global Instance from_sep_absorbingly P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
 Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
-Global Instance from_sep_plainly P Q1 Q2 :
-  FromSep P Q1 Q2 →
-  FromSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
-Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
 Global Instance from_sep_persistently P Q1 Q2 :
   FromSep P Q1 Q2 →
   FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -511,16 +445,6 @@ Proof.
   - by rewrite -affinely_and !persistently_affinely.
   - intros ->. by rewrite affinely_and.
 Qed.
-Global Instance into_and_plainly p P Q1 Q2 :
-  IntoAnd p P Q1 Q2 →
-  IntoAnd p (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
-Proof.
-  rewrite /IntoAnd /=. destruct p; simpl.
-  - rewrite -plainly_and persistently_plainly -plainly_persistently
-            -plainly_affinely => ->.
-    by rewrite plainly_affinely plainly_persistently persistently_plainly.
-  - intros ->. by rewrite plainly_and.
-Qed.
 Global Instance into_and_persistently p P Q1 Q2 :
   IntoAnd p P Q1 Q2 →
   IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -581,17 +505,6 @@ Global Instance into_sep_affinely_trim 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 `{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_plainly_affine P Q1 Q2 :
-  IntoSep P Q1 Q2 →
-  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
-  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
-Proof.
-  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
-Qed.
-
 Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 →
   IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -638,9 +551,6 @@ Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
 Global Instance from_or_absorbingly P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly 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_2. Qed.
 Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -660,9 +570,6 @@ 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 `{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 :
   IntoOr P Q1 Q2 →
   IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -683,9 +590,6 @@ Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.
 Global Instance from_exist_absorbingly {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
 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_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.
@@ -718,9 +622,6 @@ 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 `{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) :
   IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
@@ -734,9 +635,6 @@ Proof. by rewrite /IntoForall. Qed.
 Global Instance into_forall_affinely {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
-Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
-  IntoForall P Φ → IntoForall (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
-Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
@@ -774,9 +672,6 @@ Global Instance from_forall_affinely `{BiAffine PROP} {A} P (Φ : A → PROP) :
 Proof.
   rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
 Qed.
-Global Instance from_forall_plainly {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (bi_plainly P)%I (λ a, bi_plainly (Φ a))%I.
-Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
@@ -1110,6 +1005,19 @@ Global Instance from_assumption_fupd `{BiBUpdFUpd PROP} E p P Q :
   FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
 
+Global Instance from_assumption_plainly_l_true `{BiPlainly PROP} P Q :
+  FromAssumption true P Q → FromAssumption true (■ P) Q.
+Proof.
+  rewrite /FromAssumption /= =><-.
+  by rewrite persistently_elim plainly_elim_persistently.
+Qed.
+Global Instance from_assumption_plainly_l_false `{BiPlainly PROP, BiAffine PROP} P Q :
+  FromAssumption true P Q → FromAssumption false (■ P) Q.
+Proof.
+  rewrite /FromAssumption /= =><-.
+  by rewrite affine_affinely plainly_elim_persistently.
+Qed.
+
 (* FromPure *)
 Global Instance from_pure_internal_eq af {A : ofeT} (a b : A) :
   @FromPure PROP af (a ≡ b) (a ≡ b).
@@ -1128,11 +1036,19 @@ Global Instance from_pure_fupd `{BiFUpd PROP} a E P φ :
   FromPure a P φ → FromPure a (|={E}=> P) φ.
 Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
 
+Global Instance from_pure_plainly `{BiPlainly PROP} P φ :
+  FromPure false P φ → FromPure false (■ P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
+
 (* IntoPure *)
 Global Instance into_pure_eq {A : ofeT} (a b : A) :
   Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
 Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
 
+Global Instance into_pure_plainly `{BiPlainly PROP} P φ :
+  IntoPure P φ → IntoPure (■ P) φ.
+Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
+
 (* IntoWand *)
 Global Instance into_wand_later p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
@@ -1200,6 +1116,13 @@ Proof.
   apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
 Qed.
 
+Global Instance into_wand_plainly_true `{BiPlainly PROP} q R P Q :
+  IntoWand true q R P Q → IntoWand true q (■ R) P Q.
+Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
+Global Instance into_wand_plainly_false `{BiPlainly PROP, !BiAffine PROP} q R P Q :
+  IntoWand false q R P Q → IntoWand false q (■ R) P Q.
+Proof. by rewrite /IntoWand plainly_elim. Qed.
+
 (* FromAnd *)
 Global Instance from_and_later P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
@@ -1211,6 +1134,10 @@ Global Instance from_and_except_0 P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromAnd=><-. by rewrite except_0_and. Qed.
 
+Global Instance from_and_plainly `{BiPlainly PROP} P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
+
 (* FromSep *)
 Global Instance from_sep_later P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
@@ -1229,6 +1156,10 @@ Global Instance from_sep_fupd `{BiFUpd PROP} E P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
 Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
 
+Global Instance from_sep_plainly `{BiPlainly PROP} P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
+
 (* IntoAnd *)
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -1252,6 +1183,16 @@ Proof.
              affinely_persistently_if_elim except_0_and.
 Qed.
 
+Global Instance into_and_plainly `{BiPlainly PROP} p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p (■ P) (■ Q1) (■ Q2).
+Proof.
+  rewrite /IntoAnd /=. destruct p; simpl.
+  - rewrite -plainly_and persistently_plainly -plainly_persistently
+            -plainly_affinely => ->.
+    by rewrite plainly_affinely plainly_persistently persistently_plainly.
+  - intros ->. by rewrite plainly_and.
+Qed.
+
 (* IntoSep *)
 Global Instance into_sep_later P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (▷ P) (▷ Q1) (▷ Q2).
@@ -1275,6 +1216,18 @@ Proof.
   by rewrite -(False_elim Q1) -(False_elim Q2).
 Qed.
 
+Global Instance into_sep_plainly `{BiPlainly PROP, BiPositive PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
+
+Global Instance into_sep_plainly_affine `{BiPlainly PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 →
+  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
+  IntoSep (â–  P) (â–  Q1) (â–  Q2).
+Proof.
+  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
+Qed.
+
 (* FromOr *)
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
@@ -1299,6 +1252,10 @@ Proof.
                          [apply bi.or_intro_l|apply bi.or_intro_r].
 Qed.
 
+Global Instance from_or_plainly `{BiPlainly PROP} P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
+
 (* IntoOr *)
 Global Instance into_or_later P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
@@ -1310,6 +1267,10 @@ Global Instance into_or_except_0 P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite except_0_or. Qed.
 
+Global Instance into_or_plainly `{BiPlainly PROP, BiPlainlyExist PROP} P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
+
 (* FromExist *)
 Global Instance from_exist_later {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -1336,6 +1297,10 @@ Proof.
   rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
 
+Global Instance from_exist_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
+  FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
+
 (* IntoExist *)
 Global Instance into_exist_later {A} P (Φ : A → PROP) :
   IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -1347,6 +1312,10 @@ Global Instance into_exist_except_0 {A} P (Φ : A → PROP) :
   IntoExist P Φ → Inhabited A → IntoExist (◇ P) (λ a, ◇ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 
+Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A → PROP) :
+  IntoExist P Φ → IntoExist (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
+
 (* IntoForall *)
 Global Instance into_forall_later {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
@@ -1368,6 +1337,10 @@ Proof.
   by rewrite -(pure_intro True%I) // /bi_affinely right_id emp_wand.
 Qed.
 
+Global Instance into_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
+
 (* FromForall *)
 Global Instance from_forall_later {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I.
@@ -1376,6 +1349,10 @@ Global Instance from_forall_except_0 {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
 
+Global Instance from_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
+  FromForall P Φ → FromForall (■ P)%I (λ a, ■ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
+
 (* IsExcept0 *)
 Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
@@ -1415,6 +1392,16 @@ Global Instance from_modal_later_embed `{SbiEmbed PROP PROP'} `(sel : A) n P Q :
   FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
 Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
 
+Global Instance from_modal_plainly `{BiPlainly PROP} P :
+  FromModal modality_plainly (â–  P) (â–  P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance from_modal_plainly_embed
+    `{BiPlainly PROP, BiPlainly PROP', SbiEmbed PROP PROP'} `(sel : A) P Q :
+  FromModal modality_plainly sel P Q →
+  FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
+
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
   @IntoInternalEq PROP A (x ≡ y) x y.
@@ -1425,8 +1412,8 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
 Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (bi_absorbingly P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (bi_plainly P) x y.
+Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (■ P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
 Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
@@ -1450,8 +1437,8 @@ 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 `{BiPlainlyExist PROP} P Q :
-  IntoExcept0 P Q → IntoExcept0 (bi_plainly P) (bi_plainly Q).
+Global Instance into_except_0_plainly `{BiPlainly PROP, BiPlainlyExist PROP} P Q :
+  IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
 Global Instance into_except_0_persistently P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q).
@@ -1470,10 +1457,10 @@ Qed.
 Global Instance elim_modal_bupd `{BiBUpd PROP} P Q :
   ElimModal True (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-Global Instance elim_modal_bupd_plain_goal `{BiBUpd PROP} P Q :
+Global Instance elim_modal_bupd_plain_goal `{BiBUpdPlainly PROP} P Q :
   Plain Q → ElimModal True (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
-Global Instance elim_modal_bupd_plain `{BiBUpd PROP} P Q :
+Global Instance elim_modal_bupd_plain `{BiBUpdPlainly PROP} P Q :
   Plain P → ElimModal True (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} E1 E2 P Q :
@@ -1629,8 +1616,8 @@ Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2.
 Global Instance into_later_absorbingly n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
-Global Instance into_later_plainly n P Q :
-  IntoLaterN false n P Q → IntoLaterN false n (bi_plainly P) (bi_plainly Q).
+Global Instance into_later_plainly `{BiPlainly PROP} n P Q :
+  IntoLaterN false n P Q → IntoLaterN false n (■ P) (■ Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (bi_persistently P) (bi_persistently Q).
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 5786a01a7b83abacdeef05ec58eeaab2234ac439..119c45711e554f1c0e2e7b6004be20f0a00c0b2c 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -215,7 +215,8 @@ Hint Mode IntoForall + - ! - : typeclass_instances.
 
 Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
   from_forall : (∀ x, Φ x) ⊢ P.
-Arguments from_forall {_ _} _ _ {_}.
+Arguments FromForall {_ _} _%I _%I : simpl never.
+Arguments from_forall {_ _} _%I _%I {_}.
 Hint Mode FromForall + - ! - : typeclass_instances.
 
 Class IsExcept0 {PROP : sbi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index 197be17f0a52b575ac9c3738e4b83b27ea68db31..af0e205e4b230eeb9e69a8946510fbad729997a3 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -34,26 +34,6 @@ Section bi_modalities.
   Definition modality_affinely_persistently :=
     Modality _ modality_affinely_persistently_mixin.
 
-  Lemma modality_plainly_mixin :
-    modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
-  Proof.
-    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
-      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
-  Qed.
-  Definition modality_plainly :=
-    Modality _ modality_plainly_mixin.
-
-  Lemma modality_affinely_plainly_mixin :
-    modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
-  Proof.
-    split; simpl; split_and?; eauto using equiv_entails_sym,
-      affinely_plainly_emp, affinely_intro,
-      plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
-      affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
-  Qed.
-  Definition modality_affinely_plainly :=
-    Modality _ modality_affinely_plainly_mixin.
-
   Lemma modality_embed_mixin `{BiEmbed PROP PROP'} :
     modality_mixin (@embed PROP PROP' _)
       (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
@@ -71,6 +51,15 @@ End bi_modalities.
 Section sbi_modalities.
   Context {PROP : sbi}.
 
+  Lemma modality_plainly_mixin `{BiPlainly PROP} :
+    modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
+  Proof.
+    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
+      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
+  Qed.
+  Definition modality_plainly `{BiPlainly PROP} :=
+    Modality _ modality_plainly_mixin.
+
   Lemma modality_laterN_mixin n :
     modality_mixin (@sbi_laterN PROP n)
       (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index ecd669fd329ee71805af21da5b2d2f89f60f4601..179150e9073598be1418444aaa7af2dade29ead7 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -1,4 +1,5 @@
 From iris.bi Require Export monpred.
+From iris.bi Require Import plainly.
 From iris.proofmode Require Import tactics class_instances.
 
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
@@ -33,6 +34,7 @@ End modalities.
 
 Section bi.
 Context {I : biIndex} {PROP : bi}.
+Local Notation monPredI := (monPredI I PROP).
 Local Notation monPred := (monPred I PROP).
 Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP).
 Implicit Types P Q R : monPred.
@@ -290,21 +292,6 @@ Proof.
   by rewrite monPred_at_exist.
 Qed.
 
-Global Instance foram_forall_monPred_at_plainly i P Φ :
-  (∀ i, MakeMonPredAt i P (Φ i)) →
-  FromForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
-Proof.
-  rewrite /FromForall /MakeMonPredAt=>H. rewrite monPred_at_plainly.
-  by setoid_rewrite H.
-Qed.
-Global Instance into_forall_monPred_at_plainly i P Φ :
-  (∀ i, MakeMonPredAt i P (Φ i)) →
-  IntoForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
-Proof.
-  rewrite /IntoForall /MakeMonPredAt=>H. rewrite monPred_at_plainly.
-  by setoid_rewrite H.
-Qed.
-
 Global Instance from_forall_monPred_at_absolutely P (Φ : I → PROP) i :
   (∀ i, MakeMonPredAt i P (Φ i)) → FromForall ((∀ᵢ P) i)%I Φ.
 Proof.
@@ -423,6 +410,21 @@ Implicit Types 𝓟 𝓠 𝓡 : PROP.
 Implicit Types φ : Prop.
 Implicit Types i j : I.
 
+Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
+  (∀ i, MakeMonPredAt i P (Φ i)) →
+  FromForall ((■ P) i) (λ j, ■ (Φ j))%I.
+Proof.
+  rewrite /FromForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
+  by setoid_rewrite HPΦ.
+Qed.
+Global Instance into_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
+  (∀ i, MakeMonPredAt i P (Φ i)) →
+  IntoForall ((■ P) i) (λ j, ■ (Φ j))%I.
+Proof.
+  rewrite /IntoForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
+  by setoid_rewrite HPΦ.
+Qed.
+
 Global Instance is_except_0_monPred_at i P :
   IsExcept0 P → IsExcept0 (P i).
 Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 29d90f3df3d5035436c118a77aee63dad266115e..b4bdc052d8e83a9dbf6c8afe9e1fa56bbe489e21 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1963,7 +1963,7 @@ Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros.
 Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit.
 Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit.
 Hint Extern 1 (envs_entails _ (â–· _)) => iNext.
-Hint Extern 1 (envs_entails _ (bi_plainly _)) => iAlways.
+Hint Extern 1 (envs_entails _ (â–  _)) => iAlways.
 Hint Extern 1 (envs_entails _ (bi_persistently _)) => iAlways.
 Hint Extern 1 (envs_entails _ (bi_affinely _)) => iAlways.
 Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.