diff --git a/ProofMode.md b/ProofMode.md
index 2eaab453a1c2a5c648f7c07723e9de89ebbb18f4..8bc2bf2dd40fb5bd8a2b0c83e90e1fafd814ab24 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -31,7 +31,7 @@ Context management
 - `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the selection
   pattern `selpat` into wands, and the Coq level hypotheses/variables
   `x1 ... xn` into universal quantifiers. Persistent hypotheses are wrapped into
-  the always modality.
+  the persistence modality.
 - `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
 - `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
   implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
@@ -162,8 +162,8 @@ Miscellaneous
   introduces pure connectives.
 - The proof mode adds hints to the core `eauto` database so that `eauto`
   automatically introduces: conjunctions and disjunctions, universal and
-  existential quantifiers, implications and wand, always, later and update
-  modalities, and pure connectives.
+  existential quantifiers, implications and wand, plainness, persistence, later
+  and update modalities, and pure connectives.
 
 Selection patterns
 ==================
@@ -207,7 +207,9 @@ appear at the top level:
   Items of the selection pattern can be prefixed with `$`, which cause them to
   be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an always modality and clear the spatial context.
+- `!#` : introduce an persistence or plainness modality and clear the spatial
+  context. In case of a plainness modality, it will prune all persistent
+  hypotheses that are not plain.
 - `!>` : introduce a modality.
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 86ec1a0464158da40033db47eed1bbfe7a24e001..d6139bd888c868e6310b0bf30807203b15048a0c 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -36,6 +36,9 @@ Global Instance uPred_affine : AffineBI (uPredI M) | 0.
 Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
 
 (* Own and valid derived *)
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
+  ✓ a ⊢ bi_persistently (✓ a : uPred M).
+Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
 Lemma affinely_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
   rewrite affine_affinely=>?; apply (anti_symm _); [by rewrite persistently_elim|].
@@ -47,6 +50,11 @@ 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_empty. 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 affinely_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
   rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
@@ -90,12 +98,24 @@ Proof.
     auto using and_elim_l, and_elim_r.
 Qed.
 
-(* Derived lemmas for persistence *)
-Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
-  NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
+(* Plainness *)
+Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
+  NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
+Global Instance cmra_valid_plain {A : cmraT} (a : A) :
+  Plain (✓ a : uPred M)%I.
+Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
+
+Lemma bupd_affinely_plainly P : (|==> ■ P) ⊢ P.
+Proof. by rewrite affine_affinely bupd_plainly. Qed.
+
+Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
+Proof. by rewrite -{1}(plain_plainly P) bupd_plainly. Qed.
 
 (* Persistence *)
+Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
+  NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
+Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index e6d584217ca120eb903dcc557cd024f17b7b7f14..8bd7b3c3eb3474c51205c29d49f8b0a14c30e3a0 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -3,19 +3,9 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-(** The "core" of an assertion is its maximal persistent part.
-    It can be defined entirely within the logic... at least
-    in the shallow embedding.
-    WARNING: The function "coreP" is NOT NON-EXPANSIVE.
-    This is because the turnstile is not non-expansive as a function
-    from iProp to (discreteC Prop).
-    To obtain a core that's non-expansive, we would have to add another
-    modality to the logic: a box that removes access to *all* resources,
-    not just restricts access to the core.
-*)
-
+(** The "core" of an assertion is its maximal persistent part. *)
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ `(!Persistent Q), ⌜P ⊢ Q⌝ → Q)%I.
+  (∀ Q, ■ (Q → □ Q) → ■ (P → Q) → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -24,25 +14,31 @@ Section core.
   Implicit Types P Q : uPred M.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
+  Proof. rewrite /coreP. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
 
   Global Instance coreP_persistent P : Persistent (coreP P).
-  Proof. rewrite /coreP. apply _. Qed.
-
-  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
   Proof.
-    rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??).
-    iApply ("H" $! Q with "[%]"). by etrans.
+    rewrite /coreP /Persistent. iIntros "HC" (Q). rewrite !affine_affinely.
+    iApply persistently_impl_plainly. iIntros "#HQ".
+    iApply persistently_impl_plainly. iIntros "#HPQ".
+    iApply "HQ". by iApply "HC"; rewrite !affine_affinely.
   Qed.
 
+  Global Instance coreP_ne : NonExpansive (@coreP M).
+  Proof. solve_proper. Qed.
   Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
-  Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
+  Proof. solve_proper. Qed.
+
+  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
+  Proof.
+    rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q) "#HQ #HPQ".
+    iApply ("H" $! Q with "[]"); first done. by rewrite HP.
+  Qed.
 
   Lemma coreP_elim P : Persistent P → coreP P -∗ P.
-  Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
+  Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
 
-  Lemma coreP_wand P Q :
-    (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
+  Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
   Proof.
     split.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index 3e0f907a3f01877663b0511198841c7f559fc173..0347eeaa9af97aaf970b44d1fe9763d6d5d53249 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -115,6 +115,12 @@ Proof. apply bupd_intro. Qed.
 Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 
+Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
+
+Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+
 Global Instance is_except_0_bupd P : IsExcept0 P → IsExcept0 (|==> P).
 Proof.
   rewrite /IsExcept0=> HP.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index e4d3b97b13cb87c62c6bdcd5d14556aa86764faf..9928e985505566a7c02f4a0c764611d5eace5152 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -6,22 +6,16 @@ Section adequacy.
 Context {M : ucmraT}.
 
 (** Consistency and adequancy statements *)
-Lemma soundness φ n :
-  bi_valid (PROP:=uPredI M) (Nat.iter n (λ P, |==> ▷ P) (⌜ φ ⌝))%I → φ.
+Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
 Proof.
-  cut (∀ x, ✓{n} x → Nat.iter n (λ P, |==> ▷ P)%I (@uPred_pure M φ) n x → φ).
-  { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
-    eapply H; first by eauto using ucmra_unit_validN.
-    rewrite /bi_emp /= /uPred_emp. by unseal. }
-  unseal. induction n as [|n IH]=> x Hx Hupd; auto.
-  destruct (Hupd (S n) ε) as (x'&?&?); rewrite ?right_id; auto.
-  eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
+  cut ((▷^n ⌜ φ ⌝ : uPred M)%I n ε → φ).
+  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
+  rewrite /bi_laterN; unseal. induction n as [|n IH]=> H; auto.
 Qed.
 
-Corollary consistency_modal n :
-  ¬bi_valid (PROP:=uPredI M) (Nat.iter n (λ P, |==> ▷ P) (False : uPred M))%I.
+Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
 Proof. exact (soundness False n). Qed.
 
-Corollary consistency : ¬bi_valid (PROP:=uPredI M) False.
+Corollary consistency : ¬(False : uPred M)%I.
 Proof. exact (consistency_modal 0). Qed.
 End adequacy.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index ecc41121ec23a7c74ea1455a2ff2811b7a5d72e3..a52cce8a6492e1355456c7b4042395c50d577805 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -248,6 +248,14 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M.
 Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
 
+Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
+  {| uPred_holds n x := P n ε |}.
+Solve Obligations with naive_solver eauto using uPred_closed, 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.
+
 Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Next Obligation.
@@ -311,24 +319,25 @@ Module uPred_unseal.
 Definition unseal_eqs :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
   uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
-  uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq,
-  uPred_bupd_eq).
+  uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
+  uPred_cmra_valid_eq, uPred_bupd_eq).
 Ltac unseal := rewrite
   /bi_emp /= /uPred_emp /bi_pure /bi_and /bi_or /bi_impl
-  /bi_forall /bi_exist /bi_internal_eq /bi_sep /bi_wand /bi_persistently
-  /bi_later /=
+  /bi_forall /bi_exist /bi_internal_eq /bi_sep /bi_wand /bi_plainly
+  /bi_persistently /bi_later /=
   /sbi_emp /sbi_pure /sbi_and /sbi_or /sbi_impl
-  /sbi_forall /sbi_exist /sbi_internal_eq /sbi_sep /sbi_wand /sbi_persistently /=
+  /sbi_forall /sbi_exist /sbi_internal_eq /sbi_sep /sbi_wand /sbi_plainly
+  /sbi_persistently /=
   !unseal_eqs /=.
 End uPred_unseal.
 Import uPred_unseal.
 
 Local Arguments uPred_holds {_} !_ _ _ /.
 
-Lemma uPred_bi_mixin (M : ucmraT) : BIMixin
+Lemma uPred_bi_mixin (M : ucmraT) : BIMixin (ofe_mixin_of (uPred M))
   uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
                 (@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
-                uPred_sep uPred_wand uPred_persistently.
+                uPred_sep uPred_wand uPred_plainly uPred_persistently.
 Proof.
   split.
   - (* PreOrder uPred_entails *)
@@ -364,6 +373,9 @@ 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.
@@ -438,16 +450,43 @@ 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 (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a) *)
+    by unseal.
+  - (* bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q *)
+    unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
+    split; eapply HPQ; eauto using @ucmra_unit_least.
+  - (* (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q) *)
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with (core x), cmra_included_includedN; auto.
+    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 ε, cmra_included_includedN; auto.
+    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.
+  - (* bi_plainly (bi_persistently P) ⊢ bi_plainly P (ADMISSIBLE) *)
+    intros P. unseal; split=> n  x ?? /=. by rewrite -(core_id_core ε).
   - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
   - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
     by unseal.
-  - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
-    intros P. unfold uPred_emp; unseal; by split=> n x ? _.
   - (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
     intros P Q. move: (uPred_persistently P)=> P'.
     unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
@@ -460,7 +499,7 @@ Qed.
 Lemma uPred_sbi_mixin (M : ucmraT) : SBIMixin
   uPred_entails uPred_pure uPred_or uPred_impl
   (@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
-  uPred_sep uPred_persistently uPred_later.
+  uPred_sep uPred_plainly uPred_persistently uPred_later.
 Proof.
   split.
   - (* Contractive bi_later *)
@@ -489,6 +528,10 @@ 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 *)
@@ -602,8 +645,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 persistently_cmra_valid_1 {A : cmraT} (a : A) :
-  ✓ a ⊢ bi_persistently (✓ a : uPred M).
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ bi_plainly (✓ 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.
@@ -646,5 +688,11 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
+Lemma bupd_plainly P : (|==> bi_plainly P) ⊢ P.
+Proof.
+  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.
 End uPred.
 End uPred.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 291994248cfd58a4d6434b9b6ffd7eacbb89418b..c4cc36c5fed0f8fc032915b64571c562a4b74e38 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -125,9 +125,13 @@ Section sep_list.
     ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x).
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
+  Lemma big_sepL_plainly `{AffineBI PROP} Φ l :
+    bi_plainly ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, bi_plainly (Φ k x).
+  Proof. apply (big_opL_commute _). Qed.
+
   Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
