definitions: instr_kinds are either the same or different

This proves that instr_kinds are either the same or different.  As the
monotonicity proof is splitted in two case, one where two instrs are the
same, and one where two instrs are different, this will be useful to
reunite them.

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

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) :=