diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index f04722cf0c44235d30c24a4395ee34212fef7b8d..c7fb6c7523829111ddb239000dd5ad38aef27449 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -210,16 +210,6 @@ Next Obligation. solve_proper. Qed.
 Definition monPred_in_aux : seal (@monPred_in_def). by eexists. Qed.
 Definition monPred_in := monPred_in_aux.(unseal).
 Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
-
-Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred :=
-  (* monPred_upclosed is not actually needed, since bupd is always
-     monotone. However, this depends on BUpdFacts, and we do not want
-     this definition to depend on BUpdFacts to avoid having proofs
-     terms in logical terms. *)
-  monPred_upclosed (λ i, |==> P i)%I.
-Definition monPred_bupd_aux `{BUpd PROP} : seal monPred_bupd_def. by eexists. Qed.
-Definition monPred_bupd `{BUpd PROP} : BUpd _ := monPred_bupd_aux.(unseal).
-Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := monPred_bupd_aux.(seal_eq).
 End Bi.
 
 Arguments monPred_objectively {_ _} _%I.
@@ -233,41 +223,27 @@ Implicit Types i : I.
 Notation monPred := (monPred I PROP).
 Implicit Types P Q : monPred.
 
-Definition monPred_plainly_def `{BiPlainly PROP} P : monPred := MonPred (λ _, ∀ i, ■ (P i))%I _.
-Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. by eexists. Qed.
-Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := monPred_plainly_aux.(unseal).
-Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := monPred_plainly_aux.(seal_eq).
-
-Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _.
+Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred :=
+  MonPred (λ _, a ≡ b)%I _.
 Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
 Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
-Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := monPred_internal_eq_aux.(seal_eq).
+Definition monPred_internal_eq_eq : @monPred_internal_eq = _ :=
+  monPred_internal_eq_aux.(seal_eq).
 
 Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_later_aux : seal monPred_later_def. by eexists. Qed.
 Definition monPred_later := monPred_later_aux.(unseal).
 Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
-
-Definition monPred_fupd_def `{FUpd PROP} (E1 E2 : coPset) (P : monPred) : monPred :=
-  (* monPred_upclosed is not actually needed, since fupd is always
-     monotone. However, this depends on FUpdFacts, and we do not want
-     this definition to depend on FUpdFacts to avoid having proofs
-     terms in logical terms. *)
-  monPred_upclosed (λ i, |={E1,E2}=> P i)%I.
-Definition monPred_fupd_aux `{FUpd PROP} : seal monPred_fupd_def. by eexists. Qed.
-Definition monPred_fupd `{FUpd PROP} : FUpd _ := monPred_fupd_aux.(unseal).
-Definition monPred_fupd_eq `{FUpd PROP} : @fupd _ monPred_fupd = _ := monPred_fupd_aux.(seal_eq).
 End Sbi.
 
 Module MonPred.
 Definition unseal_eqs :=
   (@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
-   @monPred_forall_eq, @monPred_exist_eq,
-   @monPred_sep_eq, @monPred_wand_eq,
+   @monPred_forall_eq, @monPred_exist_eq, @monPred_sep_eq, @monPred_wand_eq,
    @monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq,
-   @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq, @monPred_plainly_eq,
-   @monPred_objectively_eq, @monPred_subjectively_eq, @monPred_bupd_eq, @monPred_fupd_eq).
+   @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq,
+   @monPred_objectively_eq, @monPred_subjectively_eq).
 Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
          monPred_upclosed, bi_and, bi_or,
@@ -375,48 +351,6 @@ Qed.
 Canonical Structure monPredSI : sbi :=
   {| sbi_ofe_mixin := monPred_ofe_mixin; sbi_bi_mixin := monPred_bi_mixin I PROP;
      sbi_sbi_mixin := monPred_sbi_mixin |}.
-
-Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredSI monPred_plainly.
-Proof.
-  split; unseal.
-  - by (split=> ? /=; repeat f_equiv).
-  - intros P Q [?]. split=> i /=. by do 3 f_equiv.
-  - intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently.
-  - intros P. split=> i /=. repeat setoid_rewrite <-plainly_forall.
-    rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
-  - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
-    rewrite plainly_forall. apply bi.forall_intro=> a.
-    by rewrite !bi.forall_elim.
-  - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
-    repeat setoid_rewrite <-plainly_forall.
-    repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv.
-    apply persistently_impl_plainly.
-  - intros P Q. split=> i /=.
-    repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
-    repeat setoid_rewrite <-plainly_forall.
-    setoid_rewrite plainly_impl_plainly. f_equiv.
-    do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
-  - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
-  - intros P Q. split=> i. apply bi.sep_elim_l, _.
-  - intros P Q. split=> i /=.
-    rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _).
-    rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j.
-    rewrite -prop_ext !(bi.forall_elim j) !bi.pure_impl_forall
-            !bi.forall_elim //.
-  - intros P. split=> i /=.
-    rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
-  - intros P. split=> i /=.
-    rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
-Qed.
-Global Instance monPred_plainlyC `{BiPlainly PROP} : BiPlainly monPredSI :=
-  {| bi_plainly_mixin := monPred_plainly_mixin |}.
-
-Global Instance monPred_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
-  BiPlainlyExist PROP → BiPlainlyExist monPredSI.
-Proof.
-  split=>?/=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
-  apply bi.forall_intro=>?. by do 2 f_equiv.
-Qed.
 End canonical_sbi.
 
 Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
