diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index 2350e14a6163e4dbc12cb750f6cc1fff3bd598c3..35aa7886e2b5f8d46656fb45bde8a87e4e2b378b 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -35,7 +35,7 @@ Class rwlock `{!heapGS_gen hlc Σ} := RwLock {
   (** * General properties of the predicates *)
   is_rw_lock_persistent γ lk Φ :> Persistent (is_rw_lock γ lk Φ);
   is_rw_lock_iff γ lk Φ Ψ :
-    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q,  Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ;
+    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ;
   reader_locked_timeless γ q :> Timeless (reader_locked γ q);
   writer_locked_timeless γ :> Timeless (writer_locked γ);
   writer_locked_exclusive γ : writer_locked γ -∗ writer_locked γ -∗ False;