diff --git a/src/definitions.v b/src/definitions.v
index ad4fe5bc8f2745e12b34c99f884bb60a614c1774..3096c8746c0e85b777589b8b20162edb68c007a2 100644
--- a/src/definitions.v
+++ b/src/definitions.v
@@ -110,6 +110,15 @@ Definition state_leb st1 st2 :=
 Definition instr_kind := (opcode * state)%type.
 Definition trace_kind := list instr_kind.
 
+(* Compare two with options.  This will be necessary for proofs since we will
+ * make heavy use of List.nth_error. *)
+Definition compare_two (e1 e2 : option instr_kind) :=
+  match e1, e2 with
+  | None, _
+  | _, None => false
+  | Some (_, st1), Some (_, st2) => state_leb st1 st2
+  end.
+
 Definition get_opc (trace : trace_kind) :=
   fst (List.split trace).
 
diff --git a/src/store_buffer.v b/src/store_buffer.v
index dff98d31534b00a0a50a64e9c2c2055f81d5a469..dcfd33a4f73f64bb38170b8163dddefa5bb382dd 100644
--- a/src/store_buffer.v
+++ b/src/store_buffer.v
@@ -57,13 +57,6 @@ Definition cycle dchit busTaken wbFull trace :=
   let isSuUsed := List.existsb is_in_su trace in
   List.map (cycle_elt isSuUsed dchit busTaken wbFull trace) trace.
 
-Definition compare_two (e1 e2 : option instr_kind) :=
-  match e1, e2 with
-  | None, _
-  | _, None => false
-  | Some (_, st1), Some (_, st2) => state_leb st1 st2
-  end.
-
 Section can_advance.
   Variable isSuUsed dchit busTaken wbFull : bool.
   Variable n : nat.