diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 03397a4e230e197ccdc1becac6010af5896ccd5b..2d910d657eac002a9b8c85e837498dd3b268b9f0 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -41,12 +41,12 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed
Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
Proof.
split.
- - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q ?) "HQP HQ [Hw HE]".
- iAssert (◇ P)%I as "#>$".
+ - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "HQP HQ [Hw HE]".
+ iAssert (◇ ■ P)%I as "#>HP'".
{ by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
by iFrame.
- - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (p E1 E2 P ?) "HP [Hw HE]".
- iAssert (▷?p ◇ P)%I with "[-]" as "#$"; last by iFrame.
+ - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (p E1 E2 P) "HP [Hw HE]".
+ iAssert (▷?p ◇ ■ P)%I with "[-]" as "#HP'"; last by (rewrite plainly_elim; iFrame).
iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index cd936f5dbe005d47e10a3046cf198570b2c80916..5a3be2fc980ddf9a78f83b73cdebba98e0ae25da 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -957,10 +957,10 @@ Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Q
Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
Proof.
split; rewrite monPred_fupd_eq; unseal.
- - intros E P Q ?. split=>/= i. do 3 f_equiv.
- apply fupd_plain_weak; apply _.
- - intros p E1 E2 P ?. split=>/= i. specialize (later_fupd_plain p) => HFP.
- destruct p; simpl; [ unseal | ]; apply HFP, _.
+ - intros E P Q. split=>/= i. do 3 f_equiv.
+ rewrite monPred_at_plainly (bi.forall_elim _) fupd_plainly_weak //=.
+ - intros p E1 E2 P; split=>/= i; specialize (later_fupd_plainly p) => HFP.
+ destruct p; simpl; [ unseal | ]; rewrite monPred_at_plainly (bi.forall_elim _); apply HFP.
Qed.
Global Instance plainly_objective `{BiPlainly PROP} P : Objective (■ P).
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 8df0ab3db78f09beacd01f5223c6a74df6e21b91..50827b359050d8fcd0b15d7c30ebe6bac0a67a81 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -78,10 +78,10 @@ Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
- fupd_plain_weak E (P Q : PROP) `{!Plain P} :
- (Q ={E}=∗ P) -∗ Q ={E}=∗ Q ∗ P;
- later_fupd_plain p E1 E2 (P : PROP) `{!Plain P} :
- (▷?p |={E1, E2}=> P) ={E1}=∗ ▷?p ◇ P;
+ fupd_plainly_weak E (P Q : PROP) :
+ (Q ={E}=∗ ■ P) -∗ Q ={E}=∗ Q ∗ P;
+ later_fupd_plainly p E1 E2 (P : PROP) :
+ (▷?p |={E1, E2}=> ■ P) ={E1}=∗ ▷?p ◇ P;
}.
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
@@ -272,6 +272,14 @@ Section fupd_derived.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
+ Lemma fupd_plain_weak `{BiPlainly PROP, !BiFUpdPlainly PROP} E P Q `{!Plain P}:
+ (Q ={E}=∗ P) -∗ Q ={E}=∗ Q ∗ P.
+ Proof. by rewrite {1}(plain P) fupd_plainly_weak. Qed.
+
+ Lemma later_fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} p E1 E2 P `{!Plain P} :
+ (▷?p |={E1, E2}=> P) ={E1}=∗ ▷?p ◇ P.
+ Proof. by rewrite {1}(plain P) later_fupd_plainly. Qed.
+
Lemma fupd_plain_strong `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P `{!Plain P} :
(|={E1, E2}=> P) ={E1}=∗ ◇ P.
Proof. by apply (later_fupd_plain false). Qed.