diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index ed80e9ca4ed7abbfbd9ae8a13161e356fc751d2b..5c66f9c7c283d4d1c6647cade4a331233811f3d6 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -30,7 +30,7 @@ Class lock `{!heapGS_gen hlc Σ} := Lock {
   (** * General properties of the predicates *)
   is_lock_persistent γ lk R :> Persistent (is_lock γ lk R);
   is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2;
+    is_lock γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock γ lk R2;
   locked_timeless γ :> Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (** * Program specs *)
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 30753ba199745709696bb6a35c05d29ea38bc8af..c449f45c6f4484e7e7d8f32a5b49bc66764b4c82 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -39,7 +39,7 @@ Section proof.
 
   (** The main proofs. *)
   Local Lemma is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk 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").
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 6095603642904fdc76224c0e4bb87763af50fa0e..02c4e48d071cb9983206c99655b54317ebc2e52d 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -63,7 +63,7 @@ Section proof.
   Qed.
 
   Local Lemma is_lock_iff γ lk R1 R2 :
-    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk 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").