diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 9b9daea32a22a5a4ff0b6ca3b520d6d444b436e9..5eac49b7c4fb40a49add52f4005f671f213d0fe7 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -126,7 +126,7 @@ Section list.
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall Φ l :
-    (∀ k x, PersistentP (Φ k x)) →
+    (∀ k x, PersistentP true (Φ k x)) →
     ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
     intros HΦ. apply (anti_symm _).
@@ -149,14 +149,14 @@ Section list.
     by rewrite -always_wand_impl always_elim wand_elim_l.
   Qed.
 
-  Global Instance big_sepL_nil_persistent Φ :
-    PersistentP ([∗ list] k↦x ∈ [], Φ k x).
+  Global Instance big_sepL_nil_persistent c Φ :
+    PersistentP c ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL_persistent Φ l :
-    (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x).
+  Global Instance big_sepL_persistent c Φ l :
+    (∀ k x, PersistentP c (Φ k x)) → PersistentP c ([∗ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
-  Global Instance big_sepL_persistent_id Ps :
-    TCForall PersistentP Ps → PersistentP ([∗] Ps).
+  Global Instance big_sepL_persistent_id c Ps :
+    TCForall (PersistentP c) Ps → PersistentP c ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
 
   Global Instance big_sepL_nil_timeless Φ :
@@ -316,7 +316,7 @@ Section gmap.
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall Φ m :
-    (∀ k x, PersistentP (Φ k x)) →
+    (∀ k x, PersistentP true (Φ k x)) →
     ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x).
   Proof.
     intros. apply (anti_symm _).
@@ -342,11 +342,11 @@ Section gmap.
     by rewrite -always_wand_impl always_elim wand_elim_l.
   Qed.
 
-  Global Instance big_sepM_empty_persistent Φ :
-    PersistentP ([∗ map] k↦x ∈ ∅, Φ k x).
+  Global Instance big_sepM_empty_persistent c Φ :
+    PersistentP c ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
-  Global Instance big_sepM_persistent Φ m :
-    (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x).
+  Global Instance big_sepM_persistent c Φ m :
+    (∀ k x, PersistentP c (Φ k x)) → PersistentP c ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
   Global Instance big_sepM_nil_timeless Φ :
     TimelessP ([∗ map] k↦x ∈ ∅, Φ k x).
@@ -468,7 +468,7 @@ Section gset.
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall Φ X :
-    (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
+    (∀ x, PersistentP true (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
   Proof.
     intros. apply (anti_symm _).
     { apply forall_intro=> x.
@@ -490,10 +490,10 @@ Section gset.
     by rewrite -always_wand_impl always_elim wand_elim_l.
   Qed.
 
-  Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x).
+  Global Instance big_sepS_empty_persistent c Φ : PersistentP c ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
-  Global Instance big_sepS_persistent Φ X :
-    (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x).
+  Global Instance big_sepS_persistent c Φ X :
+    (∀ x, PersistentP c (Φ x)) → PersistentP c ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
   Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
@@ -578,10 +578,10 @@ Section gmultiset.
     □?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Global Instance big_sepMS_empty_persistent Φ : PersistentP ([∗ mset] x ∈ ∅, Φ x).
+  Global Instance big_sepMS_empty_persistent c Φ : PersistentP c ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
-  Global Instance big_sepMS_persistent Φ X :
-    (∀ x, PersistentP (Φ x)) → PersistentP ([∗ mset] x ∈ X, Φ x).
+  Global Instance big_sepMS_persistent c Φ X :
+    (∀ x, PersistentP c (Φ x)) → PersistentP c ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
   Global Instance big_sepMS_nil_timeless Φ : TimelessP ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index cdecce17dc9b8a3d6f0db94b2db15db0a9cf8da9..81c79423e20a290a9a4aaa90ccbccf740bd19161 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -16,11 +16,13 @@ Notation "â–·? p P" := (uPred_laterN (Nat.b2n p) P)
   (at level 20, p at level 9, P at level 20,
    format "â–·? p  P") : uPred_scope.
 
-Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
-  (if p then â–¡ P else P)%I.
+Definition uPred_always_if {M} (c p : bool) (P : uPred M) : uPred M :=
+  (if p then â–¡{c} P else P)%I.
 Instance: Params (@uPred_always_if) 2.
-Arguments uPred_always_if _ !_ _/.
-Notation "â–¡? p P" := (uPred_always_if p P)
+Arguments uPred_always_if _ _ !_ _/.
+Notation "â–¡{ c }? p P" := (uPred_always_if c p P)
+  (at level 20, c at next level, p at level 9, P at level 20, format "â–¡{ c }? p  P").
+Notation "â–¡? p P" := (uPred_always_if true p P)
   (at level 20, p at level 9, P at level 20, format "â–¡? p  P").
 
 Definition uPred_except_0 {M} (P : uPred M) : uPred M := ▷ False ∨ P.
@@ -34,15 +36,10 @@ Arguments timelessP {_} _ {_}.
 Hint Mode TimelessP + ! : typeclass_instances.
 Instance: Params (@TimelessP) 1.
 
-Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
-Arguments persistentP {_} _ {_}.
-Hint Mode PersistentP + ! : typeclass_instances.
-Instance: Params (@PersistentP) 1.
-
-Class PlainP {M} (P : uPred M) := plainP : P ⊢ ☃ P.
-Arguments plainP {_} _ {_}.
-Hint Mode PlainP + ! : typeclass_instances.
-Instance: Params (@PlainP) 1.
+Class PersistentP {M} (c : bool) (P : uPred M) := persistentP : P ⊢ □{c} P.
+Arguments persistentP {_} _ _ {_}.
+Hint Mode PersistentP + + ! : typeclass_instances.
+Instance: Params (@PersistentP) 2.
 
 Module uPred.
 Section derived.
@@ -476,178 +473,105 @@ 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.
 
-(* Plain 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.
+(* The always modality *)
+Global Instance always_mono' c : Proper ((⊢) ==> (⊢)) (@uPred_always M c).
+Proof. intros P Q; apply always_mono. Qed.
+Global Instance always_flip_mono' c :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M c).
+Proof. intros P Q; apply always_mono. Qed.
 
-Lemma plainly_elim P : ☃ P ⊢ P.
-Proof. by rewrite plainly_elim' always_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 always_elim c P : □{c} P ⊢ P.
+Proof. destruct c; by rewrite ?always_mask_mono always_elim'. Qed.
+Hint Resolve always_elim always_mono.
+Lemma always_intro' c P Q : (□{c} P ⊢ Q) → □{c} P ⊢ □{c} Q.
+Proof. intros <-. apply always_idemp_2. Qed.
+Lemma always_idemp c P : □{c} □{c} P ⊣⊢ □{c} P.
+Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
-Lemma always_plainly P : □ ☃ P ⊣⊢ ☃ P.
+Lemma always_idemp' c P : □ □{c} P ⊣⊢ □{c} P.
 Proof.
   apply (anti_symm _); auto using always_elim.
-  by rewrite -plainly_elim' plainly_idemp.
+  destruct c; [|rewrite -always_mask_mono]; by rewrite always_idemp.
 Qed.
-Lemma plainly_always P : ☃ □ P ⊣⊢ ☃ P.
+Lemma always_idemp'' c P : □{c} □ P ⊣⊢ □{c} P.
 Proof.
-  apply (anti_symm _); auto using plainly_mono, always_elim.
-  by rewrite -plainly_elim' plainly_idemp.
+  apply (anti_symm _); auto using always_elim.
+  destruct c; [|rewrite -always_mask_mono]; by rewrite always_idemp.
 Qed.
 
-Lemma plainly_pure φ : ☃ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma always_pure c φ : □{c} ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 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.
+  trans (∀ x : False, □{c} True : uPred M)%I; [by apply forall_intro|].
+  rewrite always_forall_2. auto using always_mono, pure_intro.
 Qed.
-Lemma plainly_forall {A} (Ψ : A → uPred M) : (☃ ∀ a, Ψ a) ⊣⊢ (∀ a, ☃ Ψ a).
+Lemma always_forall {A} c (Ψ : A → uPred M) : (□{c} ∀ a, Ψ a) ⊣⊢ (∀ a, □{c} Ψ a).
 Proof.
-  apply (anti_symm _); auto using plainly_forall_2.
+  apply (anti_symm _); auto using always_forall_2.
   apply forall_intro=> x. by rewrite (forall_elim x).
 Qed.
-Lemma plainly_exist {A} (Ψ : A → uPred M) : (☃ ∃ a, Ψ a) ⊣⊢ (∃ a, ☃ Ψ a).
+Lemma always_exist {A} c (Ψ : A → uPred M) : (□{c} ∃ a, Ψ a) ⊣⊢ (∃ a, □{c} Ψ a).
 Proof.
-  apply (anti_symm _); auto using plainly_exist_1.
+  apply (anti_symm _); auto using always_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.
+Lemma always_and c P Q : □{c} (P ∧ Q) ⊣⊢ □{c} P ∧ □{c} Q.
+Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
+Lemma always_or c P Q : □{c} (P ∨ Q) ⊣⊢ □{c} P ∨ □{c} Q.
+Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
+Lemma always_impl c P Q : □{c} (P → Q) ⊢ □{c} P → □{c} Q.
 Proof.
-  apply impl_intro_l; rewrite -plainly_and.
-  apply plainly_mono, impl_elim with P; auto.
+  apply impl_intro_l; rewrite -always_and.
+  apply always_mono, impl_elim with P; auto.
 Qed.
-Lemma plainly_internal_eq {A:ofeT} (a b : A) : ☃ (a ≡ b) ⊣⊢ a ≡ b.
+Lemma always_internal_eq {A : ofeT} c (a b : A) : □{c} (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)); auto using always_elim.
-  apply (internal_eq_rewrite a b (λ b, ☃ (a ≡ b))%I); auto.
+  apply (internal_eq_rewrite a b (λ b, □{c} (a ≡ b))%I); auto.
   { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) plainly_pure; auto.
+  rewrite -(internal_eq_refl a) always_pure; auto.
 Qed.
-
-Lemma plainly_and_sep_l_1 P Q : ☃ P ∧ Q ⊢ ☃ P ∗ Q.
-Proof. by rewrite -always_plainly always_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).
+Lemma always_and_sep_l' c P Q : □{c} P ∧ Q ⊣⊢ □{c} 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_wand_impl P Q : ☃ (P -∗ Q) ⊣⊢ ☃ (P → Q).
-Proof.
-  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
-  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].
-  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 always_mono always_elim.
-Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
-Global Instance always_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
-
-Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros <-. apply always_idemp_2. Qed.
-Lemma always_idemp P : □ □ P ⊣⊢ □ P.
-Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
-
-Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof. by rewrite -plainly_pure always_plainly. Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
-Proof.
-  apply (anti_symm _); auto using always_forall_2.
-  apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
-Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
-Proof.
-  apply (anti_symm _); auto using always_exist_1.
-  apply exist_elim=> x. by rewrite (exist_intro x).
-Qed.
-Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
-Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
-Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
-Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
-Lemma always_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
-Proof.
-  apply impl_intro_l; rewrite -always_and.
-  apply always_mono, impl_elim with P; auto.
+  by rewrite -always_idemp' always_and_sep_l_1'.
 Qed.
-Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
-Proof. by rewrite -plainly_internal_eq always_plainly. Qed.
-
-Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
-Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
+Lemma always_and_sep_r' c P Q : P ∧ □{c} Q ⊣⊢ P ∗ □{c} Q.
 Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
+Lemma always_sep_dup' c P : □{c} P ⊣⊢ □{c} P ∗ □{c} P.
 Proof. by rewrite -always_and_sep_l' idemp. Qed.
 
-Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Lemma always_and_sep c P Q : □{c} (P ∧ Q) ⊣⊢ □{c} (P ∗ Q).
 Proof.
   apply (anti_symm (⊢)); auto.
   rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
 Qed.
-Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma always_sep c P Q : □{c} (P ∗ Q) ⊣⊢ □{c} P ∗ □{c} Q.
 Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
 
-Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
+Lemma always_wand c P Q : □{c} (P -∗ Q) ⊢ □{c} P -∗ □{c} Q.
 Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
-Lemma always_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q).
+Lemma always_wand_impl c P Q : □{c} (P -∗ Q) ⊣⊢ □{c} (P → Q).
 Proof.
   apply (anti_symm (⊢)); [|by rewrite -impl_wand].
   apply always_intro', impl_intro_r.
   by rewrite always_and_sep_l' always_elim wand_elim_l.
 Qed.
-Lemma wand_impl_always P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
+Lemma wand_impl_always c P Q : (□{c} P -∗ Q) ⊣⊢ (□{c} P → Q).
 Proof.
   apply (anti_symm (⊢)); [|by rewrite -impl_wand].
   apply impl_intro_l. by rewrite always_and_sep_l' wand_elim_r.
 Qed.
-Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
+Lemma always_entails_l' c P Q : (P ⊢ □{c} Q) → P ⊢ □{c} Q ∗ P.
 Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
+Lemma always_entails_r' c P Q : (P ⊢ □{c} Q) → P ⊢ P ∗ □{c} Q.
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
-Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
+Lemma always_laterN c n P : □{c} ▷^n P ⊣⊢ ▷^n □{c} P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
 
-Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
+Lemma wand_alt c P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □{c} (P ∗ R → Q).
 Proof.
   apply (anti_symm (⊢)).
   - rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
@@ -656,7 +580,7 @@ Proof.
   - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -always_and_sep_r'.
     by rewrite always_elim impl_elim_r.
 Qed.
-Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
+Lemma impl_alt c P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □{c} (P ∧ R -∗ Q).
 Proof.
   apply (anti_symm (⊢)).
   - rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I).
