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

---
 lib/Coqlib.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lib')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 02c5d07f..16d880fa 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -1325,3 +1325,9 @@ Lemma nlist_forall2_imply:
 Proof.
   induction 1; simpl; intros; constructor; auto.
 Qed.
+
+Lemma if_same : forall {T : Type} (b : bool) (x : T),
+    (if b then x else x) = x.
+Proof.
+  destruct b; trivial.
+Qed.
-- 
cgit