3 files changed, 31 insertions, 4 deletions
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 6e3da423e8..04e3981001 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -42,6 +42,8 @@ For the first one we provide explicit and short proof terms. *)
 
 (* Direct version *)
 
+Require Import Arith.
+
 Section ConstructiveIndefiniteGroundDescription_Direct.
 
 Variable P : nat -> Prop.
@@ -84,14 +86,38 @@ Definition constructive_indefinite_ground_description_nat :
   (exists n, P n) -> {n:nat | P n} :=
   fun e => linear_search O (let (n, p) := e in O_witness n (stop n p)).
 
+Fixpoint linear_search_smallest (start : nat) (pr : before_witness start) :
+  forall k : nat, start <= k < proj1_sig (linear_search start pr) -> ~P k.
+Proof.
+  (* Recursion on pr, which is the distance between start and linear_search *)
+  intros. destruct (P_dec start) eqn:Pstart.
+  - (* P start, k cannot exist *)
+    intros. assert (proj1_sig (linear_search start pr) = start).
+    { unfold linear_search. destruct pr; rewrite -> Pstart; reflexivity. }
+    rewrite -> H0 in H. destruct H. apply (le_lt_trans start k) in H1.
+    apply lt_irrefl in H1. contradiction. assumption.
+  - (* ~P start, step once in the search and use induction hypothesis *)
+    destruct pr. contradiction. destruct H. apply le_lt_or_eq in H. destruct H.
+    apply (linear_search_smallest (S start) pr). split. assumption.
+    simpl in H0. rewrite -> Pstart in H0. assumption. subst. assumption.
+Defined.
+
+Definition epsilon_smallest :
+  (exists n : nat, P n)
+  -> { n : nat | P n /\ forall k : nat, k < n -> ~P k }.
+Proof.
+  intros. pose (wit := (let (n, p) := H in O_witness n (stop n p))).
+  destruct (linear_search 0 wit) as [n pr] eqn:ls. exists n. split. assumption. intros.
+  apply (linear_search_smallest 0 wit). split. apply le_0_n.
+  rewrite -> ls. assumption.
+Qed.
+
 End ConstructiveIndefiniteGroundDescription_Direct.
 
 (************************************************************************)
 
 (* Version using the predicate [Acc] *)
 
-Require Import Arith.
-
 Section ConstructiveIndefiniteGroundDescription_Acc.
 
 Variable P : nat -> Prop.
diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v
index 02c8998a8d..a70bd92329 100644
--- a/theories/Logic/ExtensionalityFacts.v
+++ b/theories/Logic/ExtensionalityFacts.v
@@ -40,6 +40,7 @@ Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g
 
 (** The diagonal over A and the one-one correspondence with A *)
 
+#[universes(template)]
 Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }.
 
 Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 25b7811417..3914f44a2c 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -31,7 +31,7 @@ Arguments JMeq_refl {A x} , [A] x.
 Register JMeq as core.JMeq.type.
 Register JMeq_refl as core.JMeq.refl.
 
-Hint Resolve JMeq_refl.
+Hint Resolve JMeq_refl : core.
 
 Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
 
@@ -42,7 +42,7 @@ Proof.
 intros; destruct H; trivial.
 Qed.
 
-Hint Immediate JMeq_sym.
+Hint Immediate JMeq_sym : core.
 
 Register JMeq_sym as core.JMeq.sym.