-    (bi_persistently ([∗ list] k↦x ∈ l, Φ k x)) ⊣⊢
-    ([∗ list] k↦x ∈ l, bi_persistently (Φ k x)).
+    bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢
+    [∗ list] k↦x ∈ l, bi_persistently (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall `{AffineBI PROP} Φ l :
@@ -159,6 +163,16 @@ 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.
@@ -264,9 +278,13 @@ 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)).
+    bi_persistently ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢
+    [∧ list] k↦x ∈ l, bi_persistently (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_andL_forall `{AffineBI PROP} Φ l :
@@ -281,6 +299,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.
@@ -395,6 +420,10 @@ Section gmap.
     ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x).
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
+  Lemma big_sepM_plainly `{AffineBI PROP} Φ m :
+    bi_plainly ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, bi_plainly (Φ k x).
+  Proof. apply (big_opM_commute _). Qed.
+
   Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
     (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
       ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
@@ -435,6 +464,12 @@ 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.
@@ -561,8 +596,12 @@ Section gset.
     ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
+  Lemma big_sepS_plainly `{AffineBI PROP} Φ X :
+    bi_plainly ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_plainly (Φ y).
+  Proof. apply (big_opS_commute _). Qed.
+
   Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
-    bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, bi_persistently (Φ y)).
+    bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall `{AffineBI PROP} Φ X :
@@ -593,6 +632,13 @@ Section gset.
       apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       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.
@@ -611,7 +657,6 @@ Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
   ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom _ m, Φ k).
 Proof. apply big_opM_dom. Qed.
 
-
 (** ** Big ops over finite multisets *)
 Section gmultiset.
   Context `{Countable A}.
@@ -669,11 +714,21 @@ Section gmultiset.
     ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