@@ -811,42 +745,37 @@ Global Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
   Objective ([∗ mset] y ∈ X, Φ y)%I.
 Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at. Qed.
 
-(** bupd *)
+(** BUpd *)
+Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
+  MonPred (λ i, |==> P i)%I _.
+Next Obligation. solve_proper. Qed.
+Definition monPred_bupd_aux `{BiBUpd PROP} : seal monPred_bupd_def. by eexists. Qed.
+Definition monPred_bupd `{BiBUpd PROP} : BUpd _ := monPred_bupd_aux.(unseal).
+Definition monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = _ :=
+  monPred_bupd_aux.(seal_eq).
+
 Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
 Proof.
-  split; unseal; unfold monPred_bupd_def, monPred_upclosed.
-  (* Note: Notation is somewhat broken here. *)
-  - intros n P Q HPQ. split=>/= i. by repeat f_equiv.
-  - intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall.
-    apply bi.forall_intro=><-. apply bupd_intro.
-  - intros P Q HPQ. split=>/= i. by repeat f_equiv.
-  - intros P. split=>/= i. do 3 f_equiv. rewrite -(bupd_trans (P _))
-      bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
-  - intros P Q. split=> /= i. apply bi.forall_intro=>?.
-    rewrite bi.pure_impl_forall. apply bi.forall_intro=><-.
-    rewrite -bupd_frame_r bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+  split; rewrite monPred_bupd_eq.
+  - split=>/= i. solve_proper.
+  - intros P. split=>/= i. apply bupd_intro.
+  - intros P Q HPQ. split=>/= i. by rewrite HPQ.
+  - intros P. split=>/= i. apply bupd_trans.
+  - intros P Q. split=>/= i. rewrite !monPred_at_sep /=. apply bupd_frame_r.
 Qed.
 Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
   {| bi_bupd_mixin := monPred_bupd_mixin |}.
 
 Lemma monPred_at_bupd `{BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
-Proof.
-  unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
-  - rewrite !bi.forall_elim //.
-  - do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
-Qed.
+Proof. by rewrite monPred_bupd_eq. Qed.
+
 Global Instance bupd_objective `{BiBUpd PROP} P `{!Objective P} :
   Objective (|==> P)%I.
 Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
 
 Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
   BiEmbedBUpd PROP monPredI.
-Proof.
-  split. unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall.
-  apply bi.equiv_spec; split.
-  - by do 2 apply bi.forall_intro=>?.
-  - rewrite !bi.forall_elim //.
-Qed.
+Proof. split. split=>i /=. by rewrite monPred_at_bupd !monPred_at_embed. Qed.
 End bi_facts.
 
 Section sbi_facts.
@@ -877,84 +806,15 @@ Proof.
   apply (@bi.f_equiv _ _ _ (λ P, monPred_at P inhabitant)); solve_proper.
 Qed.
 
-Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■ (P i) ⎤%I.
-Proof. by unseal. Qed.
 Lemma monPred_internal_eq_unfold : @sbi_internal_eq monPredSI = λ A x y, ⎡ x ≡ y ⎤%I.
 Proof. by unseal. Qed.
 
-Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredSI monPred_fupd.
-Proof.
-  split; unseal; unfold monPred_fupd_def, monPred_upclosed.
-  (* Note: Notation is somewhat broken here. *)
-  - intros E1 E2 n P Q HPQ. split=>/= i. by repeat f_equiv.
-  - intros E1 E2 P HE12. split=>/= i.
-    do 2 setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro=>?.
-    rewrite (fupd_intro_mask E1 E2 (P i)) //. f_equiv.
-    do 2 apply bi.forall_intro=>?. do 2 f_equiv. by etrans.
-  - intros E1 E2 P. split=>/= i. etrans; [apply bi.equiv_entails, bi.except_0_forall|].
-    do 2 f_equiv. rewrite bi.pure_impl_forall bi.except_0_forall. do 2 f_equiv.
-    by apply except_0_fupd.
-  - intros E1 E2 P Q HPQ. split=>/= i. by repeat f_equiv.
-  - intros E1 E2 E3 P. split=>/= i. do 3 f_equiv. rewrite -(fupd_trans _ _ _ (P _))
-      bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
-  - intros E1 E2 Ef P HE1f. split=>/= i. do 3 f_equiv. rewrite -fupd_mask_frame_r' //
-      bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
-  - intros E1 E2 P Q. split=>/= i. setoid_rewrite bi.pure_impl_forall.
-    do 2 setoid_rewrite bi.sep_forall_r. setoid_rewrite fupd_frame_r.
-    by repeat f_equiv.
-Qed.
-Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredSI :=
-  {| bi_fupd_mixin := monPred_fupd_mixin |}.
-Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredSI.
-Proof.
-  rewrite /BiBUpdFUpd; unseal; unfold monPred_fupd_def, monPred_upclosed.
-  intros E P. split=>/= i. by setoid_rewrite bupd_fupd.
-Qed.
-
-Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredSI.
-Proof.
-  rewrite /BiBUpdPlainly=> P; unseal.
-  split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall.
-  by rewrite bi.forall_elim // -plainly_forall bupd_plainly bi.forall_elim.
-Qed.
-
-Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i).
-Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed.
-
-Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
-Proof.
-  split; unseal.
-  - intros E1 E2 E2' P Q ? HE12. split=>/= i. repeat setoid_rewrite bi.pure_impl_forall.
-    do 4 f_equiv. rewrite 4?bi.forall_elim // fupd_plain' //.
-    apply bi.wand_intro_r. rewrite bi.wand_elim_l. do 2 apply bi.forall_intro=>?.
-    repeat f_equiv=>//. do 2 apply bi.forall_intro=>?. repeat f_equiv. by etrans.
-  - intros E P ?. split=>/= i. setoid_rewrite bi.pure_impl_forall.
-    do 2 setoid_rewrite bi.later_forall. do 4 f_equiv. apply later_fupd_plain, _.
-Qed.
-
-Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredSI.
-Proof.
-  split. unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall.
-  apply bi.equiv_spec; split.
-  - by do 2 apply bi.forall_intro=>?.
-  - rewrite !bi.forall_elim //.
-Qed.
-
 (** Unfolding lemmas *)
-Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
-Proof. by unseal. Qed.
 Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
   @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
 Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
 Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
 Proof. by unseal. Qed.
-Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
-  (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
-Proof.
-  unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
-  - rewrite !bi.forall_elim //.
-  - do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
-Qed.
 Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
 Proof. by unseal. Qed.
 
@@ -967,18 +827,7 @@ Proof.
                -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI.
 Qed.
 
-Global Instance monPred_objectively_plain `{BiPlainly PROP} P : Plain P → Plain (<obj> P).
-Proof. rewrite monPred_objectively_unfold. apply _. Qed.
-Global Instance monPred_subjectively_plain `{BiPlainly PROP} P : Plain P → Plain (<subj> P).
-Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
-
 (** Objective  *)
-Global Instance plainly_objective `{BiPlainly PROP} P : Objective (â–  P).
-Proof. intros ??. by unseal. Qed.
-Global Instance plainly_if_objective `{BiPlainly PROP} P p `{!Objective P} :
-  Objective (â– ?p P).
-Proof. rewrite /plainly_if. destruct p; apply _. Qed.
-
 Global Instance internal_eq_objective {A : ofeT} (x y : A) :
   @Objective I PROP (x ≡ y)%I.
 Proof. intros ??. by unseal. Qed.
