From 4deb1b6e9da9592ada2c4ea527066dbe496901ab Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:15:50 +0200
Subject: [PATCH] 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 | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/definitions.v b/src/definitions.v
index 34e7527..1e934bc 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
-- 
GitLab