diff --git a/algebra/cmra.v b/algebra/cmra.v
index 94a13c0c1bd2dc2a509c8a7cf7dd5a6347ecbde4..94a6e73c1c96200567d34c7f6285d86f165475bc 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -378,6 +378,8 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
 Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
+Lemma cmra_update_id x : x ~~> x.
+Proof. intro. auto. Qed.
 
 Section identity_updates.
   Context `{Empty A, !CMRAIdentity A}.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 128cb1c9267daa827d2deb1941d6574f92597d74..140232a58bedd8e444a05f621944272a082ac219 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -35,6 +35,10 @@ Section auth.
     by rewrite always_and_sep_l.
   Qed.
 
+  Lemma auth_empty γ E :
+    True ⊑ pvs E E (auth_own γ ∅).
+  Proof. by rewrite own_update_empty /auth_own. Qed.
+
   Context {Hφ : ∀ n, Proper (dist n ==> dist n) φ}.
 
   Lemma auth_opened E a γ :
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 16c09f5e73490057c58fe3ad143de3166e08694f..c4dd8960025dc521473390672e61a0c17ae31c5d 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -93,7 +93,7 @@ Proof.
     by rewrite -(exist_intro γ).
 Qed.
 
-Lemma own_updateP γ a P E :
+Lemma own_updateP P γ a E :
   a ~~>: P → own i γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own i γ a').
 Proof.
   intros Ha.
@@ -105,7 +105,7 @@ Proof.
     rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
 Qed.
 
-Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} γ a P E :
+Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E :
   ∅ ~~>: P → True ⊑ pvs E E (∃ a, ■ P a ∧ own i γ a).
 Proof.
   intros Hemp.
@@ -119,7 +119,14 @@ Qed.
 
 Lemma own_update γ a a' E : a ~~> a' → own i γ a ⊑ pvs E E (own i γ a').
 Proof.
-  intros; rewrite (own_updateP _ _ (a' =)); last by apply cmra_update_updateP.
-  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
+  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
+  by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
+Qed.
+
+Lemma own_update_empty `{Empty A, !CMRAIdentity A} γ E :
+  True ⊑ pvs E E (own i γ ∅).
+Proof.
+  rewrite (own_updateP_empty (∅ =)); last by apply cmra_updateP_id.
+  apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
 Qed.
 End global.