@@ -990,7 +839,124 @@ Proof. induction n; apply _. Qed.
 Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P)%I.
 Proof. rewrite /sbi_except_0. apply _. Qed.
 
+(** FUpd  *)
+Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
+        (P : monPred) : monPred :=
+  MonPred (λ i, |={E1,E2}=> P i)%I _.
+Next Obligation. solve_proper. Qed.
+Definition monPred_fupd_aux `{BiFUpd PROP} : seal monPred_fupd_def. by eexists. Qed.
+Definition monPred_fupd `{BiFUpd PROP} : FUpd _ := monPred_fupd_aux.(unseal).
+Definition monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = _ :=
+  monPred_fupd_aux.(seal_eq).
+
+Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredSI monPred_fupd.
+Proof.
+  split; rewrite monPred_fupd_eq.
+  - split=>/= i. solve_proper.
+  - intros E1 E2 P HE12. split=>/= i. by apply fupd_intro_mask.
+  - intros E1 E2 P. split=>/= i. by rewrite monPred_at_except_0 except_0_fupd.
+  - intros E1 E2 P Q HPQ. split=>/= i. by rewrite HPQ.
+  - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
+  - intros E1 E2 Ef P HE1f. split=>/= i.
+    rewrite monPred_impl_force monPred_at_pure -fupd_mask_frame_r' //.
+  - intros E1 E2 P Q. split=>/= i. by rewrite !monPred_at_sep /= fupd_frame_r.
+Qed.
+Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredSI :=
+  {| bi_fupd_mixin := monPred_fupd_mixin |}.
+Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredSI.
+Proof.
+  intros E P. split=>/= i. rewrite monPred_at_bupd monPred_fupd_eq bupd_fupd //=.
+Qed.
+Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredSI.
+Proof. split. split=>i /=. by rewrite monPred_fupd_eq /= !monPred_at_embed. Qed.
+
+Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
+  (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
+Proof. by rewrite monPred_fupd_eq. Qed.
+
 Global Instance fupd_objective E1 E2 P `{!Objective P} `{BiFUpd PROP} :
   Objective (|={E1,E2}=> P)%I.
 Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
+
+(** Plainly *)
+Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
+  MonPred (λ _, ∀ i, ■ (P i))%I _.
+Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. by eexists. Qed.
+Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := monPred_plainly_aux.(unseal).
+Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := monPred_plainly_aux.(seal_eq).
+
+Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredSI monPred_plainly.
+Proof.
+  split; rewrite monPred_plainly_eq; try unseal.
+  - by (split=> ? /=; repeat f_equiv).
+  - intros P Q [?]. split=> i /=. by do 3 f_equiv.
+  - intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently.
+  - intros P. split=> i /=. repeat setoid_rewrite <-plainly_forall.
+    rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
+  - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
+    rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
+  - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
+    repeat setoid_rewrite <-plainly_forall.
+    repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv.
+    apply persistently_impl_plainly.
+  - intros P Q. split=> i /=.
+    repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
+    repeat setoid_rewrite <-plainly_forall.
+    setoid_rewrite plainly_impl_plainly. f_equiv.
+    do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
+  - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
+  - intros P Q. split=> i. apply bi.sep_elim_l, _.
+  - intros P Q. split=> i /=.
+    rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _).
+    rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j.
+    rewrite -prop_ext !(bi.forall_elim j) !bi.pure_impl_forall
+            !bi.forall_elim //.
+  - intros P. split=> i /=.
+    rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
+  - intros P. split=> i /=.
+    rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
+Qed.
+Global Instance monPred_plainlyC `{BiPlainly PROP} : BiPlainly monPredSI :=
+  {| bi_plainly_mixin := monPred_plainly_mixin |}.
+
+Global Instance monPred_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
+  BiPlainlyExist PROP → BiPlainlyExist monPredSI.
+Proof.
+  split=>?/=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
+  rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
+  apply bi.forall_intro=>?. by do 2 f_equiv.
+Qed.
+
+Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■ (P i) ⎤%I.
+Proof. by rewrite monPred_plainly_eq monPred_embed_eq. Qed.
+Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
+Proof. by rewrite monPred_plainly_eq. Qed.
+
+Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredSI.
+Proof.
+  intros P. split=> /= i.
+  rewrite monPred_at_bupd monPred_at_plainly bi.forall_elim. apply bupd_plainly.
+Qed.
+
+Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i).
+Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
+
+Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
+Proof.
+  split; rewrite monPred_fupd_eq; unseal.
+  - intros E1 E2 E2' P Q ? HE12. split=>/= i. do 3 f_equiv.
+    apply fupd_plain'; [apply _|done].
+  - intros E P ?. split=>/= i. apply later_fupd_plain, _.
+Qed.
+
+Global Instance plainly_objective `{BiPlainly PROP} P : Objective (â–  P).
+Proof. rewrite monPred_plainly_unfold. apply _. Qed.
+Global Instance plainly_if_objective `{BiPlainly PROP} P p `{!Objective P} :
+  Objective (â– ?p P).
+Proof. rewrite /plainly_if. destruct p; apply _. Qed.
+
+Global Instance monPred_objectively_plain `{BiPlainly PROP} P : Plain P → Plain (<obj> P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+Global Instance monPred_subjectively_plain `{BiPlainly PROP} P : Plain P → Plain (<subj> P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
 End sbi_facts.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index cc9c7c09a0d011bd78509b8f1a690dc29702654b..953b7bd91cb23fb29714883a8124dc7ec70ea159 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -8,11 +8,12 @@ Import env_notations.
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
 Record envs (PROP : bi) :=
-  Envs { env_persistent : env PROP; env_spatial : env PROP }.
+  Envs { env_persistent : env PROP; env_spatial : env PROP; env_counter : positive }.
 Add Printing Constructor envs.
-Arguments Envs {_} _ _.
+Arguments Envs {_} _ _ _.
 Arguments env_persistent {_} _.
 Arguments env_spatial {_} _.
+Arguments env_counter {_} _.
 
 Record envs_wf {PROP} (Δ : envs PROP) := {
   env_persistent_valid : env_wf (env_persistent Δ);
@@ -43,7 +44,7 @@ Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
   env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
 
 Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match env_lookup i Γp with
   | Some P => Some (true, P)
   | None => P ← env_lookup i Γs; Some (false, P)
@@ -51,18 +52,18 @@ Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP
 
 Definition envs_delete {PROP} (remove_persistent : bool)
     (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match p with
-  | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs
-  | false => Envs Γp (env_delete i Γs)
+  | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
+  | false => Envs Γp (env_delete i Γs) n
   end.
 
 Definition envs_lookup_delete {PROP} (remove_persistent : bool)
     (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match env_lookup_delete i Γp with
-  | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs)
-  | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
+  | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
+  | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
   end.
 
 Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
@@ -77,23 +78,23 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
 
 Definition envs_snoc {PROP} (Δ : envs PROP)
     (p : bool) (j : ident) (P : PROP) : envs PROP :=
-  let (Γp,Γs) := Δ in
-  if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).
+  let (Γp,Γs,n) := Δ in
+  if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
 
 Definition envs_app {PROP : bi} (p : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match p with
-  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs)
-  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs')
+  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs n)
+  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs' n)
   end.
 
 Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match p with
-  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs)
-  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs')
+  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs n)
+  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs' n)
   end.
 
 Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
