From 1cf17f44b8389754d99535df800186177b394f0c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 9 Oct 2020 14:35:38 +0200
Subject: centralize if_same

---
 backend/CSE3proof.v | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 6e489066..3fbc9912 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -443,12 +443,6 @@ Ltac IND_STEP :=
         idtac mpc mpc' fn minstr *)
       end.
 
-Lemma if_same : forall {T : Type} (b : bool) (x : T),
-    (if b then x else x) = x.
-Proof.
-  destruct b; trivial.
-Qed.
-
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 -> 
   forall S1', match_states S1 S1' ->
-- 
cgit