diff --git a/src/definitions.v b/src/definitions.v
index 34e7527b6c52e16a63b888f5f73c17423617c711..1e934bc811da49b755961764c1d668b0dbe69ee9 100644
--- a/src/definitions.v
+++ b/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