+  Lemma big_sepMS_plainly `{AffineBI PROP} Φ X :
+    bi_plainly ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, bi_plainly (Φ y).
+  Proof. apply (big_opMS_commute _). Qed.
+
   Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
     bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
-      ([∗ mset] y ∈ X, bi_persistently (Φ 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.
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 04534f3d0b5abef4c3252ec87fc84615a691875c..e9b2f14e27c53a0b43c783557fff6579342aa78b 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -13,6 +13,12 @@ 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 {_}.
@@ -25,6 +31,8 @@ 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.
@@ -47,6 +55,12 @@ Class Absorbing {PROP : bi} (P : PROP) := absorbing : ▲ 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 /.
@@ -61,6 +75,9 @@ 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
@@ -162,6 +179,8 @@ Proof.
 Qed.
 Global Instance internal_eq_proper (A : ofeT) :
   Proper ((≡) ==> (≡) ==> (⊣⊢)) (@bi_internal_eq PROP A) := ne_proper_2 _.
+Global Instance plainly_proper :
+  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_plainly PROP) := ne_proper _.
 Global Instance persistently_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently PROP) := ne_proper _.
 
@@ -938,7 +957,7 @@ Section affine_bi.
   Qed.
 End affine_bi.
 
-(* Properties of the persistently modality *)
+(* Properties of the persistence modality *)
 Hint Resolve persistently_mono.
 Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@bi_persistently PROP).
 Proof. intros P Q; apply persistently_mono. Qed.
@@ -1019,14 +1038,6 @@ Proof.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 
-Lemma persistently_internal_eq {A : ofeT} (a b : A) :
-  bi_persistently (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
-  apply (anti_symm (⊢)); first by rewrite persistently_elim.
-  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 persistently_sep_dup P :
   bi_persistently P ⊣⊢ bi_persistently P ∗ bi_persistently P.
 Proof.
@@ -1043,6 +1054,17 @@ Qed.
 Lemma persistently_and_sep_r_1 P Q : P ∧ bi_persistently Q ⊢ P ∗ bi_persistently Q.
 Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
 
+Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
+Proof. by rewrite -plainly_elim_persistently -plainly_emp_intro. Qed.
+
+Lemma persistently_internal_eq {A : ofeT} (a b : A) :
+  bi_persistently (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+  apply (anti_symm (⊢)); first by rewrite persistently_elim.
+  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 persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
 Lemma persistently_and_sep P Q : bi_persistently (P ∧ Q) ⊢ bi_persistently (P ∗ Q).
@@ -1141,6 +1163,233 @@ 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 absorbingly_plainly P : ▲ bi_plainly P ⊣⊢ bi_plainly P.
+Proof.
+  apply (anti_symm _), absorbingly_intro.
+  by rewrite /bi_absorbingly comm plainly_absorbing.
+Qed.
+Global Instance plainly_absorbing P : Absorbing (bi_plainly P).
+Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorbing. 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. Qed.
+Lemma plainly_and_sep_assoc P Q R :
+  bi_plainly P ∧ (Q ∗ R) ⊣⊢ (bi_plainly P ∧ Q) ∗ R.
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite {1}plainly_idemp_2 plainly_and_sep_elim assoc.
+    apply sep_mono_l, and_intro.
+    + by rewrite and_elim_r sep_elim_l.
+    + by rewrite and_elim_l left_id.
+  - apply and_intro.
+    + by rewrite and_elim_l sep_elim_l.
+    + by rewrite and_elim_r.
+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 ⊢ ▲ 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. 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.
+  - 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 {A} (Ψ : A → PROP) :
+  bi_plainly (∃ a, Ψ a) ⊣⊢ ∃ a, bi_plainly (Ψ a).
+Proof.
+  apply (anti_symm _); auto using plainly_exist_1.
+  apply exist_elim=> x. by rewrite (exist_intro x).
+Qed.
+Lemma plainly_and P Q : bi_plainly (P ∧ Q) ⊣⊢ bi_plainly P ∧ bi_plainly Q.
+Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
+Lemma plainly_or P Q : bi_plainly (P ∨ Q) ⊣⊢ bi_plainly P ∨ bi_plainly Q.
+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 _); last by eauto using sep_elim_l with typeclass_instances.
+  by rewrite -{1}(idemp bi_and (bi_plainly _)%I)
+         -{2}(left_id emp%I _ (bi_plainly _)%I) plainly_and_sep_assoc and_elim_l.
+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_internal_eq {A:ofeT} (a b : A) : bi_plainly (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+  apply (anti_symm (⊢)); [by rewrite plainly_elim|].
+  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_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.
+  - eauto 10 using sep_elim_l, sep_elim_r with typeclass_instances.
+Qed.
+Lemma plainly_sep_2 P Q :
+  bi_plainly P ∗ bi_plainly Q ⊢ bi_plainly (P ∗ Q).
+Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
+Lemma plainly_sep `{PositiveBI PROP} P Q :
+  bi_plainly (P ∗ Q) ⊣⊢ bi_plainly P ∗ bi_plainly Q.
+Proof.
+  apply (anti_symm _); auto using plainly_sep_2.
+  by rewrite -plainly_affinely affinely_sep sep_and !affinely_elim plainly_and
+             and_sep_plainly.
+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 persistently_plainly P : bi_persistently (bi_plainly P) ⊣⊢ bi_plainly P.
+Proof.
+  apply (anti_symm _); [by rewrite persistently_elim|].
+    by rewrite -plainly_elim_persistently plainly_idemp.
+Qed.
+Lemma plainly_persistently P : bi_plainly (bi_persistently P) ⊣⊢ bi_plainly P.
+Proof.
+  apply (anti_symm _). apply plainly_persistently_1.
+  by rewrite -plainly_elim_persistently plainly_idemp.
+Qed.
+
+Section plainly_affinely_bi.
+  Context `{AffineBI 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 wand_impl_persistently P Q : (bi_persistently P -∗ Q) ⊣⊢ (bi_persistently P → Q).
+  Proof.
+    apply (anti_symm (⊢)); [|by rewrite -impl_wand_1].
+    apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
+  Qed.
+
+  Lemma wand_impl_plainly P Q : (bi_plainly P -∗ Q) ⊣⊢ (bi_plainly P → Q).
+  Proof.
+    apply (anti_symm (⊢)); [|by rewrite -impl_wand_1].
+    apply impl_intro_l. by rewrite plainly_and_sep_l wand_elim_r.
+  Qed.
+End plainly_affinely_bi.
+
+(* 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 P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+Proof. by rewrite plainly_or affinely_or. Qed.
+Lemma affinely_plainly_exist {A} (Φ : A → PROP) : ■ (∃ x, Φ x) ⊣⊢ ∃ x, ■ Φ x.
+Proof. by rewrite plainly_exist affinely_exist. Qed.
+Lemma affinely_plainly_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
+Proof. by rewrite affinely_sep_2 plainly_sep_2. Qed.
+Lemma affinely_plainly_sep `{PositiveBI PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+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.
+  apply (anti_symm _).
+  - by rewrite /bi_affinely -(comm bi_and (bi_plainly P)%I)
+               -plainly_and_sep_assoc left_id.
+  - apply and_intro. by rewrite affinely_elim sep_elim_l. by rewrite sep_elim_r.
+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.
 
 (* The combined affinely persistently modality *)
 Lemma affinely_persistently_elim P : □ P ⊢ P.
@@ -1230,6 +1479,67 @@ Lemma affinely_if_idemp p P :
   bi_affinely_if p (bi_affinely_if p P) ⊣⊢ bi_affinely_if p P.
 Proof. destruct p; simpl; auto using affinely_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 p P Q : bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P ∨ bi_plainly_if p Q.
+Proof. destruct p; simpl; auto using plainly_or. Qed.
+Lemma plainly_if_exist {A} p (Ψ : A → PROP) : (bi_plainly_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_plainly_if p (Ψ a).
+Proof. destruct p; simpl; auto using plainly_exist. Qed.
+Lemma plainly_if_sep `{PositiveBI 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 p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
+Proof. destruct p; simpl; auto using affinely_plainly_or. Qed.
+Lemma affinely_plainly_if_exist {A} p (Ψ : A → PROP) :
+  (■?p ∃ a, Ψ a) ⊣⊢ ∃ a, ■?p Ψ a.
+Proof. destruct p; simpl; auto using affinely_plainly_exist. Qed.
+Lemma affinely_plainly_if_sep_2 p P Q : ■?p P ∗ ■?p Q ⊢ ■?p (P ∗ Q).
+Proof. destruct p; simpl; auto using affinely_plainly_sep_2. Qed.
+Lemma affinely_plainly_if_sep `{PositiveBI PROP} p P Q :
+  ■?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.
+
 (* Conditional persistently *)
 Global Instance persistently_if_ne p : NonExpansive (@bi_persistently_if PROP p).
 Proof. solve_proper. Qed.
@@ -1298,6 +1608,74 @@ 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.
 
+(* Plainness *)
+Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain PROP).
+Proof. solve_proper. Qed.
+
+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 -!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. apply exist_mono=> x. by rewrite -plain.
+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 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.
+(* TODO : can we prove this lemma under positivity of the BI (or even
+   weaker assumptions) ? *)
+Global Instance wand_plain `{AffineBI PROP} P Q :
+  Plain P → Plain Q → Plain (P -∗ Q).
+Proof.
+  intros. rewrite /Plain {2}(plain P) wand_impl_plainly -plainly_impl_plainly.
+  by rewrite -wand_impl_plainly -(plain Q) (plainly_elim P).
+Qed.
+Global Instance pure_wand_plain φ Q `{!Absorbing Q} : Plain Q → Plain (⌜φ⌝ -∗ Q).
+Proof. intros ?. rewrite pure_wand_forall. apply _. 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 (▲ 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.
+
+(* Properties of plain propositions *)
+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.
+
 (* Persistence *)
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
 Proof. solve_proper. Qed.
@@ -1329,8 +1707,20 @@ Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
   Persistent (a ≡ b : PROP)%I.
 Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 
-Global Instance pure_impl_persistent φ Q : Persistent Q → Persistent (⌜φ⌝ → Q).
-Proof. rewrite pure_impl_forall. apply _. 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.
+(* TODO : can we prove this lemma under positivity of the BI (or even
+   weaker assumptions) ? *)
+Global Instance wand_persistent `{AffineBI PROP} P Q :
+  Plain P → Persistent Q → Persistent (P -∗ Q).
+Proof.
+ intros. by rewrite /Persistent {2}(plain P) wand_impl_plainly
+   -persistently_impl_plainly -wand_impl_plainly -(persistent Q) (plainly_elim P).
+Qed.
 Global Instance pure_wand_persistent φ Q :
   Persistent Q → Absorbing Q → Persistent (⌜φ⌝ -∗ Q).
 Proof. intros. rewrite pure_wand_forall. apply _. Qed.
@@ -1339,17 +1729,22 @@ 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).
 Proof. rewrite /bi_affinely. apply _. Qed.
 Global Instance absorbingly_persistent P : Persistent P → Persistent (▲ P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-
 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.
 
+Lemma plain_persistent P : Plain P → Persistent P.
+Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
+Hint Immediate plain_persistent.
+
 (* Properties of persistent propositions *)
 Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ bi_persistently P.
 Proof. done. Qed.
@@ -1430,6 +1825,34 @@ 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 :
+  MonoidHomomorphism bi_or bi_or (≡) (@bi_plainly PROP).
+Proof.
+  split; [split|]; try apply _. apply plainly_or. apply plainly_pure.
+Qed.
+
+Global Instance bi_plainly_sep_weak_homomorphism `{PositiveBI PROP} :
+  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP).
+Proof. split; try apply _. apply plainly_sep. Qed.
+
+Global Instance bi_plainly_sep_homomorphism `{AffineBI 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.
@@ -1557,22 +1980,27 @@ 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 : ▷ ▲ P ⊣⊢ ▲ ▷ 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 {1}(persistent_persistently_2 P)
-                     later_persistently.
-Qed.
+Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed.
 Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
 Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
 
@@ -1627,18 +2055,25 @@ 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_persistently n P :
-  ▷^n bi_persistently P ⊣⊢ bi_persistently (▷^n P).
+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 ▲ P ⊣⊢ ▲ ▷^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).
@@ -1691,14 +2126,20 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
+Lemma except_0_plainly P : ◇ bi_plainly P ⊣⊢ bi_plainly (◇ P).
+Proof. by rewrite /bi_except_0 plainly_or -later_plainly plainly_pure. Qed.
 Lemma except_0_persistently P : ◇ bi_persistently P ⊣⊢ bi_persistently (◇ P).
 Proof.
   by rewrite /bi_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 P : ■ ◇ P ⊢ ◇ ■ P.
+Proof. by rewrite -except_0_plainly except_0_affinely_2. Qed.
 Lemma except_0_affinely_persistently_2 P : □ ◇ P ⊢ ◇ □ P.
 Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed.
+Lemma except_0_affinely_plainly_if_2 p P : ■?p ◇ P ⊢ ◇ ■?p P.
+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 : ◇ ▲ P ⊣⊢ ▲ ◇ P.
@@ -1770,6 +2211,11 @@ Proof.
   - rewrite /bi_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
+Global Instance plainly_timeless P : Timeless P → Timeless (bi_plainly P).
+Proof.
+  intros. rewrite /Timeless /bi_except_0 later_plainly_1.
+  by rewrite (timeless P) /bi_except_0 plainly_or {1}plainly_elim.
+Qed.
 Global Instance persistently_timeless P : Timeless P → Timeless (bi_persistently P).
 Proof.
   intros. rewrite /Timeless /bi_except_0 later_persistently_1.
diff --git a/theories/bi/fractional.v b/theories/bi/fractional.v
index 370f735b6324fe4c3b354a18d813bf9dbeb11ccd..7d1074804706c42705a86d7a44d152944b25a61c 100644
--- a/theories/bi/fractional.v
+++ b/theories/bi/fractional.v
@@ -142,7 +142,7 @@ Section fractional.
   Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
 
   (* The instance [frame_fractional] can be tried at all the nodes of
-     the proof search. The proof search then fails almost persistently on
+     the proof search. The proof search then fails almost always on
      [AsFractional R Φ r], but the slowdown is still noticeable.  For
      that reason, we factorize the three instances that could have been
      defined for that purpose into one. *)
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ced63e3f6d5cc24f02d2df6f8ce8d5d9b66f3041..3d1dbb6ea986ff58958b7221382d0add9df11fcf 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -8,7 +8,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}.
+  Context {PROP : Type} `{Dist PROP, Equiv PROP} (prop_ofe_mixin : OfeMixin PROP).
   Context (bi_entails : PROP → PROP → Prop).
   Context (bi_emp : PROP).
   Context (bi_pure : Prop → PROP).
@@ -20,6 +20,7 @@ Section bi_mixin.
   Context (bi_internal_eq : ∀ A : ofeT, A → A → PROP).
   Context (bi_sep : PROP → PROP → PROP).
   Context (bi_wand : PROP → PROP → PROP).
+  Context (bi_plainly : PROP → PROP).
   Context (bi_persistently : PROP → PROP).
   Context (bi_later : PROP → PROP).
 
@@ -55,6 +56,7 @@ 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;
     bi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (bi_internal_eq A);
 
@@ -97,18 +99,40 @@ 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 *)
+    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);
+    bi_mixin_plainly_exist_1 {A} (Ψ : A → PROP) :
+      bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a);
+
+    bi_mixin_prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢
+      bi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
+
+    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 *)
     bi_mixin_persistently_mono P Q :
       (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
     bi_mixin_persistently_idemp_2 P :
       bi_persistently P ⊢ bi_persistently (bi_persistently P);
+    bi_mixin_plainly_persistently_1 P :
+      bi_plainly (bi_persistently P) ⊢ bi_plainly P;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
       (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
       bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
 
-    bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
     bi_mixin_persistently_absorbing P Q :
       bi_persistently P ∗ Q ⊢ bi_persistently P;
     bi_mixin_persistently_and_sep_elim P Q :
@@ -129,6 +153,8 @@ 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 :
@@ -153,11 +179,12 @@ Structure bi := BI {
   bi_internal_eq : ∀ A : ofeT, A → A → 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_internal_eq
-                        bi_sep bi_wand bi_persistently;
+  bi_bi_mixin : BIMixin bi_ofe_mixin bi_entails bi_emp bi_pure bi_and bi_or
+                        bi_impl bi_forall bi_exist bi_internal_eq
+                        bi_sep bi_wand bi_plainly bi_persistently;
 }.
 
 Coercion bi_ofeC (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
@@ -174,6 +201,7 @@ Instance: Params (@bi_exist) 2.
 Instance: Params (@bi_internal_eq) 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.
@@ -191,6 +219,7 @@ Arguments bi_exist {PROP _} _%I : simpl never, rename.
 Arguments bi_internal_eq {PROP _} _ _ : 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 {
@@ -208,15 +237,16 @@ Structure sbi := SBI {
   sbi_internal_eq : ∀ A : ofeT, A → A → 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;
   bi_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_internal_eq
-                         sbi_sep sbi_wand sbi_persistently;
+  sbi_bi_mixin : BIMixin sbi_ofe_mixin sbi_entails 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;
   sbi_sbi_mixin : SBIMixin sbi_entails sbi_pure sbi_or sbi_impl
                            sbi_forall sbi_exist sbi_internal_eq
-                           sbi_sep sbi_persistently bi_later;
+                           sbi_sep sbi_plainly sbi_persistently bi_later;
 }.
 
 Arguments sbi_car : simpl never.
@@ -231,6 +261,7 @@ Arguments bi_exist {PROP _} _%I : simpl never, rename.
 Arguments bi_internal_eq {PROP _} _ _ : 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.
 
 Coercion sbi_ofeC (PROP : sbi) : ofeT := OfeT PROP (sbi_ofe_mixin PROP).
@@ -253,6 +284,7 @@ Arguments sbi_exist {PROP _} _%I : simpl never, rename.
 Arguments sbi_internal_eq {PROP _} _ _ : 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 bi_later {PROP} _%I : simpl never, rename.
 
@@ -327,6 +359,8 @@ 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.
 
@@ -360,7 +394,7 @@ Proof. eapply bi_mixin_impl_elim_l', bi_bi_mixin. Qed.
 Lemma forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
 Proof. eapply bi_mixin_forall_intro, bi_bi_mixin. Qed.
 Lemma forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. eapply (bi_mixin_forall_elim  bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_forall_elim  _ bi_entails), bi_bi_mixin. Qed.
 
 Lemma exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a.
 Proof. eapply bi_mixin_exist_intro, bi_bi_mixin. Qed.
@@ -393,7 +427,7 @@ Proof. eapply bi_mixin_emp_sep_1, bi_bi_mixin. Qed.
 Lemma emp_sep_2 P : emp ∗ P ⊢ P.
 Proof. eapply bi_mixin_emp_sep_2, bi_bi_mixin. Qed.
 Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P.
-Proof. eapply (bi_mixin_sep_comm' bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_sep_comm' _ bi_entails), bi_bi_mixin. Qed.
 Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R).
 Proof. eapply bi_mixin_sep_assoc', bi_bi_mixin. Qed.
 Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
@@ -401,12 +435,41 @@ 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 plainly_exist_1 {A} (Ψ : A → PROP) :
+  bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a).
+Proof. eapply bi_mixin_plainly_exist_1, bi_bi_mixin. Qed.
+Lemma prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+Proof. eapply (bi_mixin_prop_ext _ bi_entails), bi_bi_mixin. Qed.
+Lemma persistently_impl_plainly P Q :
+  (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.
 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 plainly_persistently_1 P :
+  bi_plainly (bi_persistently P) ⊢ bi_plainly P.
+Proof. eapply (bi_mixin_plainly_persistently_1 _ bi_entails), bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
@@ -415,10 +478,8 @@ Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
   bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a).
 Proof. eapply bi_mixin_persistently_exist_1, 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_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
-Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_persistently_absorbing _ bi_entails), bi_bi_mixin. Qed.
 Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q.
 Proof. eapply bi_mixin_persistently_and_sep_elim, bi_bi_mixin. Qed.
 End bi_laws.
@@ -450,6 +511,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.
 Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 7b14039a0f7de4a52d3a8124b569a374102a560a..e650a9f5f66a33e051ab35c028d8ea52f627ea5d 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -106,8 +106,11 @@ Proof.
   iModIntro; iNext; iMod "H" as ">?". by iApply IH.
 Qed.
 
-Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |==> ▷ P)%I).
-Proof. intros P Q HP. induction n; simpl; do 2?f_equiv; auto. Qed.
+Lemma bupd_iter_laterN_mono n P Q `{!Plain Q} :
+  (P ⊢ Q) → Nat.iter n (λ P, |==> ▷ P)%I P ⊢ ▷^n Q.
+Proof.
+  intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_plain.
+Qed.
 
 Lemma bupd_iter_frame_l n R Q :
   R ∗ Nat.iter n (λ P, |==> ▷ P) Q ⊢ Nat.iter n (λ P, |==> ▷ P) (R ∗ Q).
@@ -118,44 +121,42 @@ Qed.
 
 Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
   nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) →
-  world σ1 ∗ WP e1 {{ v, ⌜φ v⌝ }} ∗ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ v2⌝.
+  world σ1 ∗ WP e1 {{ v, ⌜φ v⌝ }} ∗ wptp t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝.
 Proof.
-  intros. rewrite wptp_steps //.
-  rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
+  intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
   iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
   iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
 Qed.
 
 Lemma wp_safe e σ Φ :
-  world σ ∗ WP e {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+  world σ -∗ WP e {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
 Proof.
-  rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) H]".
+  rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
   destruct (to_val e) as [v|] eqn:?; [eauto 10|].
-  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
-  eauto 10.
+  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
 Qed.
 
 Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 →
   world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
+  ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
-  intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
+  intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
-  apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
-  iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
+  apply elem_of_cons in He2 as [<-|?].
+  - iMod (wp_safe with "Hw H") as "$".
+  - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
 Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
   (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
-  ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ⌝.
+  ⊢ ▷^(S (S n)) ⌜φ⌝.
 Proof.
-  intros ?. rewrite wptp_steps //.
-  rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l. apply bupd_iter_mono.
-  iIntros "[Hback H]". iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
+  intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
+  apply: bupd_iter_laterN_mono.
+  iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
   rewrite fupd_eq.
   iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
 Qed.
@@ -170,19 +171,17 @@ Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
-    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
-    rewrite fupd_eq in Hwp. iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    eapply (soundness (M:=iResUR Σ) _ (S (S n))).
+    iMod wsat_alloc as (Hinv) "[Hw HE]".
+    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
-    iModIntro. iNext. iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto.
-    iFrame; auto.
+    iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
   - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
-    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+    eapply (soundness (M:=iResUR Σ) _ (S (S n))).
+    iMod wsat_alloc as (Hinv) "[Hw HE]".
     rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
-    iModIntro. iNext. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto.
-    iFrame; auto.
+    iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.
 
 Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
@@ -194,10 +193,9 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
   φ.
 Proof.
   intros Hwp [n ?]%rtc_nsteps.
-  eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-  rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
+  eapply (soundness (M:=iResUR Σ) _ (S (S n))).
+  iMod wsat_alloc as (Hinv) "[Hw HE]".
   rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
   iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
-  iModIntro. iNext. iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto.
-  iFrame; auto.
+  iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 70efe4a8fc8de075de9d439023cb9f23bbc0aa6a..3a05a88cc690f5606a0271e248fa4c1e9441a9e4 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -17,6 +17,9 @@ 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 (▲ 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.
+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.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
@@ -52,6 +55,24 @@ Global Instance from_assumption_absorbingly_r p P Q :
   FromAssumption p P Q → FromAssumption p P (▲ 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 `{AffineBI 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.
@@ -106,6 +127,8 @@ Global Instance into_pure_affinely P φ :
 Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
 Global Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (▲ 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.
@@ -144,6 +167,9 @@ Proof.
   by rewrite pure_wand_forall pure_impl pure_impl_forall.
 Qed.
 
+Global Instance from_pure_plainly P φ :
+  FromPure P φ → FromPure (bi_plainly P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
 Global Instance from_pure_persistently P φ :
   FromPure P φ → FromPure (bi_persistently P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
@@ -169,18 +195,26 @@ Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
 Proof. intros. by rewrite /IntoPersistent. Qed.
 
-(* FromPersistent *)
-Global Instance from_persistent_here P : FromPersistent false false P P | 1.
-Proof. by rewrite /FromPersistent. Qed.
-Global Instance from_persistent_persistently a P Q :
-  FromPersistent a false P Q → FromPersistent false true (bi_persistently P) Q | 0.
+(* FromAlways *)
+Global Instance from_always_here P : FromAlways false false false P P | 1.
+Proof. by rewrite /FromAlways. Qed.
+Global Instance from_always_plainly a pe pl P Q :
+  FromAlways a pe pl P Q → FromAlways false true true (bi_plainly P) Q | 0.
+Proof.
+  rewrite /FromAlways /= => <-.
+  destruct a, pe, pl; rewrite /= ?persistently_affinely ?plainly_affinely
+       !persistently_plainly ?plainly_idemp ?plainly_persistently //.
+Qed.
+Global Instance from_always_persistently a pe pl P Q :
+  FromAlways a pe pl P Q → FromAlways false true pl (bi_persistently P) Q | 0.
 Proof.
-  rewrite /FromPersistent /= => <-. by destruct a; rewrite /= ?persistently_affinely.
+  rewrite /FromAlways /= => <-.
+  destruct a, pe; rewrite /= ?persistently_affinely ?persistently_idemp //.
 Qed.
-Global Instance from_persistent_affinely a p P Q :
-  FromPersistent a p P Q → FromPersistent true p (bi_affinely P) Q | 0.
+Global Instance from_always_affinely a pe pl P Q :
+  FromAlways a pe pl P Q → FromAlways true pe pl (bi_affinely P) Q | 0.
 Proof.
-  rewrite /FromPersistent /= => <-. destruct a; by rewrite /= ?affinely_idemp.
+  rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp.
 Qed.
 
 (* IntoWand *)
@@ -234,6 +268,19 @@ 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 `{!AffineBI 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.
 Global Instance into_wand_persistently_true q R P Q :
   IntoWand true q R P Q → IntoWand true q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
@@ -241,10 +288,6 @@ Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
 
-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.
-
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
 Proof. by rewrite /FromAnd. Qed.
@@ -267,6 +310,15 @@ 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).
@@ -303,6 +355,10 @@ Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
 Global Instance from_sep_absorbingly P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▲ P) (▲ Q1) (▲ 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).
@@ -347,6 +403,16 @@ 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).
@@ -394,6 +460,9 @@ Global Instance into_sep_affinely P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_affinely P) Q1 Q2 | 20.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
 
+Global Instance into_sep_plainly `{PositiveBI PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
+Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
 Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 →
   IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -424,6 +493,9 @@ Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
 Global Instance from_or_absorbingly P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▲ P) (▲ Q1) (▲ Q2).
 Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
+Global Instance from_or_plainly P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
+Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
 Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
@@ -440,6 +512,9 @@ Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
 Global Instance into_or_absorbingly P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▲ P) (▲ Q1) (▲ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
+Global Instance into_or_plainly 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).
@@ -457,6 +532,9 @@ Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.
 Global Instance from_exist_absorbingly {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (▲ P) (λ a, ▲ (Φ 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. 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.
@@ -486,6 +564,9 @@ Qed.
 Global Instance into_exist_absorbingly {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (▲ P) (λ a, ▲ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
+Global Instance into_exist_plainly {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.
@@ -496,6 +577,9 @@ 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.
@@ -527,6 +611,9 @@ Global Instance from_forall_affinely `{AffineBI 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.
@@ -776,27 +863,31 @@ Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
 Global Instance into_wand_later p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
 Proof.
-  rewrite /IntoWand /= => HR. by rewrite !later_affinely_persistently_if_2 -later_wand HR.
+  rewrite /IntoWand /= => HR.
+    by rewrite !later_affinely_persistently_if_2 -later_wand HR.
 Qed.
 
 Global Instance into_wand_later_args p q R P Q :
   IntoWand p q R P Q → IntoWand' p q R (▷ P) (▷ Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !later_affinely_persistently_if_2 (later_intro (â–¡?p R)%I) -later_wand HR.
+  by rewrite !later_affinely_persistently_if_2
+             (later_intro (â–¡?p R)%I) -later_wand HR.
 Qed.
 
 Global Instance into_wand_laterN n p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
 Proof.
-  rewrite /IntoWand /= => HR. by rewrite !laterN_affinely_persistently_if_2 -laterN_wand HR.
+  rewrite /IntoWand /= => HR.
+    by rewrite !laterN_affinely_persistently_if_2 -laterN_wand HR.
 Qed.
 
 Global Instance into_wand_laterN_args n p q R P Q :
   IntoWand p q R P Q → IntoWand' p q R (▷^n P) (▷^n Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !laterN_affinely_persistently_if_2 (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
+  by rewrite !laterN_affinely_persistently_if_2
+             (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
 (* FromAnd *)
@@ -826,19 +917,22 @@ Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
 Proof.
   rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
-  by rewrite later_affinely_persistently_if_2 HP affinely_persistently_if_elim later_and.
+  by rewrite later_affinely_persistently_if_2 HP
+             affinely_persistently_if_elim later_and.
 Qed.
 Global Instance into_and_laterN n p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
 Proof.
   rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
-  by rewrite laterN_affinely_persistently_if_2 HP affinely_persistently_if_elim laterN_and.
+  by rewrite laterN_affinely_persistently_if_2 HP
+             affinely_persistently_if_elim laterN_and.
 Qed.
 Global Instance into_and_except_0 p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (◇ P) (◇ Q1) (◇ Q2).
 Proof.
   rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
-  by rewrite except_0_affinely_persistently_if_2 HP affinely_persistently_if_elim except_0_and.
+  by rewrite except_0_affinely_persistently_if_2 HP
+             affinely_persistently_if_elim except_0_and.
 Qed.
 
 (* IntoSep *)
@@ -945,8 +1039,12 @@ Proof. rewrite /IntoExcept0. destruct p; auto using except_0_intro. Qed.
 Global Instance into_timeless_affinely P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_affinely P) (bi_affinely Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_affinely_2. Qed.
-Global Instance into_timeless_absorbingly P Q : IntoExcept0 P Q → IntoExcept0 (▲ P) (▲ Q).
+Global Instance into_timeless_absorbingly P Q :
+  IntoExcept0 P Q → IntoExcept0 (▲ P) (▲ Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
+Global Instance into_timeless_plainly P Q :
+  IntoExcept0 P Q → IntoExcept0 (bi_plainly P) (bi_plainly Q).
+Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
 Global Instance into_timeless_persistently P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
@@ -1050,6 +1148,9 @@ Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
 Global Instance into_later_absorbingly n P Q :
   IntoLaterN n P Q → IntoLaterN n (▲ P) (▲ Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
+Global Instance into_later_plainly n P Q :
+  IntoLaterN n P Q → IntoLaterN n (bi_plainly P) (bi_plainly Q).
+Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
   IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
@@ -1127,6 +1228,9 @@ Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 Global Instance from_later_affinely n P Q `{AffineBI PROP} :
   FromLaterN n P Q → FromLaterN n (bi_affinely P) (bi_affinely Q).
 Proof. rewrite /FromLaterN=><-. by rewrite affinely_elim affine_affinely. Qed.
+Global Instance from_later_plainly n P Q :
+  FromLaterN n P Q → FromLaterN n (bi_plainly P) (bi_plainly Q).
+Proof. by rewrite /FromLaterN laterN_plainly=> ->. Qed.
 Global Instance from_later_persistently n P Q :
   FromLaterN n P Q → FromLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 88d6b667c26dc6614958adaf1975cc3358f651be..1d5f1139377c87c26fdd02d1635ec18a42aded06 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -55,11 +55,11 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
-  from_persistent : bi_affinely_if a (bi_persistently_if p Q) ⊢ P.
-Arguments FromPersistent {_} _ _ _%I _%I : simpl never.
-Arguments from_persistent {_} _ _ _%I _%I {_}.
-Hint Mode FromPersistent + - - ! - : typeclass_instances.
+Class FromAlways {PROP : bi} (a pe pl : bool) (P Q : PROP) :=
+  from_always : bi_affinely_if a (bi_persistently_if pe (bi_plainly_if pl Q)) ⊢ P.
+Arguments FromAlways {_} _ _ _ _%I _%I : simpl never.
+Arguments from_always {_} _ _ _ _%I _%I {_}.
+Hint Mode FromAlways + - - - ! - : typeclass_instances.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 850e3ce5bfc13778c313860a5c71432e5fab0cf6..7c003f2438b2f0032f6060f06aed683266e7a29b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -523,17 +523,70 @@ Qed.
 Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ⌜φ⌝ → Q) → (φ → Δ ⊢ Q).
 Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
-(** * Persistently *)
-Lemma tac_persistently_intro Δ a p Q Q' :
-  FromPersistent a p Q' Q →
-  (if a then TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) else TCTrue) →
-  ((if p then envs_clear_spatial Δ else Δ) ⊢ Q) → Δ ⊢ Q'.
+(** * Persistence and plainness modalities *)
+Class IntoPlainEnv (Γ1 Γ2 : env PROP) := {
+  into_plain_env_subenv : env_subenv Γ2 Γ1;
+  into_plain_env_plain : Plain ([∧] Γ2);
+}.
+
+Global Instance into_plain_env_nil : IntoPlainEnv Enil Enil.
+Proof. constructor. constructor. simpl; apply _. Qed.
+Global Instance into_plain_env_snoc_plain Γ1 Γ2 i P :
+  Plain P → IntoPlainEnv Γ1 Γ2 →
+  IntoPlainEnv (Esnoc Γ1 i P) (Esnoc Γ2 i P) | 1.
+Proof. intros ? [??]; constructor. by constructor. simpl; apply _. Qed.
+Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P :
+  IntoPlainEnv Γ1 Γ2 → IntoPlainEnv (Esnoc Γ1 i P) Γ2 | 2.
+Proof. intros [??]; constructor. by constructor. done. Qed.
+
+Lemma into_plain_env_sound Γ1 Γ2 :
+  IntoPlainEnv Γ1 Γ2 → (Envs Γ1 Enil) ⊢ bi_plainly (Envs Γ2 Enil).
+Proof .
+  intros [Hsub ?]. rewrite !of_envs_eq plainly_and plainly_pure /=. f_equiv.
+  { f_equiv=>-[/= ???]. split; auto. by eapply env_subenv_wf. }
+  rewrite !(right_id emp%I). trans (□ [∧] Γ2)%I.
+  - do 2 f_equiv. clear -Hsub.
+    induction Hsub as [|????? IH|????? IH]=>//=; rewrite IH //. apply and_elim_r.
+  - by rewrite {1}(plain ([∧] Γ2)) affinely_elim plainly_affinely
+               plainly_persistently persistently_plainly.
+Qed.
+
+Class IntoAlwaysEnvs (pe : bool) (pl : bool) (Δ1 Δ2 : envs PROP) := {
+  into_persistent_envs_persistent :
+    if pl then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
+    else env_persistent Δ1 = env_persistent Δ2;
+  into_persistent_envs_spatial :
+    if pe || pl then env_spatial Δ2 = Enil else env_spatial Δ1 = env_spatial Δ2
+}.
+
+Global Instance into_always_false_false Δ : IntoAlwaysEnvs false false Δ Δ.
+Proof. by split. Qed.
+Global Instance into_always_envs_true_false Γp Γs :
+  IntoAlwaysEnvs true false (Envs Γp Γs) (Envs Γp Enil).
+Proof. by split. Qed.
+Global Instance into_always_envs_x_true Γp1 Γp2 Γs1 pe :
+  IntoPlainEnv Γp1 Γp2 →
+  IntoAlwaysEnvs pe true (Envs Γp1 Γs1) (Envs Γp2 Enil).
+Proof. destruct pe; by split. Qed.
+
+Lemma tac_always_intro Δ Δ' a pe pl Q Q' :
+  FromAlways a pe pl Q' Q →
+  (if a then TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ')) else TCTrue) →
+  IntoAlwaysEnvs pe pl Δ' Δ →
+  (Δ ⊢ Q) → Δ' ⊢ Q'.
 Proof.
-  intros ? Haffine HQ. rewrite -(from_persistent a p Q') -HQ. destruct p=> /=.
-  - rewrite envs_clear_spatial_sound.
-    rewrite {1}(env_spatial_is_nil_affinely_persistently (envs_clear_spatial Δ)) //.
-    destruct a=> /=. by rewrite sep_elim_l. by rewrite affinely_elim sep_elim_l.
-  - destruct a=> //=. apply and_intro; auto using tac_emp_intro.
+  intros ? Haffine [Hep Hes] HQ. rewrite -(from_always a pe pl Q') -HQ.
+  trans (bi_affinely_if a Δ'); [destruct a=>//; by apply: affinely_intro|f_equiv].
+  destruct pl; [|destruct pe].
+  - rewrite (envs_clear_spatial_sound Δ') into_plain_env_sound sep_elim_l.
+    destruct Δ as [Δ ?]. rewrite orb_true_r /= in Hes. rewrite Hes /=.
+    destruct pe=>/= //. by rewrite persistently_plainly.
+  - rewrite (envs_clear_spatial_sound Δ') /= /envs_clear_spatial Hep.
+    destruct Δ as [Δ ?]. simpl in Hes. subst. simpl.
+    rewrite -(sep_elim_l (bi_persistently _)). f_equiv.
+    rewrite {1}(env_spatial_is_nil_affinely_persistently (Envs Δ Enil)) //.
+    by rewrite affinely_elim.
+  - destruct Δ, Δ'; simpl in *. by subst.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index c2280ac28670946d9307561e51e900de875eb0ec..31164e0be062b55b1f53cfde17e2511541271e5e 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -44,7 +44,7 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
   match Γapp with
   | Enil => Some Γ
   | Esnoc Γapp i x =>
-     Γ' ← env_app Γapp Γ; 
+     Γ' ← env_app Γapp Γ;
      match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
   end.
 
@@ -84,6 +84,13 @@ Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
   | env_Forall2_snoc Γ1 Γ2 i x y :
      env_Forall2 P Γ1 Γ2 → P x y → env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y).
 
+Inductive env_subenv {A} : relation (env A) :=
+  | env_subenv_nil : env_subenv Enil Enil
+  | env_subenv_snoc Γ1 Γ2 i x :
+     env_subenv Γ1 Γ2 → env_subenv (Esnoc Γ1 i x) (Esnoc Γ2 i x)
+  | env_subenv_skip Γ1 Γ2 i y :
+     env_subenv Γ1 Γ2 → env_subenv Γ1 (Esnoc Γ2 i y).
+
 Section env.
 Context {A : Type}.
 Implicit Types Γ : env A.
@@ -197,4 +204,12 @@ Proof. by induction 1; simplify. Qed.
 Lemma env_Forall2_wf {B} (P : A → B → Prop) Γ Σ :
   env_Forall2 P Γ Σ → env_wf Γ → env_wf Σ.
 Proof. induction 1; inversion_clear 1; eauto using env_Forall2_fresh. Qed.
+
+Lemma env_subenv_fresh Γ Σ i : env_subenv Γ Σ → Σ !! i = None → Γ !! i = None.
+Proof. by induction 1; simplify. Qed.
+Lemma env_subenv_wf Γ Σ : env_subenv Γ Σ → env_wf Σ → env_wf Γ.
+Proof. induction 1; inversion_clear 1; eauto using env_subenv_fresh. Qed.
+Global Instance env_to_list_subenv_proper :
+  Proper (env_subenv ==> sublist) (@env_to_list A).
+Proof. induction 1; simpl; constructor; auto. Qed.
 End env.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 7039f6ebc633743393189a8d3f5ae6be032c0802..f6ca7d33082c5491c3228157550958eee3f2e6bb 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -850,10 +850,11 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  eapply tac_persistently_intro;
+  eapply tac_always_intro;
     [apply _ (* || fail "iAlways: the goal is not a persistently modality" *)
     |env_cbv; apply _ ||
      fail "iAlways: spatial context contains non-affine hypotheses"
+    |apply _
     |env_cbv].
 
 (** * Later *)
@@ -1770,6 +1771,7 @@ Hint Extern 0 (_ ⊢ _) => progress iIntros.
 Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
+Hint Extern 1 (of_envs _ ⊢ bi_plainly _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ bi_persistently _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ bi_affinely _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.