1 files changed, 6 insertions, 0 deletions
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.