diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-14 12:36:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-15 18:15:52 +0200 |
| commit | 6afdf9bd419e0353924789c6c0d5d92ecdae2f46 (patch) | |
| tree | ad8a5efbcadd128382c83a999faa88d5f8308a57 /theories/Logic | |
| parent | ec94edf830ff9676c43c86f0eb9038c4bd205f62 (diff) | |
Some basics facts about eq_dep.
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 2f61e0e29..653f0b9b4 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -440,3 +440,25 @@ 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). +Proof. +intros * []. reflexivity. +Qed. + +Lemma eq_dep_non_dep : + forall U P p q x y, @eq_dep U (fun _ => P) p x q y -> x = y. +Proof. +intros * []. reflexivity. +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. +Proof. +intros * []. reflexivity. +Qed. |