diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 94c3bcc694cd5a57c589d9789bf92738b1695b58..d4a33a5685a2460977dbda9c0c28b57c2a5733cc 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -206,7 +206,7 @@ Proof.
 Qed.
 
 Lemma twp_xchg_offset s E l off vs v v' :
-  (vs !! off) = Some v →
+  vs !! off = Some v →
   val_is_unboxed v ->
   [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
 Proof.