diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 0889c404dea27917a7a67c3585cee8af77f89d0b..e72d196f43d8268f2f49a9bb45282b3db973ad08 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -59,11 +59,12 @@ Proof.
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness `{!invPreG Σ} E (P: iProp Σ) `{!Plain P}:
-  (∀ `{Hinv: !invG Σ}, (|={⊤,E}=> P)%I) → (▷ P)%I.
+Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
+  (∀ `{Hinv: !invG Σ}, (|={E1,E2}=> P)%I) → (▷ P)%I.
 Proof.
   iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
-  iPoseProof (Hfupd Hinv) as "H".
+  iAssert (|={⊤,E2}=> P)%I as "H".
+  { iMod fupd_intro_mask'; last iApply Hfupd. done. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
@@ -74,7 +75,7 @@ Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
 Proof.
   intros Hiter.
   apply (soundness (M:=iResUR Σ) _  (S (S n))); simpl.
-  apply (fupd_plain_soundness ⊤ _)=> Hinv.
+  apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   destruct n as [|n].
   - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 9e8ba8f6dbfe6f2be17f8b305b95d6167248ebe3..170602811f2ea7f2678d3b3002635c21b2d90f8a 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -124,7 +124,7 @@ Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  2); simpl.
-  apply (fupd_plain_soundness ⊤ _)=> Hinv.
+  apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iMod (Hwp) as (stateI fork_post) "[Hσ H]".
   iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ").
   by iApply (@twp_twptp _ _ (IrisG _ _ Hinv stateI fork_post)).