diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index e375b48f8a5add3f83d78662d178410df0776551..4616ed4b84e6cd0b67fb9c3336b92f092c2d7067 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -282,7 +282,9 @@ Section monotonicity.
     compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
   Proof.
     intros He He' Hed Hsl.
-    specialize (Hsu st' opc).
+    specialize (Hlu st opc 0).
+    pose proof (Hsu st' opc) as Hsu'.
+    specialize (Hsu st opc).
 
     (* Goal transformation: show exactly how e and e' are modified by the
      * cycle function. *)
@@ -303,14 +305,22 @@ Section monotonicity.
     - now destruct (ready _ _ _ && free _ _ _ _), opc.
     - destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc;
         try reflexivity.
-      now discriminate Hsu.
+      now discriminate Hsu'.
     - now destruct (ready _ _ _ && free _ _ _ _), opc.
 
     (* st = Lu, st' = Sn *)
-    - now destruct opc.
+    - now destruct opc;
+        (* Trivial when opc = Load, eliminate the case where opc = Store. *)
+        [| discriminate Hlu].
 
     (* st = Su, st' = Sn *)
-    - now destruct (ready _ _ _ && free _ _ _ _), opc.
+    - now destruct opc; [
+          (* Eliminate the case where opc = Load. *)
+          discriminate Hsu |
+          (* Either the instruction remains in Su, or it progresses in Sn. *)
+          (* Both cases are trivial. *)
+          destruct (_ && _)
+        ].
   Qed.
 
   Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.