diff options
| author |  vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-26 15:12:17 +0000 |
|---|---|---|
| committer | vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-26 15:12:17 +0000 |
| commit | 5f4a8ef2cd2a8ad965366530bef9e793337b023b (patch) | |
| tree | f53a5b4c2f7650a19cb844fa4c9eae5624821484 /theories/Logic/Eqdep_dec.v | |
| parent | d0ca084ce6e466c68e3c6288cd7da67411154d6e (diff) | |
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
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index ba183b1f8..1943c1629 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. |