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/big_op.v b/theories/base_logic/big_op.v
index 6079c922a11989c852610650be32d332e05ad851..f9fb0aeacffef8c9d239b828deb0ce8b6abdda02 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -149,6 +149,14 @@ Section list.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   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.
@@ -342,12 +350,19 @@ Section gmap.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   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.
   Global Instance big_sepM_persistent Φ m :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
+
   Global Instance big_sepM_nil_timeless Φ :
     Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
@@ -490,11 +505,18 @@ Section gset.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   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.
   Global Instance big_sepS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
+
   Global Instance big_sepS_nil_timeless Φ : Timeless ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
   Global Instance big_sepS_timeless Φ X :
@@ -578,11 +600,18 @@ Section gmultiset.
     □?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ 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.
   Global Instance big_sepMS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
+
   Global Instance big_sepMS_nil_timeless Φ : Timeless ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_timeless Φ X :
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 0875fde43fa25d793102d7e9f5c55825ed4e1b4f..76e2f0b93f95fe2009df2061b39f9c2611ef8971 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -39,6 +39,11 @@ Arguments persistent {_} _ {_}.
 Hint Mode Persistent + ! : typeclass_instances.
 Instance: Params (@Persistent) 1.
 
+Class Plain {M} (P : uPred M) := plain : P ⊢ ■ P.
+Arguments plain {_} _ {_}.
+Hint Mode Plain + ! : typeclass_instances.
+Instance: Params (@Plain) 1.
+
 Module uPred.
 Section derived.
 Context {M : ucmraT}.
