diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 7dd8dbc47c4714553166652323650b772b469793..f49d3f68138a9dbdec03862f464741218e3cc198 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -110,6 +110,7 @@ Section constrained.
   Hypothesis Hl' : List.length tpost' = List.length tpost.
   Hypothesis Htc : tc = cycle sbState t.
   Hypothesis Htc' : tc' = cycle sbState' t'.
+  Hypothesis HconstT : is_constrained e t sbState = true.
 
   (* Delve into tc, tc', cycle, cycle_elt, etc.
    * Pretty specific to these constraints, do not use it outside this section. *)
@@ -136,12 +137,11 @@ Section constrained.
 
   (* If a constrained Sp can advance, an unconstrained Sp can advance. *)
   Theorem constrained_sp_can_advance_unconstrained_too :
-    e = (opc, (Sp, 0)) ->
     (* t is constrained, t' is unconstrained *)
-    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+    e = (opc, (Sp, 0)) -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
   Proof.
-    intros He HconstT HconstT'.
+    intros He HconstT'.
     rewrite He in HconstT'.
 
     constraint_delve He.
@@ -155,12 +155,11 @@ Section constrained.
   (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
   (* Load version *)
   Theorem constrained_lsu_load_advance_unconstrained_too :
-    e = (Load, (Lsu, 0)) ->
     (* t is constrained, t' is unconstrained *)
-    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+    e = (Load, (Lsu, 0)) -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (Load, (Lu, 0)) -> List.nth_error tc' i = Some (Load, (Lu, 0)).
   Proof.
-    intros He Hconst.
+    intro He.
 
     rewrite He.
     unfold is_constrained.
@@ -181,12 +180,11 @@ Section constrained.
 
   (* Store version *)
   Theorem constrained_lsu_store_advance_unconstrained_too :
-    e = (Store, (Lsu, 0)) ->
     (* t is constrained, t' is unconstrained *)
-    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+    e = (Store, (Lsu, 0)) -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
   Proof.
-    intros He HconstT HconstT'.
+    intros He HconstT'.
     rewrite He in HconstT'.
 
     constraint_delve He.