@@ -764,31 +688,31 @@ Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
 
 (* Conditional always *)
-Global Instance always_if_ne p : NonExpansive (@uPred_always_if M p).
+Global Instance always_if_ne c p : NonExpansive (@uPred_always_if M c p).
 Proof. solve_proper. Qed.
-Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
+Global Instance always_if_proper c p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M c p).
 Proof. solve_proper. Qed.
-Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
+Global Instance always_if_mono c p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M c p).
 Proof. solve_proper. Qed.
 
-Lemma always_if_elim p P : □?p P ⊢ P.
+Lemma always_if_elim c p P : □{c}?p P ⊢ P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_elim_if p P : □ P ⊢ □?p P.
+Lemma always_elim_if c p P : □{c} P ⊢ □{c}?p P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
 
-Lemma always_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma always_if_pure c p φ : □{c}?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. destruct p; simpl; auto using always_pure. Qed.
-Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Lemma always_if_and c p P Q : □{c}?p (P ∧ Q) ⊣⊢ □{c}?p P ∧ □{c}?p Q.
 Proof. destruct p; simpl; auto using always_and. Qed.
-Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
+Lemma always_if_or c p P Q : □{c}?p (P ∨ Q) ⊣⊢ □{c}?p P ∨ □{c}?p Q.
 Proof. destruct p; simpl; auto using always_or. Qed.
-Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
+Lemma always_if_exist {A} c p (Ψ : A → uPred M) : (□{c}?p ∃ a, Ψ a) ⊣⊢ ∃ a, □{c}?p Ψ a.
 Proof. destruct p; simpl; auto using always_exist. Qed.
-Lemma always_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
+Lemma always_if_sep c p P Q : □{c}?p (P ∗ Q) ⊣⊢ □{c}?p P ∗ □{c}?p Q.
 Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
+Lemma always_if_later c p P : □{c}?p ▷ P ⊣⊢ ▷ □{c}?p P.
 Proof. destruct p; simpl; auto using always_later. Qed.
-Lemma always_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
+Lemma always_if_laterN c p n P : □{c}?p ▷^n P ⊣⊢ ▷^n □{c}?p P.
 Proof. destruct p; simpl; auto using always_laterN. Qed.
 
 (* True now *)
@@ -819,7 +743,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
 Proof.
   rewrite /uPred_except_0. apply (anti_symm _).
   - apply or_elim; last by auto.
-    by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
+    by rewrite -!or_intro_l -(always_pure true) -always_later -always_sep_dup'.
   - rewrite sep_or_r sep_elim_l sep_or_l; auto.
 Qed.
 Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
@@ -835,11 +759,9 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
-Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P.
+Lemma except_0_always c P : ◇ □{c} P ⊣⊢ □{c} ◇ P.
 Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed.