@@ -471,6 +476,104 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
+(* Plainness modality *)
+Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@uPred_plainly M).
+Proof. intros P Q; apply plainly_mono. Qed.
+Global Instance naugth_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_plainly M).
+Proof. intros P Q; apply plainly_mono. Qed.
+
+Lemma plainly_elim P : ■ P ⊢ P.
+Proof. by rewrite plainly_elim' persistently_elim. Qed.
+Hint Resolve plainly_mono plainly_elim.
+Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
+Proof. intros <-. apply plainly_idemp. Qed.
+Lemma plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
+Proof. apply (anti_symm _); auto using plainly_idemp. Qed.
+
+Lemma persistently_plainly P : □ ■ P ⊣⊢ ■ P.
+Proof.
+  apply (anti_symm _); auto using persistently_elim.
+  by rewrite -plainly_elim' plainly_idemp.
+Qed.
+Lemma plainly_persistently P : ■ □ P ⊣⊢ ■ P.
+Proof.
+  apply (anti_symm _); auto using plainly_mono, persistently_elim.
+  by rewrite -plainly_elim' plainly_idemp.
+Qed.
+
+Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Proof.
+  apply (anti_symm _); auto.
+  apply pure_elim'=> Hφ.
+  trans (∀ x : False, ■ True : uPred M)%I; [by apply forall_intro|].
+  rewrite plainly_forall_2. auto using plainly_mono, pure_intro.
+Qed.
+Lemma plainly_forall {A} (Ψ : A → uPred M) : (■ ∀ a, Ψ a) ⊣⊢ (∀ a, ■ Ψ a).
+Proof.
+  apply (anti_symm _); auto using plainly_forall_2.
+  apply forall_intro=> x. by rewrite (forall_elim x).
+Qed.
+Lemma plainly_exist {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊣⊢ (∃ a, ■ Ψ 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 : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
+Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
+Lemma plainly_or P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
+Lemma plainly_impl P Q : ■ (P → Q) ⊢ ■ P → ■ Q.
+Proof.
+  apply impl_intro_l; rewrite -plainly_and.
+  apply plainly_mono, impl_elim with P; auto.
+Qed.
+Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+  apply (anti_symm (⊢)); auto using persistently_elim.
+  apply (internal_eq_rewrite a b (λ b, ■ (a ≡ b))%I); auto.
+  { intros n; solve_proper. }
+  rewrite -(internal_eq_refl a) plainly_pure; auto.
+Qed.
+
+Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
+Proof. by rewrite -persistently_plainly persistently_and_sep_l_1. Qed.
+Lemma plainly_and_sep_l' P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
+Proof. apply (anti_symm (⊢)); auto using plainly_and_sep_l_1. Qed.
+Lemma plainly_and_sep_r' P Q : P ∧ ■ Q ⊣⊢ P ∗ ■ Q.
+Proof. by rewrite !(comm _ P) plainly_and_sep_l'. Qed.
+Lemma plainly_sep_dup' P : ■ P ⊣⊢ ■ P ∗ ■ P.
+Proof. by rewrite -plainly_and_sep_l' idemp. Qed.
+
+Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊣⊢ ■ (P ∗ Q).
+Proof.
+  apply (anti_symm (⊢)); auto.
+  rewrite -{1}plainly_idemp plainly_and plainly_and_sep_l'; auto.
+Qed.
+Lemma plainly_sep P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Proof. by rewrite -plainly_and_sep -plainly_and_sep_l' plainly_and. Qed.
+
+Lemma plainly_wand P Q : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q.
+Proof. by apply wand_intro_r; rewrite -plainly_sep wand_elim_l. Qed.
+Lemma plainly_impl_wand P Q : ■ (P → Q) ⊣⊢ ■ (P -∗ Q).
+Proof.
+  apply (anti_symm (⊢)); [by rewrite -impl_wand_1|].
+  apply plainly_intro', impl_intro_r.
+  by rewrite plainly_and_sep_l' plainly_elim wand_elim_l.
+Qed.
+Lemma wand_impl_plainly P Q : (■ P -∗ Q) ⊣⊢ (■ 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.
+Lemma plainly_entails_l' P Q : (P ⊢ ■ Q) → P ⊢ ■ Q ∗ P.
+Proof. intros; rewrite -plainly_and_sep_l'; auto. Qed.
+Lemma plainly_entails_r' P Q : (P ⊢ ■ Q) → P ⊢ P ∗ ■ Q.
+Proof. intros; rewrite -plainly_and_sep_r'; auto. Qed.
+
+Lemma plainly_laterN n P : ■ ▷^n P ⊣⊢ ▷^n ■ P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite plainly_later IH. Qed.
+
 (* Always derived *)
 Hint Resolve persistently_mono persistently_elim.
 Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@uPred_persistently M).
@@ -485,12 +588,7 @@ Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
 Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed.
 
 Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof.
-  apply (anti_symm _); auto.
-  apply pure_elim'=> Hφ.
-  trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
-  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
-Qed.
+Proof. by rewrite -plainly_pure persistently_plainly. Qed.
 Lemma persistently_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof.
   apply (anti_symm _); auto using persistently_forall_2.
@@ -511,12 +609,7 @@ Proof.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 Lemma persistently_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
-  apply (anti_symm (⊢)); auto using persistently_elim.
-  apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
-  { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) persistently_pure; auto.
-Qed.
+Proof. by rewrite -plainly_internal_eq persistently_plainly. Qed.
 
 Lemma persistently_and_sep_l P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof. apply (anti_symm (⊢)); auto using persistently_and_sep_l_1. Qed.
@@ -616,7 +709,6 @@ Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
-
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.
@@ -747,6 +839,8 @@ Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
 Proof. by rewrite /uPred_except_0 persistently_or persistently_later persistently_pure. Qed.
 Lemma except_0_persistently_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
 Proof. destruct p; simpl; auto using except_0_persistently. Qed.
+Lemma except_0_plainly P : ◇ ■ P ⊣⊢ ■ ◇ P.
+Proof. by rewrite /uPred_except_0 plainly_or plainly_later plainly_pure. Qed.
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
@@ -764,11 +858,10 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by auto. apply ownM_unit. Qed.
+Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+Proof. apply (anti_symm _); auto using plainly_elim, plainly_cmra_valid_1. Qed.
 Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof.
-  intros; apply (anti_symm _); first by apply:persistently_elim.
-  apply:persistently_cmra_valid_1.
-Qed.
+Proof. by rewrite -plainly_cmra_valid persistently_plainly. Qed.
 
 (** * Derived rules *)
 Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
@@ -860,6 +953,25 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
   (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+(* Derived lemmas for plainness *)
+Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain M).
+Proof. solve_proper. Qed.
+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.
+
+(* Not an instance, see the bottom of this file *)
+Lemma plain_persistent P : Plain P → Persistent P.
+Proof. rewrite /Plain /Persistent=> HP. by rewrite {1}HP plainly_elim'. Qed.
+
+Lemma plainly_plainly P `{!Plain P} : ■ P ⊣⊢ P.
+Proof. apply (anti_symm (⊢)); eauto. Qed.
+Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■ Q.
+Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
+
+Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
+Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
+
 (* Derived lemmas for persistence *)
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent M).
 Proof. solve_proper. Qed.
@@ -889,20 +1001,71 @@ Proof.
   apply impl_intro_l. by rewrite and_sep_l wand_elim_r.
 Qed.
 
+(* Plain *)
+Global Instance pure_plain φ : Plain (⌜φ⌝ : uPred M)%I.
+Proof. by rewrite /Plain plainly_pure. Qed.
+Global Instance impl_plain P Q : Plain P → Plain Q → Plain (P → Q).
+Proof.
+  rewrite /Plain=> HP HQ.
+  by rewrite {2}HP -plainly_impl_plainly -HQ plainly_elim.
+Qed.
+Global Instance wand_plain P Q : Plain P → Plain Q → Plain (P -∗ Q)%I.
+Proof.
+  rewrite /Plain=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
+Qed.
+Global Instance plainly_plain P : Plain (â–  P).
+Proof. by intros; apply plainly_intro'. Qed.
+Global Instance persistently_plain P : Plain P → Plain (□ P).
+Proof. rewrite /Plain=> HP. by rewrite {1}HP persistently_plainly plainly_persistently. Qed.
+Global Instance and_plain P Q :
+  Plain P → Plain Q → Plain (P ∧ Q).
+Proof. by intros; rewrite /Plain plainly_and; apply and_mono. Qed.
+Global Instance or_plain P Q :
+  Plain P → Plain Q → Plain (P ∨ Q).
+Proof. by intros; rewrite /Plain plainly_or; apply or_mono. Qed.
+Global Instance sep_plain P Q :
+  Plain P → Plain Q → Plain (P ∗ Q).
+Proof. by intros; rewrite /Plain plainly_sep; apply sep_mono. Qed.
+Global Instance forall_plain {A} (Ψ : A → uPred M) :
+  (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
+Proof. by intros; rewrite /Plain plainly_forall; apply forall_mono. Qed.
+Global Instance exist_palin {A} (Ψ : A → uPred M) :
+  (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
+Proof. by intros; rewrite /Plain plainly_exist; apply exist_mono. Qed.
+Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+  Plain (a ≡ b : uPred M)%I.
+Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+Global Instance cmra_valid_plain {A : cmraT} (a : A) :
+  Plain (✓ a : uPred M)%I.
+Proof. by intros; rewrite /Plain; apply plainly_cmra_valid_1. Qed.
+Global Instance later_plain P : Plain P → Plain (▷ P).
+Proof. by intros; rewrite /Plain plainly_later; apply later_mono. Qed.
+Global Instance except_0_plain P : Plain P → Plain (◇ P).
+Proof. by intros; rewrite /Plain -except_0_plainly; apply except_0_mono. Qed.
+Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
+Proof. induction n; apply _. Qed.
+Global Instance from_option_palin {A} P (Ψ : A → uPred M) (mx : option A) :
+  (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
+Proof. destruct mx; apply _. Qed.
+
 (* Persistence *)
 Global Instance pure_persistent φ : Persistent (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /Persistent persistently_pure. Qed.
-Global Instance pure_impl_persistent φ Q :
-  Persistent Q → Persistent (⌜φ⌝ → Q)%I.
+Global Instance impl_persistent P Q :
+  Plain P → Persistent Q → Persistent (P → Q).
 Proof.
-  rewrite /Persistent pure_impl_forall persistently_forall. auto using forall_mono.
+  rewrite /Plain /Persistent=> HP HQ.
+  rewrite {2}HP -persistently_impl_plainly. by rewrite -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_persistent φ Q :
-  Persistent Q → Persistent (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_persistent P Q :
+  Plain P → Persistent Q → Persistent (P -∗ Q)%I.
 Proof.
-  rewrite /Persistent -impl_wand pure_impl_forall persistently_forall.
-  auto using forall_mono.
+  rewrite /Plain /Persistent=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -persistently_impl_plainly -HQ.
 Qed.
+Global Instance plainly_persistent P : Persistent (â–  P).
+Proof. by rewrite /Persistent persistently_plainly. Qed.
 Global Instance persistently_persistent P : Persistent (â–¡ P).
 Proof. by intros; apply persistently_intro'. Qed.
 Global Instance and_persistent P Q :
@@ -930,6 +1093,8 @@ Global Instance later_persistent P : Persistent P → Persistent (▷ P).
 Proof. by intros; rewrite /Persistent persistently_later; apply later_mono. Qed.
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
 Proof. induction n; apply _. Qed.
+Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
+Proof. by intros; rewrite /Persistent -except_0_persistently; apply except_0_mono. Qed.
 Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
 Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
@@ -947,6 +1112,9 @@ Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
 Global Instance uPred_persistently_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently M).
 Proof. split; [split; try apply _|]. apply persistently_and. apply persistently_pure. Qed.
+Global Instance uPred_plainly_and_homomorphism :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_and. apply plainly_pure. Qed.
 Global Instance uPred_persistently_if_and_homomorphism b :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently_if M b).
 Proof. split; [split; try apply _|]. apply persistently_if_and. apply persistently_if_pure. Qed.
@@ -963,6 +1131,9 @@ Proof. split; [split; try apply _|]. apply except_0_and. apply except_0_True. Qe
 Global Instance uPred_persistently_or_homomorphism :
   MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently M).
 Proof. split; [split; try apply _|]. apply persistently_or. apply persistently_pure. Qed.
+Global Instance uPred_plainly_or_homomorphism :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_or. apply plainly_pure. Qed.
 Global Instance uPred_persistently_if_or_homomorphism b :
   MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently_if M b).
 Proof. split; [split; try apply _|]. apply persistently_if_or. apply persistently_if_pure. Qed.
@@ -974,11 +1145,14 @@ Global Instance uPred_laterN_or_homomorphism n :
 Proof. split; try apply _. apply laterN_or. Qed.
 Global Instance uPred_except_0_or_homomorphism :
   WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_except_0 M).
-Proof. split; try apply _. apply except_0_or. Qed. 
+Proof. split; try apply _. apply except_0_or. Qed.
 
 Global Instance uPred_persistently_sep_homomorphism :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently M).
 Proof. split; [split; try apply _|]. apply persistently_sep. apply persistently_pure. Qed.
+Global Instance uPred_plainly_sep_homomorphism :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_sep. apply plainly_pure. Qed.
 Global Instance uPred_persistently_if_sep_homomorphism b :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently_if M b).
 Proof. split; [split; try apply _|]. apply persistently_if_sep. apply persistently_if_pure. Qed.
@@ -996,3 +1170,12 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 End uPred.
+
+(* When declared as an actual instance, [plain_persistent] will give cause
+failing proof searches to take exponential time, as Coq will try to apply it
+the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will only be
+used at the leaves of the proof search tree, i.e. when the premise of the hint
+can be derived from just the current context. *)
+Hint Immediate uPred.plain_persistent : typeclass_instances.
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index e6d584217ca120eb903dcc557cd024f17b7b7f14..f7cfb0ebb607fc58cb3cbdbe3335c48e1df68b78 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).
+    iApply persistently_impl_plainly. iIntros "#HQ".
+    iApply persistently_impl_plainly. iIntros "#HPQ".
+    iApply "HQ". by iApply "HC".
   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/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index 259eb66d28c31118b991225c71cdee14b0be16e1..90277119134f545d2053956938b4f10c743adb7d 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -40,13 +40,11 @@ Module savedprop. Section savedprop.
 
   Lemma contradiction : False.
   Proof using All.
-    apply (@soundness M False 1); simpl.
+    apply (@consistency M); simpl.
     iIntros "". iMod A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
-    iModIntro. iNext.
-    iApply "HN". iApply saved_A. done.
+    iApply "HN". by iApply saved_A.
   Qed.
-
 End savedprop. End savedprop.
 
 (** This proves that we need the â–· when opening invariants. *)
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 18d99c2017d88460b7af241a8ab1fea3856054ed..71af3c09c56ce281cbe9286998f2087a975e92d5 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -97,6 +97,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.
@@ -176,6 +184,8 @@ Notation "∀ x .. y , P" :=
 Notation "∃ x .. y , P" :=
   (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I)
   (at level 200, x binder, y binder, right associativity) : uPred_scope.
+Notation "â–  P" := (uPred_plainly P)
+  (at level 20, right associativity) : uPred_scope.
 Notation "â–¡ P" := (uPred_persistently P)
   (at level 20, right associativity) : uPred_scope.
 Notation "â–· P" := (uPred_later P)
@@ -198,7 +208,8 @@ Notation "P -∗ Q" := (P ⊢ Q)
 Module uPred.
 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_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
+  uPred_persistently_eq, uPred_plainly_eq, uPred_persistently_eq,
   uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq).
 Ltac unseal := rewrite !unseal_eqs /=.
 
@@ -295,6 +306,13 @@ Proof.
 Qed.
 Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
+Global Instance plainly_ne : NonExpansive (@uPred_plainly M).
+Proof.
+  intros n P1 P2 HP.
+  unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
+Qed.
+Global Instance plainly_proper :
+  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_plainly M) := ne_proper _.
 Global Instance persistently_ne : NonExpansive (@uPred_persistently M).
 Proof.
   intros n P1 P2 HP.
@@ -421,6 +439,25 @@ Proof.
   eapply HPQR; eauto using cmra_validN_op_l.
 Qed.
 
+(* The plainness modality *)
+Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
+Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
+Lemma plainly_elim' P : ■ P ⊢ □ P.
+Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
+Lemma plainly_idemp P : ■ P ⊢ ■ ■ P.
+Proof. unseal; split=> n x ?? //. Qed.
+
+Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ■ Ψ a) ⊢ (■ ∀ a, Ψ a).
+Proof. by unseal. Qed.
+Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a).
+Proof. by unseal. Qed.
+
+Lemma prop_ext P Q : ■ ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+Proof.
+  unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
+    split; eapply HPQ; eauto using @ucmra_unit_least.
+Qed.
+
 (* Always *)
 Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
 Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
@@ -443,6 +480,20 @@ Proof.
   by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 
+Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q).
+Proof.
+  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.
+Qed.
+
+Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
+Proof.
+  unseal; split=> /= n x ? HPQ n' x' ????.
+  eapply uPred_mono with ε, cmra_included_includedN; auto.
+  apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
 (* Later *)
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.
@@ -477,6 +528,8 @@ Proof.
 Qed.
 Lemma persistently_later P : □ ▷ P ⊣⊢ ▷ □ P.
 Proof. by unseal. Qed.
+Lemma plainly_later P : ■ ▷ P ⊣⊢ ▷ ■ P.
+Proof. by unseal. Qed.
 
 (* Own *)
 Lemma ownM_op (a1 a2 : M) :
@@ -512,7 +565,7 @@ Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → uPred_valid (M:=M) (✓ a
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
 Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
 Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ ✓ a.
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a.
 Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
@@ -549,6 +602,12 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
+Lemma bupd_plainly P : (|==> ■ 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.
 
 (* Products *)
 Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index e2c764eee6b59f7b913c5647a71c1a9ccb1466b8..58b19d4d3880db8a329b32cb8ed12115d45e9c46 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -6,18 +6,14 @@ Section adequacy.
 Context {M : ucmraT}.
 
 (** Consistency and adequancy statements *)
-Lemma soundness φ n : (Nat.iter n (λ P, |==> ▷ P) (@uPred_pure M φ))%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; try unseal; by eauto using ucmra_unit_validN. }
-  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 /uPred_laterN; unseal. induction n as [|n IH]=> H; auto.
 Qed.
 
-Corollary consistency_modal n :
-  ¬ (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 : ¬ (False : uPred M)%I.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index ca5667882a01646d1cb565000918969d3ec1773d..8d6f9a85b3517fdd6c8e9be2b3bc322859fcb903 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]".
+    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.
-    by iFrame.
+    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.
-    by iFrame.
+    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.
-  by iFrame.
+  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 234053f121ee02fc717e7ec1aa2e14b64be38c70..81eef985bda13aa51531be6208069b18d920d1cb 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -19,6 +19,9 @@ Global Instance from_assumption_persistently_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite persistent_persistently. Qed.
 
+Global Instance from_assumption_plainly_l p P Q :
+  FromAssumption p P Q → FromAssumption p (■ P) Q.
+Proof. rewrite /FromAssumption=><-. by rewrite plainly_elim. Qed.
 Global Instance from_assumption_persistently_l p P Q :
   FromAssumption p P Q → FromAssumption p (□ P) Q.
 Proof. rewrite /FromAssumption=><-. by rewrite persistently_elim. Qed.
@@ -48,6 +51,8 @@ Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
   @IntoPure M (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
+Global Instance into_pure_plainly P φ : IntoPure P φ → IntoPure (■ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite plainly_pure. Qed.
 Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (□ P) φ.
 Proof. rewrite /IntoPure=> ->. by rewrite persistently_pure. Qed.
 
@@ -95,6 +100,8 @@ Proof.
   rewrite -cmra_valid_intro //. auto with I.
 Qed.
 
+Global Instance from_pure_plainly P φ : FromPure P φ → FromPure (■ P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
 Global Instance from_pure_persistently P φ : FromPure P φ → FromPure (□ P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
 Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
@@ -145,6 +152,12 @@ Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
 Proof. done. Qed.
 
+(* FromAlways *)
+Global Instance from_always_persistently P : FromAlways false (â–¡ P) P.
+Proof. by rewrite /FromAlways. Qed.
+Global Instance from_always_plainly P : FromAlways true (â–  P) P.
+Proof. by rewrite /FromAlways. Qed.
+
 (* IntoLater *)
 Global Instance into_laterN_later n P Q :
   IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.
@@ -254,6 +267,9 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
   FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
 Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 
+Global Instance from_later_plainly n P Q :
+  FromLaterN n P Q → FromLaterN n (■ P) (■ Q).
+Proof. by rewrite /FromLaterN -plainly_laterN=> ->. Qed.
 Global Instance from_later_persistently n P Q :
   FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
 Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
@@ -306,6 +322,9 @@ Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
 Global Instance into_wand_forall {A} p (Φ : A → uPred M) P Q x :
   IntoWand p (Φ x) P Q → IntoWand p (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
+Global Instance into_wand_plainly p R P Q :
+  IntoWand p R P Q → IntoWand p (■ R) P Q.
+Proof. rewrite /IntoWand=> ->. by rewrite plainly_elim. Qed.
 Global Instance into_wand_persistently p R P Q :
   IntoWand p R P Q → IntoWand p (□ R) P Q.
 Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
@@ -343,6 +362,12 @@ Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
 
 Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
+Global Instance from_and_plainly p P Q1 Q2 :
+  FromAnd false P Q1 Q2 → FromAnd p (■ P) (■ Q1) (■ Q2).
+Proof.
+  intros. apply mk_from_and_and.
+  by rewrite plainly_and_sep_l' -plainly_sep -(from_and _ P).
+Qed.
 Global Instance from_and_persistently p P Q1 Q2 :
   FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
@@ -434,10 +459,14 @@ Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
+Global Instance into_and_plainly p P Q1 Q2 :
+  IntoAnd true P Q1 Q2 → IntoAnd p (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?plainly_and and_sep_r. Qed.
 Global Instance into_and_persistently p P Q1 Q2 :
   IntoAnd true P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
-  rewrite /IntoAnd=>->. destruct p; by rewrite ?persistently_and persistently_and_sep_r.
+  rewrite /IntoAnd=>->.
+  destruct p; by rewrite ?persistently_and persistently_and_sep_r.
 Qed.
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -619,6 +648,9 @@ Global Instance from_or_bupd P Q1 Q2 :
 Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
 Global Instance from_or_pure φ ψ : @FromOr M ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /FromOr pure_or. Qed.
+Global Instance from_or_plainly P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
 Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
 Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
@@ -637,6 +669,9 @@ Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
 Proof. done. Qed.
 Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoOr pure_or. Qed.
+Global Instance into_or_plainly P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
 Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
@@ -661,6 +696,9 @@ Qed.
 Global Instance from_exist_pure {A} (φ : A → Prop) :
   @FromExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /FromExist pure_exist. Qed.
+Global Instance from_exist_plainly {A} P (Φ : A → uPred M) :
+  FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /FromExist=> <-. by rewrite plainly_exist. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → uPred M) :
   FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
@@ -698,6 +736,9 @@ Proof.
   apply pure_elim_sep_l=> Hφ. by rewrite -(exist_intro Hφ).
 Qed.
 
+Global Instance into_exist_plainly {A} P (Φ : A → uPred M) :
+  IntoExist P Φ → IntoExist (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → uPred M) :
   IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
@@ -714,6 +755,9 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → uPred M) : IntoForall (∀ a, Φ a) Φ.
 Proof. done. Qed.
+Global Instance into_forall_plainly {A} P (Φ : A → uPred M) :
+  IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
@@ -768,12 +812,21 @@ Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
 
+Global Instance elim_modal_plainly P Q : ElimModal (â–  P) P Q Q.
+Proof. intros. by rewrite /ElimModal plainly_elim wand_elim_r. Qed.
+
 Global Instance elim_modal_persistently P Q : ElimModal (â–¡ P) P Q Q.
 Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. 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 elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)).
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 028fe94410b757b3ea6b83f188949f639c8296b2..57aae7cd8239553e4781a86c9bf742dc2369c49b 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -59,6 +59,11 @@ Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
 Arguments into_persistent {_} _ _ _ {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
+Class FromAlways {M} (p : bool) (P Q : uPred M) :=
+  from_always : (if p then ■ Q else □ Q) ⊢ P.
+Arguments from_always {_} _ _ _ {_}.
+Hint Mode FromAlways + - ! - : typeclass_instances.
+
 (* The class [IntoLaterN] has only two instances:
 
 - The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
@@ -252,7 +257,7 @@ with the exception of:
 - [FromAssumption] used by [iAssumption]
 - [Frame] used by [iFrame]
 - [IntoLaterN] and [FromLaterN] used by [iNext]
-- [IntoPersistentP] used by [iPersistent]
+- [IntoPersistent] used by [iPersistent]
 *)
 Instance into_pure_tc_opaque {M} (P : uPred M) φ :
   IntoPure P φ → IntoPure (tc_opaque P) φ := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 724e7175e748a9a38262475810279321e930fbf8..4ae794247b2adcc952d37f6d5a8aa968543db566 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -473,12 +473,58 @@ Proof.
   by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
 Qed.
 
-(** * Always *)
-Lemma tac_persistently_intro Δ Q :
-  (envs_clear_spatial Δ ⊢ Q) → Δ ⊢ □ Q.
+(** * Persistence and plainness modality *)
+Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
+  into_plain_env_subenv : env_subenv Γ2 Γ1;
+  into_plain_env_plain : Plain ([∗] Γ2);
+}.
+Class IntoPersistentEnvs (p : bool) (Δ1 Δ2 : envs M) := {
+  into_persistent_envs_persistent :
+    if p then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
+    else env_persistent Δ1 = env_persistent Δ2;
+  into_persistent_envs_spatial : env_spatial Δ2 = Enil
+}.
+
+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.
+
+Global Instance into_persistent_envs_false Γp Γs :
+  IntoPersistentEnvs false (Envs Γp Γs) (Envs Γp Enil).
+Proof. by split. Qed.
+Global Instance into_persistent_envs_true Γp1 Γp2 Γs1 :
+  IntoPlainEnv Γp1 Γp2 →
+  IntoPersistentEnvs true (Envs Γp1 Γs1) (Envs Γp2 Enil).
+Proof. by split. Qed.
+
+Lemma into_persistent_envs_sound (p : bool) Δ1 Δ2 :
+  IntoPersistentEnvs p Δ1 Δ2 → Δ1 ⊢ (if p then ■ Δ2 else □ Δ2).
+Proof.
+  rewrite /of_envs. destruct Δ1 as [Γp1 Γs1], Δ2 as [Γp2 Γs2]=> -[/= Hp ->].
+  apply pure_elim_sep_l=> Hwf. rewrite sep_elim_l. destruct p; simplify_eq/=.
+  - destruct Hp. rewrite right_id plainly_sep plainly_pure.
+    apply sep_intro_True_l; [apply pure_intro|].
+    + destruct Hwf; constructor; eauto using Enil_wf, env_subenv_wf.
+    + rewrite persistently_elim plainly_persistently plainly_plainly.
+      by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
+  - rewrite right_id persistently_sep persistently_pure.
+    apply sep_intro_True_l; [apply pure_intro|by rewrite persistent_persistently].
+    destruct Hwf; constructor; simpl; eauto using Enil_wf.
+Qed.
+
+Lemma tac_always_intro Δ Δ' p Q Q' :
+  FromAlways p Q' Q →
+  IntoPersistentEnvs p Δ Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q'.
 Proof.
-  intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
-  by apply (persistently_intro _ _).
+  intros ?? HQ. rewrite into_persistent_envs_sound -(from_always _ Q').
+  destruct p; auto using persistently_mono, plainly_mono.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 8ed1a9bf68c27eff6218e374fdc5d9392c461a8a..a96b0c84e0c9b68fa90679a6e91fffc4cc58a298 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -78,6 +78,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.
@@ -191,4 +198,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 cfc0658260fd598ed221f0fac755a92a0be74082..6164ad82eb2274ba0c426e24d736bc84b80ba033 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -802,8 +802,10 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  apply tac_persistently_intro; env_cbv
-    || fail "iAlways: the goal is not an persistently modality".
+  eapply tac_always_intro;
+    [apply _ || fail "iAlways: the goal is not a persistence/plainness modality"
+    |env_cbv; apply _
+    |].
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1715,6 +1717,7 @@ Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
 Hint Extern 1 (of_envs _ ⊢ □ _) => iAlways.
+Hint Extern 1 (of_envs _ ⊢ ■ _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
 Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.