1 files changed, 22 insertions, 0 deletions
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
index 1a12ac82..4610f346 100644
--- a/contrib/subtac/FunctionalExtensionality.v
+++ b/contrib/subtac/FunctionalExtensionality.v
@@ -1,3 +1,11 @@
+Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+Qed.
+
 Axiom fun_extensionality : forall A B (f g : A -> B), 
   (forall x, f x = g x) -> f = g.
 
@@ -23,3 +31,17 @@ Proof.
   apply (fun_extensionality_dep _ _ _ _ H).
   rewrite H0 ; auto.
 Qed.
+
+Lemma fix_sub_measure_eq_ext :
+  forall (A : Type) (f : A -> nat) (P : A -> Type)
+    (F_sub : forall x : A, (forall  {y : A | f y < f x}, P (`y)) -> P x),
+    forall x : A,
+      Fix_measure_sub A f P F_sub x =
+        F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)).
+Proof.
+  intros ; apply Fix_measure_eq ; auto.
+  intros.
+  assert(f0 = g).
+  apply (fun_extensionality_dep _ _ _ _ H).
+  rewrite H0 ; auto.
+Qed.