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

---
 kvx/SelectOpproof.v | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'kvx/SelectOpproof.v')

diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 0de9f51f..8c834de5 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1533,12 +1533,6 @@ Proof.
   apply Val.swap_cmplu_bool.
 Qed.
 
-Lemma if_same : forall {T : Type} (b : bool) (x : T),
-    (if b then x else x) = x.
-Proof.
-  destruct b; trivial.
-Qed.
-
 Theorem eval_select: 
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
-- 
cgit