Small extra result on JMeq vs eq_dep.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12540 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 0 deletions

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 83edf434e..fc4555a4a 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -125,6 +125,20 @@ assert (true=false) by (destruct H; reflexivity).
 discriminate.
 Qed.
 
+(** However, when the dependencies are equal, [JMeq (P p) x (P q) y]
+    is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *)
+
+Lemma JMeq_eq_dep : 
+  forall U (P:U->Prop) p q (x:P p) (y:P q), 
+  p = q -> JMeq x y -> eq_dep U P p x q y.
+Proof.
+intros.
+destruct H.
+apply JMeq_eq in H0 as ->.
+reflexivity.
+Qed.
+
+
 (* Compatibility *)
 Notation sym_JMeq := JMeq_sym (only parsing).
 Notation trans_JMeq := JMeq_trans (only parsing).