diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-17 15:08:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-17 15:15:23 +0200 |
| commit | 39e8010bf51b687f11d04c6a44cb959e85e86f7b (patch) | |
| tree | cc261c514591b9414d72006e33fcb7e6a884dfbf /theories/Logic/EqdepFacts.v | |
| parent | 293a84d36f7f2610efa4451d965684708cc6b8f3 (diff) | |
Completing c236b51348d2 by fixing EqdepFactsv actually committing the
new files (WeakFan.v and WKL.v).
Diffstat (limited to 'theories/Logic/EqdepFacts.v')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 653f0b9b4..4dfe99504 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -438,14 +438,11 @@ Notation inj_pairT2 := inj_pair2. End EqdepTheory. -Arguments eq_dep U P p x q _ : clear implicits. -Arguments eq_dep1 U P p x q y : clear implicits. - (** Basic facts about eq_dep *) Lemma f_eq_dep : forall U (P:U->Type) R p q x y (f:forall p, P p -> R p), - eq_dep x y -> eq_dep (f p x) (f q y). + eq_dep p x q y -> eq_dep p (f p x) q (f q y). Proof. intros * []. reflexivity. Qed. @@ -458,7 +455,10 @@ Qed. Lemma f_eq_dep_non_dep : forall U (P:U->Type) R p q x y (f:forall p, P p -> R), - eq_dep x y -> f p x = f q y. + eq_dep p x q y -> f p x = f q y. Proof. intros * []. reflexivity. Qed. + +Arguments eq_dep U P p x q _ : clear implicits. +Arguments eq_dep1 U P p x q y : clear implicits. |