From 6f91dbd3218761e3ecc2ef634121ab643cefff57 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 24 Nov 2009 17:22:52 +0000
Subject: 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
---
 theories/Logic/JMeq.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 83edf434e9..fc4555a4ad 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).
-- 
cgit v1.2.3