-Lemma except_0_plainly P : ◇ ☃ P ⊣⊢ ☃ ◇ P.
-Proof. by rewrite /uPred_except_0 plainly_or plainly_later plainly_pure. Qed.
-Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
+Lemma except_0_always_if c p P : ◇ □{c}?p P ⊣⊢ □{c}?p ◇ P.
 Proof. destruct p; simpl; auto using except_0_always. Qed.
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
@@ -858,10 +780,11 @@ 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 always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof. by rewrite -plainly_cmra_valid always_plainly. Qed.
+Lemma always_cmra_valid {A : cmraT} c (a : A) : □{c} ✓ a ⊣⊢ ✓ a.
+Proof.
+  apply (anti_symm _); auto using always_elim.
+  rewrite {1}always_cmra_valid_1'. destruct c; auto using always_mask_mono.
+Qed.
 
 (** * Derived rules *)
 Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
@@ -917,7 +840,7 @@ Proof.
   apply or_mono, wand_intro_l; first done.
   rewrite -{2}(löb Q); apply impl_intro_l.
   rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
-  rewrite -(always_pure) -always_later always_and_sep_l'.
+  rewrite -(always_pure true) -always_later always_and_sep_l'.
   by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
 Qed.
 Global Instance forall_timeless {A} (Ψ : A → uPred M) :