@@ -105,10 +106,13 @@ Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
   if env_spatial Δ is Enil then true else false.
 
 Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs (env_persistent Δ) Enil.
+  Envs (env_persistent Δ) Enil (env_counter Δ).
 
 Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs Enil (env_spatial Δ).
+  Envs Enil (env_spatial Δ) (env_counter Δ).
+
+Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
+  Envs (env_persistent Δ) (env_spatial Δ) (Pos.succ (env_counter Δ)).
 
 Fixpoint envs_split_go {PROP}
     (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
@@ -464,7 +468,7 @@ Proof.
     eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails.
 Qed.
 Global Instance Envs_proper (R : relation PROP) :
-  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
+  Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP).
 Proof. by constructor. Qed.
 
 Global Instance envs_entails_proper :
@@ -475,7 +479,7 @@ Global Instance envs_entails_flip_mono :
 Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
 
 (** * Adequacy *)
-Lemma tac_adequate P : envs_entails (Envs Enil Enil) P → P.
+Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P → P.
 Proof.
   rewrite envs_entails_eq /of_envs /= persistently_True_emp
           affinely_persistently_emp left_id=><-.
@@ -1083,6 +1087,18 @@ Lemma tac_accu Δ P :
   envs_entails Δ P.
 Proof. rewrite envs_entails_eq=><-. apply prop_of_env_sound. Qed.
 
