From d7abadbef61ab0d45ffc5a5a45ff31bd39103446 Mon Sep 17 00:00:00 2001 From: Abhishek Anand Date: Sun, 11 Dec 2016 11:59:33 -0500 Subject: strengthened the statement of JMeq_eq_dep because P:U->Prop implies P:U->Type, the new statement is strictly more useful. No change was needed to the proof. --- theories/Logic/JMeq.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Logic') diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 2f95856b4..86d05e8fb 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -130,7 +130,7 @@ Qed. 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), + forall U (P:U->Type) p q (x:P p) (y:P q), p = q -> JMeq x y -> eq_dep U P p x q y. Proof. intros. -- cgit v1.2.3