diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 6e796ac74c47972236d9e592738aab439fe3bb6f..580ba7dbfa3b17de2840a8c6420cb7932df7e0e0 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -99,11 +99,22 @@ Qed.
 Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
-  intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
-  destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P) as (m'&?&?); auto.
+  intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
+  destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
   { apply cmra_includedN_le with (S n); auto. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
+Lemma pvs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
+    E (P : iGst Λ Σ → Prop) :
+  ∅ ~~>: P → True ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
+Proof.
+  intros Hup r [|n] ? _ rf [|k] Ef σ ???; try lia.
+  destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto.
+  { apply cmra_empty_leastN. }
+  { apply cmra_updateP_compose_l with (Some ∅), option_updateP with P;
+      auto using option_update_None. }
+  by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
+Qed.
 Lemma pvs_alloc E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ inv i P).
 Proof.
   intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
@@ -138,7 +149,7 @@ Proof.
 Qed.
 Lemma pvs_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
 Proof.
-  intros; rewrite ->(pvs_updateP E _ (m' =)); last by apply cmra_update_updateP.
+  intros; rewrite (pvs_updateP E _ (m' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
 Qed.
 End pvs.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index c44d8a4158df434357bbc75b85d8ff32c9d8db98..7c5fb13d71ca084c03ffd3c2f8215ba5081c49b5 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -89,6 +89,10 @@ Qed.
 Lemma vs_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
 Proof. by intros; apply vs_alt, pvs_updateP. Qed.
+Lemma vs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
+    E (P : iGst Λ Σ → Prop) :
+  ∅ ~~>: P → True >{E}> (∃ m', ■ P m' ∧ ownG m').
+Proof. by intros; apply vs_alt, pvs_updateP_empty. Qed.
 Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'.
 Proof. by intros; apply vs_alt, pvs_update. Qed.
 Lemma vs_alloc E P : ¬set_finite E → ▷ P >{E}> (∃ i, ■ (i ∈ E) ∧ inv i P).
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index bf7d2c35ef8a6e34ea840123c10e7ebc85c052e8..f956c30676da1422f4340dbd1e0a8d067cf660a7 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -125,13 +125,13 @@ Proof.
   split; [done|exists rs].
   by constructor; split_ands'; try (rewrite /= -associative Hpst').
 Qed.
-Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
-  Some m1 ≼{S n} gst r → m1 ~~>: P →
+Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
+  mm1 ≼{S n} gst r → mm1 ~~>: (λ mm2, default False mm2 P) →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.
-  intros [mf Hr] Hup%option_updateP' [rs [(?&?&?) Hσ HE Hwld]].
+  intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
   destruct (Hup (mf â‹… gst (rf â‹… big_opM rs)) n) as ([m2|]&?&Hval'); try done.
-  { by rewrite /= (associative _ (Some m1)) -Hr associative. }
+  { by rewrite /= (associative _ mm1) -Hr associative. }
   exists m2; split; [exists rs; split; split_ands'; auto|done].
 Qed.
 Lemma wsat_alloc n E1 E2 σ r P rP :