@@ -954,151 +877,92 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
   (∀ x, TimelessP (Ψ x)) → TimelessP P → TimelessP (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
-(* Derived lemmas for plainness *)
-Global Instance PlainP_proper : Proper ((≡) ==> iff) (@PlainP M).
-Proof. solve_proper. Qed.
-Global Instance limit_preserving_PlainP {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
-  NonExpansive Φ → LimitPreserving (λ x, PlainP (Φ x)).
-Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
-
-Lemma plain_persistent P : PlainP P → PersistentP P.
-Proof. rewrite /PlainP /PersistentP => HP. by rewrite {1}HP plainly_elim'. Qed.
-
-Lemma plainly_plainly P `{!PlainP P} : ☃ P ⊣⊢ P.
-Proof. apply (anti_symm (⊢)); eauto. Qed.
-Lemma plainly_intro P Q `{!PlainP P} : (P ⊢ Q) → P ⊢ ☃ Q.
-Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
-
-Lemma bupd_plain P `{!PlainP P} : (|==> P) ⊢ P.
-Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
-
 (* Derived lemmas for persistence *)
-Global Instance PersistentP_proper : Proper ((≡) ==> iff) (@PersistentP M).
+Global Instance PersistentP_proper c : Proper ((≡) ==> iff) (@PersistentP M c).
 Proof. solve_proper. Qed.
-Global Instance limit_preserving_PersistentP {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
-  NonExpansive Φ → LimitPreserving (λ x, PersistentP (Φ x)).
+Global Instance limit_preserving_PersistentP
+    {A:ofeT} `{Cofe A} c (Φ : A → uPred M) :
+  NonExpansive Φ → LimitPreserving (λ x, PersistentP c (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
+Lemma persistent_mask_weaken P : PersistentP false P → PersistentP true P.
+Proof. rewrite /PersistentP=> HP. by rewrite {1}HP always_mask_mono. Qed.
+
+Lemma always_always c P `{!PersistentP c P} : □{c} P ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
-Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
+Lemma always_if_always c p P `{!PersistentP c P} : □{c}?p P ⊣⊢ P.
 Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q.
-Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ∗ P.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
-Lemma always_impl_wand P `{!PersistentP P} Q : (P → Q) ⊣⊢ (P -∗ Q).
+Lemma always_intro c P Q `{!PersistentP c P} : (P ⊢ Q) → P ⊢ □{c} Q.
+Proof. rewrite -(always_always c P); apply always_intro'. Qed.
+Lemma always_and_sep_l P Q `{!PersistentP true P} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always true P) always_and_sep_l'. Qed.
+Lemma always_and_sep_r P Q `{!PersistentP true Q} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(always_always true Q) always_and_sep_r'. Qed.
+Lemma always_sep_dup P `{!PersistentP true P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(always_always true P) -always_sep_dup'. Qed.
+Lemma always_entails_l P Q `{!PersistentP true Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. by rewrite -(always_always true Q); apply always_entails_l'. Qed.
+Lemma always_entails_r P Q `{!PersistentP true Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. by rewrite -(always_always true Q); apply always_entails_r'. Qed.
+Lemma always_impl_wand P `{!PersistentP true P} Q : (P → Q) ⊣⊢ (P -∗ Q).
 Proof.
   apply (anti_symm _); auto using impl_wand.
   apply impl_intro_l. by rewrite always_and_sep_l wand_elim_r.
 Qed.
 
-(* Plain *)
-Global Instance pure_plain φ : PlainP (⌜φ⌝ : uPred M)%I.
-Proof. by rewrite /PlainP plainly_pure. Qed.
-Global Instance impl_plain P Q : PlainP P → PlainP Q → PlainP (P → Q).
-Proof.
-  rewrite /PlainP=> HP HQ.
-  by rewrite {2}HP -plainly_impl_plainly -HQ plainly_elim.
-Qed.
-Global Instance wand_plain P Q : PlainP P → PlainP Q → PlainP (P -∗ Q)%I.
-Proof.
-  rewrite /PlainP=> HP HQ.
-  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
-Qed.
-Global Instance plainly_plain P : PlainP (☃ P).
-Proof. by intros; apply plainly_intro'. Qed.
-Global Instance always_plain P : PlainP P → PlainP (□ P).
-Proof. rewrite /PlainP=> HP. by rewrite {1}HP always_plainly plainly_always. Qed.
-Global Instance and_plain P Q :
-  PlainP P → PlainP Q → PlainP (P ∧ Q).
-Proof. by intros; rewrite /PlainP plainly_and; apply and_mono. Qed.
-Global Instance or_plain P Q :
-  PlainP P → PlainP Q → PlainP (P ∨ Q).
-Proof. by intros; rewrite /PlainP plainly_or; apply or_mono. Qed.
-Global Instance sep_plain P Q :
-  PlainP P → PlainP Q → PlainP (P ∗ Q).
-Proof. by intros; rewrite /PlainP plainly_sep; apply sep_mono. Qed.
-Global Instance forall_plain {A} (Ψ : A → uPred M) :
-  (∀ x, PlainP (Ψ x)) → PlainP (∀ x, Ψ x).
-Proof. by intros; rewrite /PlainP plainly_forall; apply forall_mono. Qed.
-Global Instance exist_palin {A} (Ψ : A → uPred M) :
-  (∀ x, PlainP (Ψ x)) → PlainP (∃ x, Ψ x).
-Proof. by intros; rewrite /PlainP plainly_exist; apply exist_mono. Qed.
-Global Instance internal_eq_plain {A : ofeT} (a b : A) :
-  PlainP (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /PlainP plainly_internal_eq. Qed.
-Global Instance cmra_valid_plain {A : cmraT} (a : A) :
-  PlainP (✓ a : uPred M)%I.
-Proof. by intros; rewrite /PlainP; apply plainly_cmra_valid_1. Qed.
-Global Instance later_plain P : PlainP P → PlainP (▷ P).
-Proof. by intros; rewrite /PlainP plainly_later; apply later_mono. Qed.
-Global Instance except_0_plain P : PlainP P → PlainP (◇ P).
-Proof. by intros; rewrite /PlainP -except_0_plainly; apply except_0_mono. Qed.
-Global Instance laterN_plain n P : PlainP P → PlainP (▷^n P).
-Proof. induction n; apply _. Qed.
-Global Instance from_option_palin {A} P (Ψ : A → uPred M) (mx : option A) :
-  (∀ x, PlainP (Ψ x)) → PlainP P → PlainP (from_option Ψ P mx).
-Proof. destruct mx; apply _. Qed.
+Lemma bupd_persistent P `{!PersistentP false P} : (|==> P) ⊢ P.
+Proof. by rewrite -{1}(always_always false P) bupd_always. Qed.
 
 (* Persistence *)
-Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
+Global Instance pure_persistent c φ : PersistentP c (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
-Global Instance impl_persistent P Q :
-  PlainP P → PersistentP Q → PersistentP (P → Q).
+Global Instance impl_persistent c P Q :
+  PersistentP false P → PersistentP c Q → PersistentP c (P → Q).
 Proof.
-  rewrite /PlainP /PersistentP=> HP HQ.
-  rewrite {2}HP -always_impl_plainly. by rewrite -HQ plainly_elim.
+  rewrite /PersistentP=> HP HQ.
+  rewrite {2}HP -always_impl_always. by rewrite -HQ always_elim.
 Qed.
-Global Instance wand_persistent P Q :
-  PlainP P → PersistentP Q → PersistentP (P -∗ Q)%I.
+Global Instance wand_persistent c P Q :
+  PersistentP false P → PersistentP c Q → PersistentP c (P -∗ Q)%I.
 Proof.
-  rewrite /PlainP /PersistentP=> HP HQ.
-  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -always_impl_plainly -HQ.
+  rewrite /PersistentP=> HP HQ.
+  by rewrite {2}HP -{1}(always_elim false P) !wand_impl_always -always_impl_always -HQ.
 Qed.
-Global Instance plainly_persistent P : PersistentP (☃ P).
-Proof. by rewrite /PersistentP always_plainly. Qed.
-Global Instance always_persistent P : PersistentP (â–¡ P).
-Proof. by intros; apply always_intro'. Qed.
-Global Instance and_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∧ Q).
+Global Instance always_persistent c P : PersistentP c (â–¡{c} P).
+Proof. by apply always_intro'. Qed.
+Global Instance always_persistent' c P : PersistentP true (â–¡{c} P).
+Proof. by rewrite /PersistentP always_idemp'. Qed.
+Global Instance and_persistent c P Q :
+  PersistentP c P → PersistentP c Q → PersistentP c (P ∧ Q).
 Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
-Global Instance or_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∨ Q).
+Global Instance or_persistent c P Q :
+  PersistentP c P → PersistentP c Q → PersistentP c (P ∨ Q).
 Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
-Global Instance sep_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∗ Q).
+Global Instance sep_persistent c P Q :
+  PersistentP c P → PersistentP c Q → PersistentP c (P ∗ Q).
 Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
-Global Instance forall_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x).
+Global Instance forall_persistent {A} c (Ψ : A → uPred M) :
+  (∀ x, PersistentP c (Ψ x)) → PersistentP c (∀ x, Ψ x).
 Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
-Global Instance exist_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
+Global Instance exist_persistent {A} c (Ψ : A → uPred M) :
+  (∀ x, PersistentP c (Ψ x)) → PersistentP c (∃ x, Ψ x).
 Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
-Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
-  PersistentP (a ≡ b : uPred M)%I.
+Global Instance internal_eq_persistent {A : ofeT} c (a b : A) :
+  PersistentP c (a ≡ b : uPred M)%I.
 Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
-Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
-  PersistentP (✓ a : uPred M)%I.
+Global Instance cmra_valid_persistent {A : cmraT} c (a : A) :
+  PersistentP c (✓ a : uPred M)%I.
 Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
-Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
+Global Instance later_persistent c P : PersistentP c P → PersistentP c (▷ P).
 Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance except_0_persistent P : PersistentP P → PersistentP (◇ P).
+Global Instance except_0_persistent c P : PersistentP c P → PersistentP c (◇ P).
 Proof. by intros; rewrite /PersistentP -except_0_always; apply except_0_mono. Qed.
-Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P).
+Global Instance laterN_persistent c n P : PersistentP c P → PersistentP c (▷^n P).
 Proof. induction n; apply _. Qed.
-Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
+Global Instance ownM_persistent : Persistent a → PersistentP true (@uPred_ownM M a).
 Proof. intros. by rewrite /PersistentP always_ownM. Qed.
-Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx).
+Global Instance from_option_persistent {A} c P (Ψ : A → uPred M) (mx : option A) :
+  (∀ x, PersistentP c (Ψ x)) → PersistentP c P → PersistentP c (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
 (* For big ops *)
@@ -1109,14 +973,11 @@ Global Instance uPred_or_monoid : Monoid (@uPred_or M) :=
 Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
   {| monoid_unit := True%I |}.
 
-Global Instance uPred_always_and_homomorphism :
-  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always M).
+Global Instance uPred_always_and_homomorphism c :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always M c).
 Proof. split; [split; try apply _|]. apply always_and. apply always_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_always_if_and_homomorphism b :
-  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M b).
+Global Instance uPred_always_if_and_homomorphism c b :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M c b).
 Proof. split; [split; try apply _|]. apply always_if_and. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_later M).
@@ -1128,14 +989,11 @@ Global Instance uPred_except_0_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_except_0 M).
 Proof. split; [split; try apply _|]. apply except_0_and. apply except_0_True. Qed.
 
-Global Instance uPred_always_or_homomorphism :
-  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always M).
+Global Instance uPred_always_or_homomorphism c :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always M c).
 Proof. split; [split; try apply _|]. apply always_or. apply always_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_always_if_or_homomorphism b :
-  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M b).
+Global Instance uPred_always_if_or_homomorphism c b :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M c b).
 Proof. split; [split; try apply _|]. apply always_if_or. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_or_homomorphism :
   WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_later M).
@@ -1147,14 +1005,11 @@ 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.
 
-Global Instance uPred_always_sep_homomorphism :
-  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always M).
+Global Instance uPred_always_sep_homomorphism c :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always M c).
 Proof. split; [split; try apply _|]. apply always_sep. apply always_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_always_if_sep_homomorphism b :
-  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M b).
+Global Instance uPred_always_if_sep_homomorphism c b :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M c b).
 Proof. split; [split; try apply _|]. apply always_if_sep. apply always_if_pure. Qed.
 Global Instance uPred_later_monoid_sep_homomorphism :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_later M).
@@ -1171,11 +1026,11 @@ 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
+(* When declared as an actual instance, [persistent_mask_weaken] 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.
+Hint Immediate uPred.persistent_mask_weaken : typeclass_instances.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index a46400ae92ae9902edfae933fc43ff3a7794bc90..67b9ac7dc56461a8ca52c20e9353bb4dec440090 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -32,7 +32,8 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance auth_own_timeless a : TimelessP (auth_own a).
   Proof. apply _. Qed.
-  Global Instance auth_own_persistent a : Persistent a → PersistentP (auth_own a).
+  Global Instance auth_own_persistent a :
+    Persistent a → PersistentP true (auth_own a).
   Proof. apply _. Qed.
 
   Global Instance auth_inv_ne n :
@@ -51,7 +52,7 @@ Section definitions.
     Proper (pointwise_relation T (≡) ==>
             pointwise_relation T (⊣⊢) ==> (⊣⊢)) (auth_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance auth_ctx_persistent N f φ : PersistentP (auth_ctx N f φ).
+  Global Instance auth_ctx_persistent N f φ : PersistentP true (auth_ctx N f φ).
   Proof. apply _. Qed.
 End definitions.
 
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index d41ce60ff2f750f90afde12af1669fafced0e07a..4a3091b1bda2041e4739681e6f396769c106dce4 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -65,7 +65,7 @@ Proof. solve_contractive. Qed.
 Global Instance slice_proper γ : Proper ((≡) ==> (≡)) (slice N γ).
 Proof. apply ne_proper, _. Qed.
 
-Global Instance slice_persistent γ P : PersistentP (slice N γ P).
+Global Instance slice_persistent γ P : PersistentP true (slice N γ P).
 Proof. apply _. Qed.
 
 Global Instance box_contractive f : Contractive (box N f).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 83e3629d72766bd9640ffc8fa96ec5f6dbd5c8a2..7fda48d80c83a3a60a4725cd77e1bcd71aa17c81 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -34,7 +34,7 @@ Section proofs.
   Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ).
   Proof. exact: ne_proper. Qed.
 
-  Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P).
+  Global Instance cinv_persistent N γ P : PersistentP true (cinv N γ P).
   Proof. rewrite /cinv; apply _. Qed.
 
   Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 5419422c20de68a71195466427376a82c9613824..1c13517107c4afe6701861936fbea8a5173c1928 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -5,7 +5,7 @@ Import uPred.
 
 (** The "core" of an assertion is its maximal persistent part. *)
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ Q, ☃ (Q → □ Q) → ☃ (P → Q) → Q)%I.
+  (∀ Q, □{false} (Q → □ Q) → □{false} (P → Q) → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -16,12 +16,12 @@ Section core.
   Lemma coreP_intro P : P -∗ coreP P.
   Proof. iIntros "HP". iIntros (Q) "_ HPQ". by iApply "HPQ". Qed.
 
-  Global Instance coreP_persistent P : PersistentP (coreP P).
+  Global Instance coreP_persistent P : PersistentP true (coreP P).
   Proof.
     rewrite /coreP /PersistentP. iIntros "HC".
     iApply always_forall. iIntros (Q). (* FIXME: iIntros should apply always_forall automatically. *)
-    iApply always_impl_plainly. iIntros "#HQ".
-    iApply always_impl_plainly. iIntros "#HPQ".
+    iApply always_impl_always. iIntros "#HQ".
+    iApply always_impl_always. iIntros "#HPQ".
     iApply "HQ". iApply "HC"; done.
   Qed.
 
@@ -36,7 +36,7 @@ Section core.
     iApply ("H" $! Q with "[]"); first done. by rewrite HP.
   Qed.
 
-  Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
+  Lemma coreP_elim P : PersistentP true P → coreP P -∗ P.
   Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
 
   Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
@@ -45,6 +45,6 @@ Section core.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
       iAlways. by iApply HP.
     - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
-      iDestruct (coreP_elim with "HcQ") as "#HQ". done.
+      iApply (coreP_elim with "HcQ").
   Qed.
 End core.
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index 6a303b19a557f6e760e0123675a79f6809338c79..8975da9cb84b550a60d64c52a6f7ded468431f0e 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -12,7 +12,7 @@ Module savedprop. Section savedprop.
 
   (** Saved Propositions and the update modality *)
   Context (sprop : Type) (saved : sprop → iProp → iProp).
-  Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
+  Hypothesis sprop_persistent : ∀ i P, PersistentP true (saved i P).
   Hypothesis sprop_alloc_dep :
     ∀ (P : sprop → iProp), (|==> (∃ i, saved i (P i)))%I.
   Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).
@@ -67,7 +67,7 @@ Module inv. Section inv.
 
   (** We have invariants *)
   Context (name : Type) (inv : name → iProp → iProp).
-  Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P).
+  Hypothesis inv_persistent : ∀ i P, PersistentP true (inv i P).
   Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
   Hypothesis inv_open :
     ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R).
@@ -130,7 +130,7 @@ Module inv. Section inv.
   (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
   Definition saved (γ : gname) (P : iProp) : iProp :=
     ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
-  Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
+  Global Instance saved_persistent γ P : PersistentP true (saved γ P) := _.
 
   Lemma saved_alloc (P : gname → iProp) : fupd M1 (∃ γ, saved γ (P γ)).
   Proof.
@@ -163,7 +163,7 @@ Module inv. Section inv.
   (** And now we tie a bad knot. *)
   Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope.
   Definition A i : iProp := ∃ P, ¬P ∗ saved i P.
-  Global Instance A_persistent i : PersistentP (A i) := _.
+  Global Instance A_persistent i : PersistentP true (A i) := _.
 
   Lemma A_alloc : fupd M1 (∃ i, saved i (A i)).
   Proof. by apply saved_alloc. Qed.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 9e707ab9b6be5e5fbf5325b994c48bbe972a5c75..da372ddd1c314b6e58bdbc7b2015a8c9d49dabdf 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -141,7 +141,7 @@ Proof.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
 Qed.
 
-Lemma fupd_plain' {E1 E2 E2'} P Q `{!PlainP P} :
+Lemma fupd_persistent' {E1 E2 E2'} P Q `{!PersistentP false P} :
   E1 ⊆ E2 →
   (Q ={E1, E2'}=∗ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
 Proof.
@@ -153,27 +153,27 @@ Proof.
   iMod "H" as "(Hws & HE2 & HQ)".
   rewrite ownE_op; trivial; iDestruct "HE2" as "[HE1 HE3]".
   iAssert (â—‡ P)%I with "[HQ Hws HE1]" as "#HP".
-  { iApply bupd_plain; eauto.
+  { iApply bupd_persistent; eauto.
     by iMod ("HQP" with "HQ [$]") as "[_ [_ HP]]". }
   iModIntro. iMod "HP".
   iModIntro; iFrame; auto.
 Qed.
 
-Lemma fupd_plain {E1 E2} P Q `{!PlainP P} :
+Lemma fupd_plain {E1 E2} P Q `{!PersistentP false P} :
   E1 ⊆ E2 → (Q ⊢ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
 Proof.
   iIntros (HE HQP) "HQ".
-  iApply (fupd_plain' with "HQ"); auto.
+  iApply (fupd_persistent' with "HQ"); auto.
   by iIntros "?"; iApply fupd_intro; iApply HQP.
 Qed.
 
-Lemma later_fupd_plain {E} P `{Hpl: !PlainP P} :
+Lemma later_fupd_plain {E} P `{Hpl: !PersistentP false P} :
   (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
 Proof.
   iIntros "HP". rewrite fupd_eq /fupd_def.
   iIntros "[Hs He]".
   iAssert (â–· â—‡ P)%I with "[-]" as "#HP'".
-  { iNext. iApply bupd_plain; eauto.
+  { iNext. iApply bupd_persistent; eauto.
     iMod ("HP" with "[$]") as "HP".
     iModIntro. iMod "HP" as "(_&_&HP)". by iModIntro. }
   by iFrame.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index fc505d702d42d078b694c975f12bee859205abb2..bf27ce2fae0ba2a4cbe6aadc17f09c888525c8fb 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -13,7 +13,7 @@ Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
 
 Context (vs_ne : ∀ E1 E2, NonExpansive2 (vs E1 E2)).
-Context (vs_persistent : ∀ E1 E2 P Q, PersistentP (P ={E1,E2}=> Q)).
+Context (vs_persistent : ∀ E1 E2 P Q, PersistentP true (P ={E1,E2}=> Q)).
 
 Context (vs_impl : ∀ E P Q, □ (P → Q) ⊢ P ={E,E}=> Q).
 Context (vs_transitive : ∀ E1 E2 E3 P Q R,
@@ -24,7 +24,7 @@ Context (vs_frame_r : ∀ E1 E2 P Q R, (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q
 Context (vs_exists : ∀ {A} E1 E2 (Φ : A → uPred M) Q,
   (∀ x, Φ x ={E1,E2}=> Q) ⊢ (∃ x, Φ x) ={E1,E2}=> Q).
 Context (vs_persistent_intro_r : ∀ E1 E2 P Q R,
-  PersistentP R →
+  PersistentP true R →
   (R -∗ (P ={E1,E2}=> Q)) ⊢ P ∗ R ={E1,E2}=> Q).
 
 Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index a94ea6989ed1ee7caf9790a6215928d8e3c639f7..6bcc01f705df827e2f924722b81df6ce256ec3a1 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -50,7 +50,7 @@ Section fractional.
 
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
-    PersistentP P → Fractional (λ _, P).
+    PersistentP true P → Fractional (λ _, P).
   Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index cadd0c88d42f1754a537136758a73a681f743336..664494284a5595c1430e800ca8fd4a35ee6bd56b 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -31,7 +31,7 @@ Proof. apply contractive_ne, _. Qed.
 Global Instance inv_Proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N).
 Proof. apply ne_proper, _. Qed.
 
-Global Instance inv_persistent N P : PersistentP (inv N P).
+Global Instance inv_persistent N P : PersistentP true (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
 Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset).
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 2f20a514e2d7996ba685afc4e3af319c62b73422..d477ea58d88f270f45d653a06e775ea7060c8ce6 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -40,7 +40,7 @@ Section proofs.
   Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
   Proof. apply (ne_proper _). Qed.
 
-  Global Instance na_inv_persistent p N P : PersistentP (na_inv p N P).
+  Global Instance na_inv_persistent p N P : PersistentP true (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
   Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 4049d8dc2546c66cab4e488db1e7ee1b769e2bab..7c456426079c4b00be3dd12ee9a9f5bc06a2b4ce 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -108,7 +108,7 @@ Proof. by rewrite comm -own_valid_r. Qed.
 
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
-Global Instance own_core_persistent γ a : Persistent a → PersistentP (own γ a).
+Global Instance own_core_persistent γ a : Persistent a → PersistentP true (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 
 (** ** Allocation *)
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 4002d1d821aedea8544a46a4bf9a2b83ba274531..04d85dbf394cf6bf92e1ddd6edb0918282b03ac6 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -23,7 +23,8 @@ Section saved_prop.
   Implicit Types x y : F (iProp Σ).
   Implicit Types γ : gname.
 
-  Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
+  Global Instance saved_prop_persistent γ x :
+    PersistentP true (saved_prop_own γ x).
   Proof. rewrite /saved_prop_own; apply _. Qed.
 
   Lemma saved_prop_alloc_strong x (G : gset gname) :
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 047d10d32b0ebab956aa04ea9138683e9be6deb8..9d7fde93cdd828baeedef1c3c94a61fa859b14b0 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -43,11 +43,11 @@ Section definitions.
   Global Instance sts_ctx_proper `{!invG Σ} N :
     Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ).
+  Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP true (sts_ctx N φ).
   Proof. apply _. Qed.
-  Global Instance sts_own_persistent s : PersistentP (sts_own s ∅).
+  Global Instance sts_own_persistent s : PersistentP true (sts_own s ∅).
   Proof. apply _. Qed.
-  Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ∅).
+  Global Instance sts_ownS_persistent S : PersistentP true (sts_ownS S ∅).
   Proof. apply _. Qed.
 End definitions.
 
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 3d658b58ff4a576d1ace6dd5153e46a076bfb069..dfe5c6b2b6e9419e874aa076f4b6ca0c1d513731 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -49,7 +49,7 @@ Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
 Proof. solve_contractive. Qed.
 Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
 Proof. solve_contractive. Qed.
-Global Instance ownI_persistent i P : PersistentP (ownI i P).
+Global Instance ownI_persistent i P : PersistentP true (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
 Lemma ownE_empty : (|==> ownE ∅)%I.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 00389a413f29e736e66768af539f0da355794e71..d11139da7d34b3425c2dfed89beeafdff66183c8 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -97,20 +97,15 @@ 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_always_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n (core x) |}.
+Program Definition uPred_always_def {M} (c : bool) (P : uPred M) : uPred M :=
+  {| uPred_holds n x := P n (if c then core x else ε) |}.
 Next Obligation.
-  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
+  intros M []; naive_solver eauto using uPred_mono, @cmra_core_monoN.
+Qed.
+Next Obligation.
+  intros M []; naive_solver eauto using uPred_closed,
+    @cmra_core_validN, ucmra_unit_validN.
 Qed.
-Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
 Definition uPred_always_aux : seal (@uPred_always_def). by eexists. Qed.
 Definition uPred_always {M} := unseal uPred_always_aux M.
 Definition uPred_always_eq :
@@ -184,10 +179,12 @@ 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_always P)
+Notation "â–¡{ c } P" := (uPred_always c P)
+  (at level 20, c at next level, right associativity, format "â–¡{ c }  P") : uPred_scope.
+
+Notation "â–¡ P" := (â–¡{true} P)%I
   (at level 20, right associativity) : uPred_scope.
+
 Notation "â–· P" := (uPred_later P)
   (at level 20, right associativity) : uPred_scope.
 Infix "≡" := uPred_internal_eq : uPred_scope.
@@ -209,7 +206,7 @@ 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_plainly_eq, uPred_always_eq, uPred_later_eq, uPred_ownM_eq,
+  uPred_always_eq, uPred_later_eq, uPred_ownM_eq,
   uPred_cmra_valid_eq, uPred_bupd_eq).
 Ltac unseal := rewrite !unseal_eqs /=.
 
@@ -306,20 +303,14 @@ 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 always_ne : NonExpansive (@uPred_always M).
+Global Instance always_ne c : NonExpansive (@uPred_always M c).
 Proof.
   intros n P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
+  unseal; split=> n' x; split; apply HP; destruct c;
+    eauto using @cmra_core_validN, @ucmra_unit_validN.
 Qed.
-Global Instance always_proper :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
+Global Instance always_proper c :
+  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M c) := ne_proper _.
 Global Instance ownM_ne : NonExpansive (@uPred_ownM M).
 Proof.
   intros n a b Ha.
