From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 theories/Vectors/VectorSpec.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'theories/Vectors/VectorSpec.v')

diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index a576315e..2f4086e5 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -16,6 +16,12 @@ Require Fin.
 Require Import VectorDef.
 Import VectorNotations.
 
+Definition cons_inj A a1 a2 n (v1 v2 : t A n)
+ (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 :=
+   match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1
+   with | eq_refl => conj eq_refl eq_refl
+   end.
+
 (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
 is true for the one that use [lt] *)
 
-- 
cgit v1.2.3