diff --git a/src/definitions.v b/src/definitions.v
index b1f10eb2a1684106786d65818f170227f6bb5177..69261dfdd96f094fb165e5c44601c7de295fdbbf 100644
--- a/src/definitions.v
+++ b/src/definitions.v
@@ -150,6 +150,12 @@ Qed.
 Definition instr_kind := (opcode * state)%type.
 Definition trace_kind := list instr_kind.
 
+(* Lemma for comparison. *)
+Lemma instr_kind_is_comparable : forall (e e' : instr_kind), (e = e') \/ (e <> e').
+Proof.
+  repeat decide equality.
+Qed.
+
 (* 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) :=