@@ -439,59 +430,46 @@ Proof.
   eapply HPQR; eauto using cmra_validN_op_l.
 Qed.
 
-(* The plain 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.
+(* The always modality *)
+Lemma always_mono c P Q : (P ⊢ Q) → □{c} P ⊢ □{c} Q.
 Proof.
-  unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
-    split; eapply HPQ; eauto using @ucmra_unit_least.
+  intros HP; unseal; split=> n x ? /=.
+  apply HP; destruct c; auto using ucmra_unit_validN, cmra_core_validN.
 Qed.
-
-(* Always *)
-Lemma always_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
-Lemma always_elim P : □ P ⊢ P.
+Lemma always_mask_mono P : □{false} P ⊢ □ P.
+Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
+Lemma always_elim' P : □ P ⊢ P.
 Proof.
   unseal; split=> n x ? /=.
   eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
 Qed.
-Lemma always_idemp_2 P : □ P ⊢ □ □ P.
-Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
+Lemma always_idemp_2 c P : □{c} P ⊢ □{c} □{c} P.
+Proof. unseal; split=> n x ?? //=. destruct c; by rewrite ?cmra_core_idemp. Qed.
 
-Lemma always_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+Lemma always_forall_2 {A} c (Ψ : A → uPred M) : (∀ a, □{c} Ψ a) ⊢ (□{c} ∀ a, Ψ a).
 Proof. by unseal. Qed.
-Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
+Lemma always_exist_1 {A} c (Ψ : A → uPred M) : (□{c} ∃ a, Ψ a) ⊢ (∃ a, □{c} Ψ a).
 Proof. by unseal. Qed.
 
-Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma prop_ext P Q : □{false} ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
 Proof.
-  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
-  by rewrite cmra_core_l cmra_core_idemp.
+  unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
+    split; eapply HPQ; eauto using @ucmra_unit_least.
 Qed.
 
-Lemma always_impl_plainly P Q : (☃ P → □ Q) ⊢ □ (☃ P → Q).
+Lemma always_and_sep_l_1' P Q : □{true} P ∧ Q ⊢ □{true} 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.
+  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
+  by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 
-Lemma plainly_impl_plainly P Q : (☃ P → ☃ Q) ⊢ ☃ (☃ P → Q).
+Lemma always_impl_always c P Q : (□{false} P → □{c} Q) ⊢ □{c} (□{false} 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.
+  unseal; split=> /= n x ? HPQ n' x' ????. destruct c.
+  - eapply uPred_mono with (core x), cmra_included_includedN; auto.
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  - eapply uPred_mono with ε, cmra_included_includedN; auto.
+    apply (HPQ n' x); eauto using cmra_validN_le.
 Qed.
 
 (* Later *)
@@ -526,9 +504,7 @@ Proof.
   intros [|n'] x' ????; [|done].
   eauto using uPred_closed, uPred_mono, cmra_included_includedN.
 Qed.
-Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
-Proof. by unseal. Qed.
-Lemma plainly_later P : ☃ ▷ P ⊣⊢ ▷ ☃ P.
+Lemma always_later c P : □{c} ▷ P ⊣⊢ ▷ □{c} P.
 Proof. by unseal. Qed.
 
 (* Own *)
@@ -565,7 +541,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 plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ☃ ✓ a.
+Lemma always_cmra_valid_1' {A : cmraT} (a : A) : ✓ a ⊢ □{false} ✓ 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.
@@ -602,7 +578,7 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma bupd_plainly P : (|==> ☃ P) ⊢ P.
+Lemma bupd_always P : (|==> □{false} P) ⊢ P.
 Proof.
   unseal; split => n x Hnx /= Hng.
   destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 79112c3fa39170854b808dce42c4a1716a7219fd..b2ff000533fb4ce226459059afe1f2e66ade0800 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -29,7 +29,7 @@ Section mono_proof.
     (∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
 
   (** The main proofs. *)
-  Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
+  Global Instance mcounter_persistent l n : PersistentP true (mcounter l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_mono_spec :
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 720dcc19aa4af6c4696ed456ae0167c6f797ac7d..d2f345218d428f21fec494a19b830bfd0ee4f72c 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -14,7 +14,7 @@ Structure lock Σ `{!heapG Σ} := Lock {
   locked (γ: name) : iProp Σ;
   (* -- general properties -- *)
   is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
-  is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
+  is_lock_persistent N γ lk R : PersistentP true (is_lock N γ lk R);
   locked_timeless γ : TimelessP (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (* -- operation specs -- *)
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index ea19cf82af00a0507f3083c814050663cb65fbd0..ce0a2c556758578c227f8174618e0d85af51a42c 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -40,7 +40,7 @@ Section proof.
   Proof. solve_proper. Qed.
 
   (** The main proofs. *)
-  Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
+  Global Instance is_lock_persistent γ l R : PersistentP true (is_lock γ l R).
   Proof. apply _. Qed.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index a926ab2ba42803fb19cc42edbc9e6dd626a1dc82..672ccddc5fa90ac1031048b012d85dc98a3d2967 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -59,7 +59,7 @@ Section proof.
   Proof. solve_proper. Qed.
   Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_persistent γ lk R : PersistentP (is_lock γ lk R).
+  Global Instance is_lock_persistent γ lk R : PersistentP true (is_lock γ lk R).
   Proof. apply _. Qed.
   Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 7dc6fbe67983693e41a30e3a9dc33c1178383471..af281424dd8e720e57fc79b17f097c3a877d1475 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -106,10 +106,10 @@ Proof.
   iModIntro; iNext; iMod "H" as ">?". by iApply IH.
 Qed.
 
-Lemma bupd_iter_laterN_mono n P Q `{!PlainP Q} :
+Lemma bupd_iter_laterN_mono n P Q `{!PersistentP false 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.
+  intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_persistent.
 Qed.
 
 Lemma bupd_iter_frame_l n R Q :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 7c2e779804b379c530579dc25d30f5af53c8f720..da52c78ca671dbbe954bfda1830c8b14eccd935a 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -19,11 +19,8 @@ Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. 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_always_l p P Q :
-  FromAssumption p P Q → FromAssumption p (□ P) Q.
+Global Instance from_assumption_always_l p c P Q :
+  FromAssumption p P Q → FromAssumption p (□{c} P) Q.
 Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
 Global Instance from_assumption_later p P Q :
   FromAssumption p P Q → FromAssumption p P (▷ Q)%I.
@@ -51,9 +48,7 @@ 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_always P φ : IntoPure P φ → IntoPure (□ P) φ.
+Global Instance into_pure_always c P φ : IntoPure P φ → IntoPure (□{c} P) φ.
 Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
 
 Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
@@ -102,9 +97,7 @@ 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_always P φ : FromPure P φ → FromPure (□ P) φ.
+Global Instance from_pure_always c P φ : FromPure P φ → FromPure (□{c} P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite always_pure. Qed.
 Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
 Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
@@ -153,15 +146,9 @@ Proof. rewrite /IntoPersistentP /==> ->. by rewrite always_if_always. Qed.
 Global Instance into_persistentP_always P : IntoPersistentP true P P | 1.
 Proof. done. Qed.
 Global Instance into_persistentP_persistent P :
-  PersistentP P → IntoPersistentP false P P | 100.
+  PersistentP true P → IntoPersistentP false P P | 100.
 Proof. done. Qed.
 
-(* FromPersistentP *)
-Global Instance from_persistentP_always P : FromPersistentP false (â–¡ P) P.
-Proof. by rewrite /FromPersistentP. Qed.
-Global Instance from_persistentP_plainly P : FromPersistentP true (☃ P) P.
-Proof. by rewrite /FromPersistentP. Qed.
-
 (* IntoLater *)
 Global Instance into_laterN_later n P Q :
   IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.
@@ -271,11 +258,8 @@ 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_always n P Q :
-  FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
+Global Instance from_later_always n c P Q :
+  FromLaterN n P Q → FromLaterN n (□{c} P) (□{c} Q).
 Proof. by rewrite /FromLaterN -always_laterN=> ->. Qed.
 
 Global Instance from_later_forall {A} n (Φ Ψ : A → uPred M) :
@@ -326,11 +310,8 @@ Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. 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_always p R P Q :
-  IntoWand p R P Q → IntoWand p (□ R) P Q.
+Global Instance into_wand_always p c R P Q :
+  IntoWand p R P Q → IntoWand p (□{c} R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
 
 Global Instance into_wand_later p R P Q :
@@ -358,22 +339,16 @@ Proof. by apply mk_from_and_and. Qed.
 Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100.
 Proof. done. Qed.
 Global Instance from_and_sep_persistent_l P1 P2 :
-  PersistentP P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
+  PersistentP true P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
 Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
-  PersistentP P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
+  PersistentP true P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
 Proof. intros. by rewrite /FromAnd always_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_always p P Q1 Q2 :
-  FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
+Global Instance from_and_always p c P Q1 Q2 :
+  FromAnd false P Q1 Q2 → FromAnd p (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof.
   intros. apply mk_from_and_and.
   by rewrite always_and_sep_l' -always_sep -(from_and _ P).
@@ -410,7 +385,7 @@ Global Instance from_and_big_sepL_cons {A} (Φ : nat → A → uPred M) x l :
   FromAnd false ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
 Proof. by rewrite /FromAnd big_sepL_cons. Qed.
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l :
-  PersistentP (Φ 0 x) →
+  PersistentP true (Φ 0 x) →
   FromAnd true ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
 Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.
 
@@ -419,7 +394,7 @@ Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. by rewrite /FromAnd big_opL_app. Qed.
 Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M) l1 l2 :
-  (∀ k y, PersistentP (Φ k y)) →
+  (∀ k y, PersistentP true (Φ k y)) →
   FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
@@ -455,21 +430,16 @@ Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) ownM_op. Qed.
 Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q.
 Proof. done. Qed.
 Global Instance into_and_and_persistent_l P Q :
-  PersistentP P → IntoAnd false (P ∧ Q) P Q.
+  PersistentP true P → IntoAnd false (P ∧ Q) P Q.
 Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed.
 Global Instance into_and_and_persistent_r P Q :
-  PersistentP Q → IntoAnd false (P ∧ Q) P Q.
+  PersistentP true Q → IntoAnd false (P ∧ Q) P Q.
 Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_into_and_sep. by rewrite pure_and always_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 always_and_sep_r.
-Qed.
-Global Instance into_and_always p P Q1 Q2 :
-  IntoAnd true P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
+Global Instance into_and_always p c P Q1 Q2 :
+  IntoAnd true P Q1 Q2 → IntoAnd p (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof.
   rewrite /IntoAnd=>->. destruct p; by rewrite ?always_and always_and_sep_r.
 Qed.
@@ -653,11 +623,8 @@ 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_always P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
+Global Instance from_or_always c P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
@@ -674,11 +641,8 @@ 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_always P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
+Global Instance into_or_always c P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (□{c} P) (□{c} Q1) (□{c} Q2).
 Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
 Global Instance into_or_later P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
@@ -701,11 +665,8 @@ 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_always {A} P (Φ : A → uPred M) :
-  FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
+Global Instance from_exist_always {A} c P (Φ : A → uPred M) :
+  FromExist P Φ → FromExist (□{c} P) (λ a, □{c} (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite always_exist. Qed.
 Global Instance from_exist_later {A} P (Φ : A → uPred M) :
   FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -727,11 +688,8 @@ Proof. done. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. 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_always {A} P (Φ : A → uPred M) :
-  IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
+Global Instance into_exist_always {A} c P (Φ : A → uPred M) :
+  IntoExist P Φ → IntoExist (□{c} P) (λ a, □{c} (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
 Global Instance into_exist_later {A} P (Φ : A → uPred M) :
   IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
@@ -746,11 +704,8 @@ 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_always {A} P (Φ : A → uPred M) :
-  IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
+Global Instance into_forall_always {A} c P (Φ : A → uPred M) :
+  IntoForall P Φ → IntoForall (□{c} P) (λ a, □{c} (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
 
 (* FromModal *)
@@ -774,20 +729,19 @@ 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_always P Q : ElimModal (â–¡ P) P Q Q.
+Global Instance elim_modal_always c P Q : ElimModal (â–¡{c} P) P Q Q.
 Proof. intros. by rewrite /ElimModal always_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 : PlainP 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_goal P Q :
+  PersistentP false Q → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_persistent. Qed.
 
-Global Instance elim_modal_bupd_plain P Q : PlainP P → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+Global Instance elim_modal_bupd_plain P Q :
+  PersistentP false P → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_persistent wand_elim_r. Qed.
 
 Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
 Proof.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 80a5bc02433c7ca676caa9c56383a9f9d81d353c..c9bbe4f26109788a4a7e5f1b7205faa0e4627c75 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -32,11 +32,6 @@ Class IntoPersistentP {M} (p : bool) (P Q : uPred M) :=
 Arguments into_persistentP {_} _ _ _ {_}.
 Hint Mode IntoPersistentP + + ! - : typeclass_instances.
 
-Class FromPersistentP {M} (p : bool) (P Q : uPred M) :=
-  from_persistentP : (if p then ☃ Q else □ Q) ⊢ P.
-Arguments from_persistentP {_} _ _ _ {_}.
-Hint Mode FromPersistentP + - ! - : typeclass_instances.
-
 (* The class [IntoLaterN] has only two instances:
 
 - The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
@@ -100,7 +95,8 @@ Lemma mk_from_and_and {M} p (P Q1 Q2 : uPred M) :
   (Q1 ∧ Q2 ⊢ P) → FromAnd p P Q1 Q2.
 Proof. rewrite /FromAnd=><-. destruct p; auto using sep_and. Qed.
 Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
-  Or (PersistentP Q1) (PersistentP Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
+  Or (PersistentP true Q1) (PersistentP true Q2) →
+  (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
 Proof.
   intros [?|?] ?; rewrite /FromAnd.
   - by rewrite always_and_sep_l.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index bd1a3962cc937aaf393c44c03332111837dfbdcf..430f0fd0457d38cb1986b151e9d3d231c738b1fe 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -189,8 +189,8 @@ Proof.
   destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
   rewrite always_if_sep -assoc. destruct q1; simpl.
   - destruct rp.
-    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (always_elim_if q2).
-    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (always_elim_if q2).
+    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (always_elim_if _ q2).
+    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (always_elim_if _ q2).
   - rewrite envs_lookup_sound // IH //; simpl. by rewrite always_if_elim.
 Qed.
 
@@ -302,7 +302,7 @@ Proof.
 Qed.
 
 Lemma env_spatial_is_nil_persistent Δ :
-  env_spatial_is_nil Δ = true → PersistentP Δ.
+  env_spatial_is_nil Δ = true → PersistentP true Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
 Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
 
@@ -467,8 +467,8 @@ Lemma tac_löb Δ Δ' i Q :
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ?? HQ. rewrite -(always_elim Q) -(löb (□ Q)) -always_later.
-  apply impl_intro_l, (always_intro _ _).
+  intros ?? HQ. rewrite -(always_elim true Q) -(löb (□ Q)) -always_later.
+  apply impl_intro_l, (always_intro _ _ _).
   rewrite envs_app_sound //; simpl.
   by rewrite right_id always_and_sep_l' wand_elim_r HQ.
 Qed.
@@ -476,56 +476,53 @@ Qed.
 (** * Always *)
 Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
   into_plain_env_subenv : env_subenv Γ2 Γ1;
-  into_plain_env_plain : PlainP ([∗] Γ2);
+  into_plain_env_plain : PersistentP false ([∗] Γ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;
+    if p then env_persistent Δ1 = env_persistent Δ2
+    else IntoPlainEnv (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 :
-  PlainP P → IntoPlainEnv Γ1 Γ2 →
+  PersistentP false 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).
+Global Instance into_persistent_envs_true Γp Γs :
+  IntoPersistentEnvs true (Envs Γp Γs) (Envs Γp Enil).
 Proof. by split. Qed.
-Global Instance into_persistent_envs_true Γp1 Γp2 Γs1 :
+Global Instance into_persistent_envs_false Γp1 Γp2 Γs1 :
   IntoPlainEnv Γp1 Γp2 →
-  IntoPersistentEnvs true (Envs Γp1 Γs1) (Envs Γp2 Enil).
+  IntoPersistentEnvs false (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).
+Lemma into_persistent_envs_sound c Δ1 Δ2 :
+  IntoPersistentEnvs c Δ1 Δ2 → Δ1 ⊢ □{c} Δ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|].
+  apply pure_elim_sep_l=> Hwf /=.
+  rewrite sep_elim_l right_id always_sep always_pure. destruct c; simplify_eq/=.
+  - apply sep_intro_True_l; [apply pure_intro|].
+    destruct Hwf; constructor; simpl; eauto using Enil_wf.
+    by rewrite always_idemp.
+  - destruct Hp. apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; eauto using Enil_wf, env_subenv_wf.
-    + rewrite always_elim plainly_always plainly_plainly.
+    + rewrite always_idemp'' -(always_idemp' false) (always_always false).
+      apply always_mono.
       by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
-  - rewrite right_id always_sep always_pure.
-    apply sep_intro_True_l; [apply pure_intro|by rewrite always_always].
-    destruct Hwf; constructor; simpl; eauto using Enil_wf.
 Qed.
 
-Lemma tac_always_intro Δ Δ' p Q Q' :
-  FromPersistentP p Q' Q →
-  IntoPersistentEnvs p Δ Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q'.
-Proof.
-  intros ?? HQ. rewrite into_persistent_envs_sound -(from_persistentP _ Q').
-  destruct p; auto using always_mono, plainly_mono.
-Qed.
+Lemma tac_always_intro Δ Δ' c Q :
+  IntoPersistentEnvs c Δ Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ □{c} Q.
+Proof. intros ? <-. by rewrite into_persistent_envs_sound. Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
@@ -539,12 +536,12 @@ Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  (if env_spatial_is_nil Δ then TCTrue else PersistentP P) →
+  (if env_spatial_is_nil Δ then TCTrue else PersistentP true P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
-  - rewrite (persistentP Δ) envs_app_sound //; simpl.
+  - rewrite (persistentP true Δ) envs_app_sound //; simpl.
     by rewrite right_id always_wand_impl always_elim.
   - apply impl_intro_l. rewrite envs_app_sound //; simpl.
     by rewrite always_and_sep_l right_id wand_elim_r.
@@ -660,22 +657,22 @@ Qed.
 
 Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  IntoWand false R P1 P2 → PersistentP P1 →
+  IntoWand false R P1 P2 → PersistentP true P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
   (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite envs_lookup_sound //.
   rewrite -(idemp uPred_and (envs_delete _ _ _)).
-  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+  rewrite {1}HP1 (persistentP _ P1) always_and_sep_l assoc.
   rewrite envs_simple_replace_sound' //; simpl.
-  rewrite right_id (into_wand _ R) (always_elim_if q) -always_if_sep wand_elim_l.
+  rewrite right_id (into_wand _ R) (always_elim_if _ q) -always_if_sep wand_elim_l.
   by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
   envs_lookup j Δ = Some (q,P) →
-  (Δ ⊢ R) → PersistentP R →
+  (Δ ⊢ R) → PersistentP true R →
   envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
@@ -711,7 +708,7 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   (of_envs Δ ⊢ Q).
 Proof.
   rewrite /IntoIH. intros HP ? HPQ.
-  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP // HPQ impl_elim_r.
+  by rewrite -(idemp uPred_and Δ) {1}(persistentP true Δ) {1}HP // HPQ impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
@@ -728,7 +725,7 @@ Qed.
 Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ = Some Δ' →
-  PersistentP P →
+  PersistentP true P →
   (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ded60303287f340ed936fee5e64cc4f093c0f508..0797a5fa49522d7d4c8a17f5c595d58c27177d87 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -808,10 +808,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  eapply tac_always_intro;
-    [apply _ || fail "iAlways: the goal is not an always modality"
-    |env_cbv; apply _
-    |].
+  eapply tac_always_intro; [env_cbv; apply _|]
+    || fail "iAlways: the goal is not an always modality".
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1722,8 +1720,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 _ ⊢ □ _) => iAlways.
-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.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 5896d63912131dc0e63bc5e214243e58859f496c..7d6166fc21b0833e8d29b2af48442f18ca9dfd21 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -191,7 +191,7 @@ Section counter_proof.
     (∃ N γ, inv N (I γ l) ∧ own γ (Frag n))%I.
 
   (** The main proofs. *)
-  Global Instance C_persistent l n : PersistentP (C l n).
+  Global Instance C_persistent l n : PersistentP true (C l n).
   Proof. apply _. Qed.
 
   Lemma newcounter_spec :
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 28e6152235d7fe8621d91f05e44915c1cf811b57..686b10eef40facb5eaf373feedc87ba69ffdb306 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -78,7 +78,7 @@ Proof.
   done.
 Qed.
 
-Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
+Lemma test_iIntros_persistent P Q `{!PersistentP true Q} : (P → Q → P ∗ Q)%I.
 Proof. iIntros "H1 H2". by iFrame. Qed.
 
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
@@ -142,11 +142,11 @@ Proof.
   iSpecialize ("H" $! _ [#10]). done.
 Qed.
 
-Lemma test_eauto_iFramE P Q R `{!PersistentP R} :
+Lemma test_eauto_iFramE P Q R `{!PersistentP true R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. eauto with iFrame. Qed.
 
-Lemma test_iCombine_persistent P Q R `{!PersistentP R} :
+Lemma test_iCombine_persistent P Q R `{!PersistentP true R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.