+(** * Fresh *)
+Lemma envs_incr_counter_equiv Δ: envs_Forall2 (⊣⊢) Δ (envs_incr_counter Δ).
+Proof. rewrite //=. Qed.
+
+Lemma tac_fresh Δ Δ' (Q : PROP) :
+  envs_incr_counter Δ = Δ' →
+  envs_entails Δ' Q → envs_entails Δ Q.
+Proof.
+  rewrite envs_entails_eq => <-. by setoid_rewrite <-envs_incr_counter_equiv.
+Qed.
+
+
 End bi_tactics.
 
 (** The following _private_ classes are used internally by [tac_modal_intro] /
@@ -1260,15 +1276,15 @@ Section tac_modal_intro.
   Qed.
 
   (** The actual introduction tactic *)
-  Lemma tac_modal_intro {A} (sel : A) Γp Γs Γp' Γs' Q Q' fi :
+  Lemma tac_modal_intro {A} (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
     FromModal M sel Q' Q →
     IntoModalPersistentEnv M Γp Γp' (modality_persistent_spec M) →
     IntoModalSpatialEnv M Γs Γs' (modality_spatial_spec M) fi →
     (if fi then Absorbing Q' else TCTrue) →
-    envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
+    envs_entails (Envs Γp' Γs' n) Q → envs_entails (Envs Γp Γs n) Q'.
   Proof.
     rewrite envs_entails_eq /FromModal /of_envs /= => HQ' HΓp HΓs ? HQ.
-    apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')) as Hwf.
+    apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs' n)) as Hwf.
     { split; simpl in *.
       - destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
       - destruct HΓs as [| |?????? []| |]; eauto using Enil_wf.
@@ -1363,10 +1379,10 @@ Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
       (MaybeIntoLaterN false n) (env_spatial Δ1) (env_spatial Δ2) false
 }.
 
-Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
+Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 m :
   TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
   TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
-  MaybeIntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
+  MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
 Proof. by split. Qed.
 
 Lemma into_laterN_env_sound n Δ1 Δ2 :
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index b0d9d515731ffc506a9deed99b9dd90029a0cc13..37bce07be123dbec55aa9b1253e42443d8e20731 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -3,7 +3,7 @@ From stdpp Require Export strings.
 Set Default Proof Using "Type".
 
 Delimit Scope proof_scope with env.
-Arguments Envs _ _%proof_scope _%proof_scope.
+Arguments Envs _ _%proof_scope _%proof_scope _.
 Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%I.
 
@@ -16,17 +16,17 @@ Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
    left associativity, format "Γ '_'  :  P '//'", only printing) : proof_scope.
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
-  (envs_entails (Envs Γ Δ) Q%I)
+  (envs_entails (Envs Γ Δ _) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
   stdpp_scope.
 Notation "Δ '--------------------------------------' ∗ Q" :=
-  (envs_entails (Envs Enil Δ) Q%I)
+  (envs_entails (Envs Enil Δ _) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
 Notation "Γ '--------------------------------------' □ Q" :=
-  (envs_entails (Envs Γ Enil) Q%I)
+  (envs_entails (Envs Γ Enil _) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : stdpp_scope.
-Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil) Q%I)
+Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil _) Q%I)
   (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 268d813e47b914700ef9604e28754773518a93bb..ac5534879b1c299c8666f04b75a1f3c02eda3cc3 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -10,12 +10,12 @@ Export ident.
 
 Declare Reduction env_cbv := cbv [
   option_bind
-  beq ascii_beq string_beq positive_beq ident_beq
+  beq ascii_beq string_beq positive_beq Pos.succ ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
-  env_persistent env_spatial env_spatial_is_nil envs_dom
+  env_persistent env_spatial env_counter env_spatial_is_nil envs_dom
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
     envs_simple_replace envs_replace envs_split
-    envs_clear_spatial envs_clear_persistent
+    envs_clear_spatial envs_clear_persistent envs_incr_counter
     envs_split_go envs_split prop_of_env].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
@@ -40,20 +40,6 @@ Ltac iSolveTC :=
   solve [once (typeclasses eauto)].
 
 (** * Misc *)
-(* Tactic Notation tactics cannot return terms *)
-Ltac iFresh :=
-  lazymatch goal with
-  |- envs_entails ?Δ _ =>
-     (* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
-     first use [cbv] to compute the domain of [Δ] *)
-     let Hs := eval cbv in (envs_dom Δ) in
-     eval vm_compute in
-       (IAnon (match Hs with
-         | [] => 1
-         | _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
-         end))%positive
-  | _ => constr:(IAnon 1)
-  end.
 
 Ltac iMissingHyps Hs :=
   let Δ :=
@@ -103,6 +89,22 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
                |apply tac_adequate]
   end.
 
+(** * Generate a fresh identifier *)
+(* Tactic Notation tactics cannot return terms *)
+Ltac iFresh :=
+  (* We need to increment the environment counter using [tac_fresh].
+     But because [iFresh] returns a value, we have to let bind
+     [tac_fresh] wrapped under a match to force evaluation of this
+     side-effect. See https://stackoverflow.com/a/46178884 *)
+  let do_incr :=
+      lazymatch goal with
+      | _ => iStartProof; eapply tac_fresh; first by (env_reflexivity)
+      end in
+  lazymatch goal with
+  |- envs_entails ?Δ _ =>
+    let n := eval env_cbv in (env_counter Δ) in
+    constr:(IAnon n)
+  end.
 
 (** * Simplification *)
 Tactic Notation "iEval" tactic(t) :=
@@ -200,13 +202,13 @@ Tactic Notation "iAssumptionCore" :=
     | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j|find Γ i P]
     end in
   match goal with
-  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
+  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
      first [is_evar i; fail 1 | env_reflexivity]
-  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
+  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
      is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
-  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
      first [is_evar i; fail 1 | env_reflexivity]
-  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
      is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
   end.
 
@@ -228,7 +230,7 @@ Tactic Notation "iAssumption" :=
        |find p Γ Q]
     end in
   lazymatch goal with
