diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index ddfcc0098198068ab3a1d21a35140737de51c9d7..46b97dbee01e16e59d4dfb900f0f38fff79c87c0 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -305,6 +305,6 @@ Section monotonicity.
     - now destruct opc.
 
     (* st = Su, st' = Sn *)
-    - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
+    - now destruct (ready _ _ _ && free _ _ _ _), opc.
   Qed.
 End monotonicity.