From 6afdf9bd419e0353924789c6c0d5d92ecdae2f46 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Jul 2014 12:36:30 +0200
Subject: Some basics facts about eq_dep.

---
 theories/Logic/EqdepFacts.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 2f61e0e297..653f0b9b4e 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.
-- 
cgit v1.2.3