diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 5ed577320d8f3f4282f5d1f1c3800707fd16242e..184b62fd4b524fff8033ef918d05b9b7137c4996 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -15,6 +15,8 @@ Structure lock Σ `{!heapG Σ} := Lock {
   (* -- general properties -- *)
   is_lock_ne N γ lk : Contractive (is_lock N γ lk);
   is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
+  is_lock_iff N γ lk R1 R2 :
+    is_lock N γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock N γ lk R2;
   locked_timeless γ : Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (* -- operation specs -- *)
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index c7e2cbc8497522b7bb7bf0819b290e67dafe2a38..d9be8c585c60044a9b962465a22be0df15ec8453 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -45,6 +45,16 @@ Section proof.
   Global Instance locked_timeless γ : Timeless (locked γ).
   Proof. apply _. Qed.
 
+  Lemma is_lock_iff γ lk R1 R2 :
+    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2.
+  Proof.
+    iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
+    iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
+    iIntros "!> !#"; iSplit; iDestruct 1 as (b) "[Hl H]";
+      iExists b; iFrame "Hl"; destruct b;
+      first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
+  Qed.
+
   Lemma newlock_spec (R : iProp Σ):
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
@@ -92,5 +102,6 @@ End proof.
 Typeclasses Opaque is_lock locked.
 
 Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
-  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
+  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
+     lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 603984a5a963340d8415aa1785720bf7a35669e9..93b60961cb81a53bdeded9d0b0f49c7a058dc1ad 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -69,6 +69,16 @@ Section proof.
     iDestruct (own_valid_2 with "H1 H2") as %[[] _].
   Qed.
 
+  Lemma is_lock_iff γ lk R1 R2 :
+    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2.
+  Proof.
+    iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
+    iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
+    iIntros "!> !#"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)";
+      iExists o, n; iFrame "Ho Hn H●";
+      (iDestruct "H" as "[[Hâ—¯ H]|Hâ—¯]"; [iLeft; iFrame "Hâ—¯"; by iApply "HR"|by iRight]).
+  Qed.
+
   Lemma newlock_spec (R : iProp Σ) :
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
@@ -162,5 +172,6 @@ End proof.
 Typeclasses Opaque is_lock issued locked.
 
 Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
-  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
+  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
+     lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.