From ba09fcb015b19e083d64f901d11381feee2c033e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 28 Dec 2006 21:05:12 +0000
Subject: Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à
 égalité décidable + maj dépendances

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/Eqdep_dec.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'theories/Logic')

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index e491a4d5c9..b45aa23fe8 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -158,6 +158,13 @@ Proof.
   apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)).
 Qed.
 
+(** We deduce the injectivity of dependent equality for decidable types *)
+Theorem eq_dep_eq_dec :
+  forall A:Type,
+    (forall x y:A, {x = y} + {x <> y}) ->
+     forall (P:A->Type) (p:A) (x y:P p), eq_dep A P p x p y -> x = y.
+Proof (fun A eq_dec => eq_rect_eq__eq_dep_eq A (eq_rect_eq_dec eq_dec)).
+
 Unset Implicit Arguments.
 
 (************************************************************************)
-- 
cgit v1.2.3