definitions: prove that stage_beq s s = true

This may become useful for subsequent proofs.

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

src/definitions.v

@@ -21,6 +21,11 @@ Variant stage :=
 
 Scheme Equality for stage.
 
+Lemma stage_beq_eq_true : forall s, stage_beq s s = true.
+Proof.
+  now destruct s.
+Qed.
+
 Definition nstg s opc :=
   match s, opc with
   | Sp, _ => Lsu