diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 009f1e5f350b33076e78e7b5ca63d541aed8b909..4fa210e537441ffc84c2f8e97ec76bff7bf138a1 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -152,4 +152,22 @@ Section constrained.
         reflexivity.
     - exact HconstT'.
   Qed.
+
+  (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
+  (* Store version *)
+  Theorem constrained_lsu_store_advance_unconstrained_too :
+    e = (Store, (Lsu, 0)) ->
+    (* t is constrained, t' is unconstrained *)
+    (List.existsb is_in_su t) = true -> (List.existsb is_in_su t') = false ->
+    List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
+  Proof.
+    intros He HconstT HconstT'.
+
+    constraint_delve He.
+
+    unfold suFree, get_instr_in_stage.
+    rewrite (not_existsb_means_cannot_find _ _ t').
+    - reflexivity.
+    - exact HconstT'.
+  Qed.
 End constrained.