From 78d21033969bf8ed91104f5382473dd66ce185d4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Mar 2017 21:15:45 +0100
Subject: Adding f_equal_dep in Logic.v.

---
 theories/Init/Logic.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 9d60cf54c3..67cbd5d0f7 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -406,6 +406,19 @@ End EqNotations.
 
 Import EqNotations.
 
+Section equality_dep.
+  Variable A : Type.
+  Variable B : A -> Type.
+  Variable f : forall x, B x.
+  Variables x y : A.
+
+  Theorem f_equal_dep : forall (H: x = y), rew H in f x = f y.
+  Proof.
+    destruct H; reflexivity.
+  Defined.
+
+End equality_dep.
+
 Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
 Proof.
 intros.
-- 
cgit v1.2.3