From 5f4a8ef2cd2a8ad965366530bef9e793337b023b Mon Sep 17 00:00:00 2001
From: vsiles
Date: Wed, 26 Sep 2007 15:12:17 +0000
Subject:  added a lemma to prove inj_pair2 when eq_dec is available.

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

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index ba183b1f85..1943c16298 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -303,3 +303,15 @@ Module DecidableEqDepSet (M:DecidableSet).
   Notation inj_pairT2 := inj_pair2.
 
 End DecidableEqDepSet.
+
+  (** From decidability to inj_pair2 **)
+Lemma inj_pair2_eq_dec : forall A:Type, (forall x y:A, {x=y}+{x<>y}) ->
+   ( forall (P:A -> Type) (p:A) (x y:P p), existT P p x = existT P p y -> x = y ).
+Proof. 
+  intros A eq_dec.
+  apply eq_dep_eq__inj_pair2.
+  apply eq_rect_eq__eq_dep_eq.
+  unfold Eq_rect_eq. 
+  apply eq_rect_eq_dec.
+  apply eq_dec.
+Qed.
-- 
cgit v1.2.3