diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 11:23:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 11:23:46 +0000 |
| commit | 9075978130301e2bc71b46b7ef7bd34cf5cc076b (patch) | |
| tree | 60f597222bc4fe5aa4cf8bed167dc5b18d9ae80c /theories/Logic/JMeq.v | |
| parent | dbdaa57106427ed61d4eff967e0295979ce9a0bf (diff) | |
Renommage K; equivalence JMeq et eq_dep sur Type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3879 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/JMeq.v')
| -rw-r--r-- | theories/Logic/JMeq.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 47a20a63d..04c62b3a1 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -46,3 +46,19 @@ Qed. Lemma JMeq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x). Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial. Qed. + +(** [JMeq] is equivalent to [(eq_dep Set [X]X)] *) + +Require Eqdep. + +Lemma JMeq_eq_dep : (A,B:Set)(x:A)(y:B)(JMeq x y)->(eq_dep Set [X]X A x B y). +Proof. +NewDestruct 1. +Apply eq_dep_intro. +Qed. + +Lemma eq_dep_JMeq : (A,B:Set)(x:A)(y:B)(eq_dep Set [X]X A x B y)->(JMeq x y). +Proof. +NewDestruct 1. +Apply JMeq_refl. +Qed. |