-  | |- envs_entails (Envs ?Γp ?Γs) ?Q =>
+  | |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
      first [find true Γp Q | find false Γs Q
            |fail "iAssumption:" Q "not found"]
   end.
@@ -974,7 +976,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Modality introduction *)
 Tactic Notation "iModIntro" uconstr(sel) :=
   iStartProof;
-  notypeclasses refine (tac_modal_intro _ sel _ _ _ _ _ _ _ _ _ _ _ _);
+  notypeclasses refine (tac_modal_intro _ sel _ _ _ _ _ _ _ _ _ _ _ _ _);
     [iSolveTC ||
      fail "iModIntro: the goal is not a modality"
     |iSolveTC ||
@@ -1569,8 +1571,8 @@ Ltac iHypsContaining x :=
        | _ => go Γ x Hs
        end
      end in
-  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _) _ => Γp end in
-  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs) _ => Γs end in
+  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _ _) _ => Γp end in
+  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs _) _ => Γs end in
   let Hs := go Γp x (@nil ident) in go Γs x Hs.
 
 Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
@@ -1872,7 +1874,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
       first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i]
     end in
   lazymatch goal with
-  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some _ =>
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some _ =>
      first [find Γp i|find Γs i]; env_reflexivity
   end.
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index fc8ff5bcdc8b89933ef72badceabf466c1395842..f9c38b371f0ac75ddf934e0b0e7930bcbb672be8 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
-From stdpp Require Import gmap.
+From iris.proofmode Require Import tactics intro_patterns.
+From stdpp Require Import gmap hlist.
 Set Default Proof Using "Type".
 
 Section tests.
@@ -112,6 +112,17 @@ Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
   P -∗ Q → R -∗ emp.
 Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
 
+Let test_fresh P Q:
+  (P ∗ Q) -∗ (P ∗ Q).
+Proof.
+  iIntros "H".
+  let H1 := iFresh in
+  let H2 := iFresh in
+  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in 
+  iDestruct "H" as pat.
+  iFrame.
+Qed.
+
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.