From b77120e7e57b40fef00dcd82f9d5642580c3a1cb Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Wed, 18 Dec 2024 22:48:34 +0100
Subject: [PATCH] especialize now must ecplicitely cite created evars.

Still looking for a way to have a "default mode" where all variables
needed to *type* the premised to be proved are evarized.

For not we do

especialize X with x,y,z at 1,2,3.

And we get errors if we forget a variable.
---
 Demo/demo.v                 |  21 +-
 LibHyps/LibEspecialize.v    | 852 ++++++++++++++++++++++++++----------
 LibHyps/LibHypsRegression.v | 697 +++++++++++++++++++++--------
 LibHyps/LibHypsTactics.v    |  29 +-
 LibHyps/LibSpecialize.v     | 774 ++++++++++++++++++++++++++++----
 _CoqProject                 |   1 +
 configure.sh                |   2 +-
 7 files changed, 1850 insertions(+), 526 deletions(-)

diff --git a/Demo/demo.v b/Demo/demo.v
index 8493ecf..27dd326 100644
--- a/Demo/demo.v
+++ b/Demo/demo.v
@@ -60,7 +60,7 @@ Proof.
   (* Revert any new hyp. Must be older fist. *)
   intros.
   revert x H H6.
-  induction x ; {< (fun h => revert dependent h) }.
+  induction x ; {< (fun h => generalize dependent h) }.
   Undo.
   (* Shortcut *)
   induction x /r.
@@ -79,7 +79,7 @@ Proof.
   Undo.
   (* combination: try subst and revert remaining hyps. *)
   intros x b1.
-  intros ; { subst_or_idtac } ; {< (fun h => revert dependent h) }.
+  intros ; { subst_or_idtac } ; {< (fun h => generalize dependent h) }.
   Undo.
   intros /s/r.
   Undo 2.
@@ -128,28 +128,28 @@ Proof.
      instantiated. *)
   Undo.
   (* THIS IS BROKEN IN COQ 8.18 *)
-  (* especialize H3 at 1.
+  especialize H3 with p at 1.
   { apply le_S.
     apply le_n. }
-  Undo 5. *)
+  Undo 5.
   (* IDEs don't like Undo, replay the next ocommand twice will resync
      proofgeneral. *)
   (* It accepts several (up to 7) premisses numers. *)
   (* BROKEN IN 8.18 *)
-  (* especialize H3 at 2,3.
-  Undo. *)
+  especialize H3 with n,m,p at 2,3.
+  Undo.
 
   (* you can ask a goal for all premisses, in the spirit of the
      "exploit" tactic from CompCert. *)
   (* BROKEN IN 8.18 *)
-  (* especialize H3 at *.
-  Undo. *)
+  especialize H3 with  n,m,p at *.
+  Undo.
   
   (* You can also specify that you want to instantiate the n first premisses. *)
   (* BROKEN IN 8.18 *)
-  (* especialize H3 until 3.
+  especialize H3 with n,m,p until 3.
   Show 4.
-  Undo. *)
+  Undo.
 
   (* VARIABLES MIXED WITH HYPOTHESIS. *)
   (* move_up_types X. moves X at top near something of the same type,
@@ -198,7 +198,6 @@ Proof.
   (* experimental: (setq coq-libhyps-intros t) *)
   Undo 2.
   Show.
-  
   Restart.
   Show.
   (* Again, better combine it with "; { }". *)
diff --git a/LibHyps/LibEspecialize.v b/LibHyps/LibEspecialize.v
index b761523..d4a1d9a 100644
--- a/LibHyps/LibEspecialize.v
+++ b/LibHyps/LibEspecialize.v
@@ -1,14 +1,33 @@
+
+Require Import LibHyps.LibHypsTactics.
+
+(* debug *)
+Module Prgoal_Notation.
+  Ltac pr_goal :=
+    match goal with
+      |- ?g =>
+        let allh := harvest_hyps revert_clearbody_all in
+        (* let allh := all_hyps in *)
+        idtac allh " ⊢ " g
+    end.
+End Prgoal_Notation.
+
 Require Import Arith.
 (* The tactics in this file use the folowing pattern, that consists in
    refining a new evar goal until being in the right scope to prove
    the premise. *)
-(* 
+(*
 Lemma foo: forall x y : nat, (forall n m p :nat, n < m -> n <= m -> p > 0 -> False) -> False.
 Proof.
   intros x y H. 
   (* On veut prouver le n <= m comme conséquence du n < m dans H. *)
   (* On crée un but dont le type n'est pas connu, et on raffine pour
      être dans le bon environnement. *)
+
+  assert (forall n m p : nat, n < m -> n <= m).
+  { admit. }
+  pose proof (fun (n m p : nat) (h:n < m) => (H n m p h (H0 n m p h))).
+
   let ev := open_constr:(_) in
   assert (ev) as h.
   { refine (fun (n m p:nat) (h:n < m) => _).
@@ -21,256 +40,625 @@ Admitted.
 
 (* Describing how each arg of a hypothesis must be treated: either
    requantify it, or evarize it, or requantify but don't use it in
-   premise proofs (not sure this is needed). We don't use list for
-   cosmetic reasons: no need for nil (since the list is non empty),
-   and avoid using lists. *)
+   premise proofs (not sure this is needed) finally make it a subgoal.
+   We don't use list for cosmetic reasons: no need for nil (since the
+   list is non empty). *)
 Inductive spec_args : Type :=
-  ConsQuantif: spec_args -> spec_args
-| ConsEvar: spec_args -> spec_args
-| ConsIgnore: spec_args -> spec_args
-| ConsSubGoal: spec_args -> spec_args
-| SubGoalEnd: spec_args.
+  ConsQuantif: spec_args -> spec_args (* re-quantify *)
+| ConsEvar: spec_args -> spec_args    (* make it an evar *)
+| ConsIgnore: spec_args -> spec_args  (* gnore it (useless?) *)
+| ConsSubGoal: spec_args -> spec_args (* make it a subgoal *)
+| SubGoalEnd: spec_args.              (* make it a subgoal, end of list. *)
 
-(* List storing heterogenous terms, for storing (tele(scopes). A
-   simple product could also be used. *)
-Inductive Depl :=
-| DNil: Depl
-| DCons: forall (A:Type) (x:A), Depl -> Depl.
 
-Declare Scope specialize_scope.
-Delimit Scope specialize_scope with spec.
-Local Open Scope specialize_scope.
+Inductive int_spec_args: Type :=
+| ConsEVAR: nat -> int_spec_args -> int_spec_args
+| ConsGOAL: nat -> int_spec_args -> int_spec_args
+| FinalGOAL: nat -> int_spec_args.
 
 
-(* builds the application of c to each element of l (in reversed
+Declare Scope especialize_scope.
+Delimit Scope especialize_scope with espec.
+(* Local Open Scope especialize_scope. *)
+
+Declare Scope especialize_using_scope.
+Delimit Scope especialize_using_scope with euspec.
+(* Local Open Scope especialize_using_scope. *)
+
+Module SpecNotation.
+
+  Infix "?::" := ConsEVAR (at level 60, right associativity) : especialize_scope.
+  Infix "#::" := ConsGOAL (at level 60, right associativity) : especialize_scope.
+  Notation "## X" := (FinalGOAL X) (at level 60) : especialize_scope.
+
+  Notation "! X" := (ConsQuantif X) (at level 100) : especialize_using_scope.
+  Notation "? X" := (ConsEvar X) (at level 100) : especialize_using_scope.
+  Notation "# X" := (ConsSubGoal X) (at level 100) : especialize_using_scope.
+  Notation "##" := (SubGoalEnd) (at level 100) : especialize_using_scope.
+
+  Ltac interp_num min l :=
+    lazymatch l with
+      nil => fail
+    | FinalGOAL ?min' =>
+        match min with
+          min' => constr:(SubGoalEnd)
+        | _ => 
+            let lres := interp_num (S min) l in
+            constr:(ConsQuantif lres)
+        end
+    | ConsGOAL ?min' ?l' =>
+        match min with
+          min' =>
+            let lres := interp_num (S min) l' in
+            constr:(ConsSubGoal lres)
+        | _ => 
+            let lres := interp_num (S min) l in
+            constr:(ConsQuantif lres)
+        end
+    | ConsEVAR ?min' ?l' =>
+        match min with
+          min' =>
+            let lres := interp_num (S min) l' in
+            constr:(ConsEvar lres)
+        | _ => 
+            let lres := interp_num (S min) l in
+            constr:(ConsQuantif lres)
+        end
+    end.
+
+End SpecNotation.
+Import SpecNotation.
+
+  (* builds the application of c to each element of l (in reversed
    order). apply t [t1;t2;t3] => (t t3 t2 t1) *)
-Ltac list_apply c l :=
-  match l with
-    DNil => c
-  | DCons _ ?x ?l' =>
-      let inside := list_apply c l' in
-      let res := constr:(ltac:(exact (inside x))) in
-      res
-  end.
-
-(* - We start from a goal evar EV with no typing constraint.
-
-    h: forall x y z, P x -> ...
-    ========================
-    ?EV
-
-    subgoal 2
-    h: forall x y z, P x -> ...
-    ========================
-    old goal
-    
-
-  - We refine is to have the same products at head than h, until we
-    reach the aimed hypothesis
-
-    h: P x -> ...
-    x: ...   y: ...   z: ...
-    ========================
-    ?EV
-
-  - then we do 2 things
-    - create a goal USERGOAL for this hyp
-    - conclude EV (and fix its type) by applying h to USERGOAL
-
-    subgoal 1
-    x: ...   y: ...   z: ...
-    ==========================
-    P x
-
-    subgoal 2:
-    h: forall x y z, P x -> ...
-    hEV: forall x y z, ...
-    ==========================
-    old goal
-
-   Refines a non specified goal (an evar) to prove the specialized
-   version of h. The idea is to use (fun x y z => (?ev x y z)) as the
-   argument being instnaciated, where ?ev will be the new goal
-
- larg is the specidication of what to do with each arg, larg2 is the
-   accumulator *)
-Ltac refine_hd h largs largs2 :=
-  match largs with
-  | SubGoalEnd => match type of h with
-                  | (forall x:?t, _) =>
-                      let h' := fresh h in
-                      (* create the user subgoal *)
-                      assert(t) as h'
-                      ;[ clear h
-                       | exact (h h')
-                         (*let res := list_apply h' largs2 in
-                  exact (h res) *) ]  
-                  end
-  | ConsQuantif ?largs' => 
-      match type of h with
-      | (forall x:?t, _) =>
-          (* let y:= fresh x in *)
-          (* intro y; *)
-          refine (fun x: t => _);
-          specialize (h x);
-          refine_hd h largs' constr:(DCons _ x largs2)
-      end
-  | ConsEvar ?largs' => 
-      match type of h with
-      | (forall x:?t, _) =>
-          (* morally this evar is of type t, don't know how to enforce this
-             without having an ugly cast in goals *)
-          let ev1 := open_constr:(_:t) in
-          refine (let x:= ev1 in _);
-          specialize (h x);
-          subst x;
-          refine_hd h largs' largs2
-      end
-  | ConsSubGoal?largs' => match type of h with
-                          | (forall x:?t, _) =>
-                              let h' := fresh h in
-                              (* create the user subgoal *)
-                              assert(t) as h'
-                              ;[ clear h
-                               | exact (h h')
-                                 (*let res := list_apply h' largs2 in
-                                   exact (h res) *) ]   
-                          end
-  end.
-
-(* Precondition: name is already fresh *)
-Global Ltac espec_gen H l name :=
-  (* let l := eval cbn [spec_interp] in (spec_interp args) in   *)
-  (* let h := fresh name in *)
-  (* morally this evar is of type Type, don't know how to enforce this
+  Ltac list_apply c l :=
+    match l with
+      DNil => c
+    | DCons _ ?x ?l' =>
+        let inside := list_apply c l' in
+        let res := constr:(ltac:(exact (inside x))) in
+        res
+    end.
+
+  Ltac refine_hd h largs :=
+    match largs with
+    | SubGoalEnd =>
+        match type of h with
+        | (forall x:?t, _) =>
+            (* create the user subgoal *)
+            let x' := fresh x in
+            unshelve (evar(x':t); exact (h x'))
+        end
+    | ConsQuantif ?largs' => 
+        match type of h with
+        | (forall x:?t, _) =>
+            let x':= fresh x in
+            refine (fun x': t => _);
+            specialize (h x');
+            refine_hd h largs'
+        end
+    (* Fallback to evar creation *)
+    (* | ConsQuantif ?largs' => refine_hd h (ConsEvar largs') *)
+    | ConsEvar ?largs' => 
+        match type of h with
+        | (forall x:?t, _) =>
+            let x' := fresh x in
+            evar(x':t);
+            specialize (h x');
+            subst x';
+            refine_hd h largs'
+        end
+    | ConsSubGoal ?largs' =>
+        match type of h with
+        | (forall x:?t, _) =>
+            let x' := fresh x in
+            unshelve (evar(x':t));[
+                clear h 
+              | specialize (h x');
+                refine_hd h largs']
+        end
+    end.
+
+
+  Ltac refine_premise_hd h largs :=
+    match largs with
+    | SubGoalEnd =>
+        match type of h with
+        | (forall x:?t, _) =>
+            (* create the user subgoal *)
+            let x' := fresh x in
+            unshelve (evar(x':t); exact x')
+        end
+    | ConsQuantif ?largs' => 
+        match type of h with
+        | (forall x:?t, _) =>
+            let x':= fresh x in
+            refine (fun x': t => _);
+            specialize (h x');
+            refine_premise_hd h largs'
+        end
+    (* Fallback to evar creation *)
+    (* | ConsQuantif ?largs' => refine_premise_hd h (ConsEvar largs') *)
+    | ConsEvar ?largs' => 
+        match type of h with
+        | (forall x:?t, _) =>
+            let x' := fresh x in
+            evar(x':t);
+            specialize (h x');
+            subst x';
+            refine_premise_hd h largs'
+        end
+    | ConsSubGoal ?largs' =>
+        match type of h with
+        | (forall x:?t, _) =>
+            let x' := fresh x in
+            unshelve (evar(x':t));[
+                clear h 
+              | specialize (h x');
+                refine_premise_hd h largs']
+        end
+    end.
+
+
+  (* Precondition: name is already fresh *)
+  Global Ltac espec_gen H l name :=
+    (* morally this evar is of type Type, don't know how to enforce this
      without having an ugly cast in goals *)
-  let ev1 := open_constr:(_) in
-  assert ev1 as name
-  ; [
-      (refine_hd H l DNil)
-    | ].
-  
-Global Ltac especialize_clear H args :=
-  let temp := fresh H "temp" in
-  espec_gen H args temp;
-  [ | clear H;
-      idtac "ICI: " temp;
-      rename temp into H ].
+    let ev1 := open_constr:(_) in
+    assert ev1 as name
+    ; [
+        (refine_hd H l)
+      | ].
+
+  Global Ltac eprem_gen H l name :=
+    (* morally this evar is of type Type, don't know how to enforce this
+     without having an ugly cast in goals *)
+    let ev1 := open_constr:(_) in
+    assert ev1 as name
+    ; [
+        (refine_premise_hd H l)
+      | ].
 
-Global Ltac especialize_autoname H args :=
-  let name := fresh H "_inst" in
-  espec_gen H args name.
 
-Global Ltac especialize_clear_autoname H args :=
-  let name := fresh H "_inst" in
-  especialize_autoname H args name.
+  Ltac fresh_unfail H :=
+    match constr:(True) with
+    | _ => fresh H
+    | _ => fresh "H_"
+    end.
+  Global Ltac especialize_clear H args :=
+    (is_var H ; 
+     let temp := fresh_unfail H in
+     espec_gen H args temp; [ .. | clear H; rename temp into H ])
+    + ((assert_fails (is_var(H))) ; 
+       let tempH := fresh_unfail H in
+       specialize H as tempH;
+       let temp := fresh_unfail H in
+       espec_gen tempH args temp).
+
+
+  Global Ltac especialize_named H args name :=
+    (is_var H ; espec_gen H args name)
+    + ((assert_fails (is_var(H))) ; 
+       let tempH := fresh_unfail H in
+       specialize H as tempH;
+       espec_gen tempH args name;
+       [ .. | clear tempH ]).
+
+  Global Ltac epremise_named H args name :=
+    (is_var H ; eprem_gen H args name)
+    + ((assert_fails (is_var(H))) ; 
+       let tempH := fresh_unfail H in
+       specialize H as tempH;
+       eprem_gen tempH args name;
+       [ .. | clear tempH ]).
+
+
+  Global Ltac especialize_autoname H args :=
+    let name := fresh_unfail H in
+    espec_gen H args name.
+
+  Global Ltac especialize_clear_autoname H args :=
+    let name := fresh_unfail H in
+    (* let name := fresh name "_inst" in *)
+    especialize_autoname H args name.
+
+
+  Tactic Notation "especialize" constr(H) "using" constr(specarg) "as" ident(idH) :=
+    especialize_named H specarg idH.
+
+  Tactic Notation "especialize" constr(H) "using" constr(specarg) :=
+    especialize_clear H specarg.
+
+  (* TODO *)
+  Tactic Notation "especialize" constr(H) "using" constr(specarg) ":" ident(hprem) :=
+    especialize_clear H specarg.
+
+  Tactic Notation "assert" "premises" constr(H) "at" constr(specarg) "as" ident(idH) :=
+    let specarg' := SpecNotation.interp_num 1%nat specarg in
+    epremise_named H specarg' idH.
+
+
+  Tactic Notation "especialize" constr(H) "at" constr(specarg) "as" ident(idH) :=
+    let specarg' := SpecNotation.interp_num 1%nat specarg in
+    especialize_named H specarg' idH.
+
+  Tactic Notation "assert" "premises" constr(H) "at" constr(specarg) :=
+    let specarg' := SpecNotation.interp_num 1%nat specarg in
+    let idH := fresh "Hprem" in
+    epremise_named H specarg' idH.
+
+  Tactic Notation "especialize" constr(H) "at" constr(specarg) :=
+    let specarg' := SpecNotation.interp_num 1%nat specarg in
+    especialize_clear H specarg'.
+
+  (* TODO *)
+  Tactic Notation "especialize" constr(H) "at" constr(specarg) ":" ident(hprem) :=
+    let specarg' := SpecNotation.interp_num 1%nat specarg in
+    especialize_clear H specarg'.
+
+
+  (* Tactic Notation "exploit" constr(H) "using" constr(specarg) "as" ident(idH) := *)
+  (* prove_premises H specarg idH. *)
+
+
+
+
+  Ltac check_var H :=
+    (is_var(H))
+    + (assert_fails(is_var(H))
+       ; fail "the term " H "is not a hypothesis. To create a new hypothesis from it, please us 'as <name>'. ").
+
 
-Module SpecNotation.
-  (* Notation "![ ]!" := DNil (format "![ ]!") : specialize_scope. *)
-  (* Notation "![ x ]!" := (DCons _ x nil) : specialize_scope. *)
-  (* Notation "![ x ; y ; .. ; z ]!" := *)
-    (* (DCons _ x (DCons _ y .. (DCons _ z DNil) ..)) *)
-      (* (format "![ '[' x ;  '/' y ;  '/' .. ;  '/' z ']' ]!") : specialize_scope. *)
-  Notation "! X" := (ConsQuantif X) (at level 100) : specialize_scope.
-  Notation "? X" := (ConsEvar X) (at level 100) : specialize_scope.
-  Notation "# X" := (ConsSubGoal X) (at level 100) : specialize_scope.
-  Notation "#" := (SubGoalEnd) (at level 100) : specialize_scope.
-Module SpecNotation.
 
-Tactic Notation "especialize" constr(H) "at" constr(specarg) "as" ident(idH) :=
-  espec_gen H specarg idH.
-Tactic Notation "especialize"  constr(specarg) "as" constr(H) "at" ident(idH) :=
-  espec_gen H specarg idH.
+  (* SPECIALIZE WITH EVAR(S) *)
+  (* Precondiion: H must already be a hyp at this point. *)
+  Ltac spec_evar H var_name :=
+    check_var(H);
+    let idt := fresh var_name "T" in
+    let id := fresh var_name in
+    evar (idt : Type);
+    evar (id : idt);
+    specialize H with (var_name := id); subst id; subst idt.
 
-Tactic Notation "especialize" constr(H) "at" constr(specarg) :=
-  especialize_clear H specarg.
+  Tactic Notation "specevar" constr(H) "at" ident(i) "as" ident(newH) :=
+    specialize H as newH;
+    spec_evar newH i.
 
+  Tactic Notation "specevar" constr(H) "at" ident(i) "as" "?" :=
+    let newH := fresh "H" in
+    specevar newH at i as newH.
 
+  Ltac create_hyp_if_necessary H :=
+    (assert_fails(is_var(H)); let newH := fresh_unfail H in specialize H as newH)
+    + idtac.
 
 
-Definition eq_one (i:nat) := i = 1.
+  (* Without a name: duplicate only if c is not a hypothesis, otherwise
+   specialize directly on H *)
+  Tactic Notation "specevar" constr(c) "at" ident(i) :=
+    create_hyp_if_necessary c;
+    spec_evar c i.
 
 
-Lemma test_espec: forall x:nat, (forall y:nat,eq_one 2 -> eq_one 3 -> eq_one y -> x=0 -> False) -> True.
+  Definition eq_one (i:nat) := i = 1.
+(*
+Module Using.
+
+Local Open Scope especialize_using_scope.
+
+Lemma test_espec: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ? ! # ##).
+  + reflexivity.
+  + reflexivity.
+  + exfalso.
+    apply h_eqone with 0.
+    * reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+Lemma test_espec': forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ? ! # ##) as h_eqonetemp.
+  + reflexivity.
+  + reflexivity.
+  + exfalso.
+    apply h_eqonetemp with 0.
+    * reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+
+Lemma test_espec2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (! ? ! ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqone with 1 0.
+    * reflexivity.
+    * reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+
+Lemma test_espec3: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
 Proof.
-  intros x h_eqone.
-  (* let nme := fresh_robust H "hh" "def" in idtac nme.Definition *)
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (! ? ? ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqone with 1.
+    * reflexivity.
+    * instantiate (z:=0). reflexivity.
+    * symmetry.
+      assumption.
+Qed.
   
-  especialize h_eqone at (?#) as newH.
-    [ admit | ].  match type of newH with (eq_one 2 -> eq_one y -> x = 0 -> False) => idtac end;
-              match type of h_eqone with forall y : nat, eq_one 2 -> eq_one 3 -> eq_one y -> x = 0 -> False => idtac end].
-  Undo.
-  especialize h_eqone at (!!#) as newH;
-    [ admit | match type of newH with (forall y : nat, eq_one 2 -> eq_one y -> x = 0 -> False) => idtac end;
-              match type of h_eqone with forall y : nat, eq_one 2 -> eq_one 3 -> eq_one y -> x = 0 -> False => idtac end].
-  Undo.
-  especialize h_eqone at (!#) as newH
-  ;[ admit
-   |  match type of newH with  forall y : nat, eq_one 3 -> eq_one y ->  x = 0 -> False => idtac end;
-        match type of h_eqone with forall y : nat, eq_one 2 -> eq_one 3 -> eq_one y -> x = 0 -> False => idtac end].
-
-  Undo.
-  especialize h_eqone at (!!!#) as newH;
-    [ admit | match type of newH with  nat -> eq_one 2 -> eq_one 3 -> x = 0 -> False => idtac end;
-                match type of h_eqone with forall y : nat, eq_one 2 -> eq_one 3 -> eq_one y -> x = 0 -> False => idtac end].
-  Undo.
-
-
-Lemma test_espec: (eq_one 2 -> eq_one 3 -> eq_one 1 -> False) -> True.
+
+Lemma test_espec4: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
 Proof.
-  intros h_eqone.
-
-
-  (* let nme := fresh_robust H "hh" "def" in idtac nme.Definition *)
-  pose (c:= !!?#).
-  pose (c:= !!?#!#).
-  especialize h_eqone at (!#) as newH;
-    [ admit | match type of newH with eq_one 2 -> eq_one 1 -> False => idtac end;
-              match type of h_eqone with  eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac end].
-  Undo.
-  especialize h_eqone at (?) as newH
-  ;[ admit
-       | match type of newH with  eq_one 3 -> eq_one 1 -> False => idtac end;
-         match type of h_eqone with  eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac end].
-
-  Undo.
-  especialize h_eqone at (!!#) as newH;
-    [ admit | match type of newH with eq_one 2 -> eq_one 3 -> False => idtac end;
-              match type of h_eqone with  eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac end].
-
-
-
-  especialize (let x:=Nat.le_antisymm in x) at 2 as hhh;
-    [ admit | match type of hhh with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end ].
-  Undo.
-
-  especialize (let x:=Nat.le_antisymm in x)as hhh at 2;
-    [ admit | match type of hhh with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end ].
-  Undo.
-
-  especialize h_eqone at 2;
-    [ admit | match type of h_eqone with eq_one 2 -> eq_one 1 -> False => idtac end].
-  Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 2;
-    [ admit | match goal with |- (_ <= _ -> _ = _) -> True => idtac | _ => fail "Test failed!" end ].
-  Undo.
-
-  especialize h_eqone as ? at 2;
-    [ admit | match type of h_eqone_spec with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
-  especialize h_eqone at 2 as ? ;
-    [ admit | match type of h_eqone_spec with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ? ? ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqone.
+    * reflexivity.
+    * instantiate (z:=0). reflexivity.
+    * symmetry.
+      assumption.
+Qed.
   
-  especialize (let x:=Nat.le_antisymm in x) as ? at 2;
-    [ admit | match type of H_spec with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 2 as ? ;
-    [ admit | match type of H_spec with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
+Lemma test_espec5: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ? ? ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqone.
+    * reflexivity.
+    * instantiate (z:=0). reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+Lemma test_espec6: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ! ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqone with 1 0.
+    * reflexivity.
+    * reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+
+Lemma test_espec7: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ! ? # ! ! ##).
+  + reflexivity.
+  + rewrite hx.
+    instantiate (z:=0).
+    reflexivity.
+  + exfalso.
+    apply h_eqone with 1.
+    * reflexivity.
+    * reflexivity.
+Qed.
+
+Lemma test_espec8: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ! ! # ! ! ##).
+  + reflexivity.
+  + subst.
+    rewrite Nat.add_comm in x2.
+    cbn in x2.
+    injection x2;intro ;assumption.
+  + exfalso.
+    apply h_eqone with 1 0.
+    * reflexivity.
+    * reflexivity.
+Qed.
+
+Lemma test_espec9: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (! ! ! # ! ! ##).
+  + subst.
+    Fail
+      (* this should fail if there are only nat hyps: *)
+      ltac:(match goal with
+            | H: ?t |- a = 1 =>
+                match t with
+                  nat => fail 1
+                | _ => idtac "remaining hyp: " H ":" t 
+                end
+            end).
+Abort.
+
+End Using. *)
+
+
+Import SpecNotation.
+  Module At.
+    Module Using.
+      Import List.ListNotations.
+      Open Scope list_scope.
+
+      Close Scope autonaming_scope.
+      Open Scope especialize_scope.
+      Lemma test_espec: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+      Proof.
+        intros x hx h_eqone.
+        (* specevar h_eqone at y. *)
+        (* especialize h_eqone at (ConsEVAR 1 (ConsEVAR 2 (ConsGOAL 4 (FinalGOAL 5)))). *)
+        assert premises h_eqone at (2?::##5) as h.
+        + reflexivity.
+        + exfalso.
+          eapply h_eqone with (z:=0);eauto.
+          subst.
+          reflexivity.
+Qed.
+
+
+
+Lemma foo: False.
+Proof.
+  (* specialize (le_sind 0) as h. *)
+  (* Set Ltac Debug. *)
+  especialize (le_sind 0)  at (1?:: ##2) as h'.
+  (* Set Ltac Debug. *)
+  especialize (le_sind 0) at (1?:: ##2) as h.  ? P.  as hh : h.
+  { admit. }
+  especialize min_l at 1 as ? : ?.
+  { apply (le_n O). }
+  
+  especialize H at 1 as hh : h.
+  { reflexivity. }
+  match type of h with False => idtac "OK" | _ => fail end.
+  assumption.
+Qed.
+*)
+
+
+Lemma test_espec2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (! ? ! ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqonetemp with 1 0.
+    * reflexivity.
+    * reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+
+Lemma test_espec3: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (! ? ? ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqonetemp with 1.
+    * reflexivity.
+    * instantiate (z:=0). reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+
+Lemma test_espec4: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ? ? ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqonetemp.
+    * reflexivity.
+    * instantiate (z:=0). reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+Lemma test_espec5: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ? ? ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqonetemp.
+    * reflexivity.
+    * instantiate (z:=0). reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+  
+Lemma test_espec6: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ! ! ##).
+  + reflexivity.
+  + exfalso.
+    apply h_eqonetemp with 1 0.
+    * reflexivity.
+    * reflexivity.
+    * symmetry.
+      assumption.
+Qed.
+
+Lemma test_espec7: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ! ? # ! ! ##).
+  + reflexivity.
+  + rewrite hx.
+    instantiate (z:=0).
+    reflexivity.
+  + exfalso.
+    apply h_eqonetemp with 1.
+    * reflexivity.
+    * reflexivity.
+Qed.
+
+Lemma test_espec8: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (? ! ! # ! ! ##).
+  + reflexivity.
+  + subst.
+    rewrite Nat.add_comm in x2.
+    cbn in x2.
+    injection x2;intro ;assumption.
+  + exfalso.
+    apply h_eqonetemp with 1 0.
+    * reflexivity.
+    * reflexivity.
+Qed.
+
+Lemma test_espec9: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  especialize h_eqone using (! ! ! # ! ! ##).
+  + subst.
+    Fail
+      (* this should fail if there are only nat hyps: *)
+      ltac:(match goal with
+            | H: ?t |- a = 1 =>
+                match t with
+                  nat => fail 1
+                | _ => idtac "remaining hyp: " H ":" t 
+                end
+            end).
+Abort.
+
+
+End At.
diff --git a/LibHyps/LibHypsRegression.v b/LibHyps/LibHypsRegression.v
index 1f7b7b1..ded8911 100644
--- a/LibHyps/LibHypsRegression.v
+++ b/LibHyps/LibHypsRegression.v
@@ -118,255 +118,559 @@ Lemma dummy: forall x y,
 Qed. 
 
 
-(* BROKEN IN 8.18 *)
-(*
 Definition eq_one (i:nat) := i = 1.
-(* eq_one is delta_reducible but I don't want it to be reduced. *)
-Lemma test_espec: (eq_one 2 -> eq_one 3 -> eq_one 1 -> False) -> True.
-Proof.
-  intros h_eqone.
-  (* let nme := fresh_robust H "hh" "def" in idtac nme.Definition *)
+Module AS.
+
+
+  Lemma test_espec: forall x:nat, x = 1 -> (x = 1 -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone at 1 .
+    + assumption.
+    + match type of h_eqone with
+        False => idtac
+      | _ => fail "test failed!"
+      end.
+      contradiction.
+  Qed.
+
+  Lemma test_espec2: forall x:nat, x = 1 -> (x = 1 -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone at 1 as h.
+    + assumption.
+    + match type of h with
+        False => idtac
+      | _ => fail "test failed!"
+      end.
+      contradiction.
+  Qed.
+
+  Lemma test_espec3: forall x:nat, x = 1 -> (x = 1 -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone at 1 as ?.
+    + assumption.
+    + match type of H with
+        False => idtac
+      | _ => fail "test failed!"
+      end.
+      contradiction.
+  Qed.
+
+  Lemma test_espec4: forall x:nat, x = 1 -> (x = 1 -> x = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone at 1,2 as ?.
+    + assumption.
+    + reflexivity.
+    + match type of H with
+        False => idtac
+      | _ => fail "test failed!"
+      end.
+      contradiction.
+  Qed.
+
+  Lemma test_espec5: forall x:nat, x = 1 -> (x = 1 -> x = x -> x = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone at 1,2,3 as ?.
+    + assumption.
+    + reflexivity.
+    + reflexivity.
+    + match type of H with
+        False => idtac
+      | _ => fail "test failed!"
+      end.
+      contradiction.
+  Qed.
 
-  especialize h_eqone as newH at 2;
-    [ admit | match type of newH with eq_one 2 -> eq_one 1 -> False => idtac end;
-              match type of h_eqone with  eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac end].
-  Undo.
-  especialize h_eqone at 2 as newH;
-    [ admit | match type of newH with eq_one 2 -> eq_one 1 -> False => idtac end;
-              match type of h_eqone with  eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac end].
-  Undo.
+  
+  Lemma test_espec_h: forall x:nat, x = 1 -> (forall a y z:nat, x = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y at 2,1 as h.
+    + reflexivity.
+    + assumption.
+    + exfalso.
+      apply h with 0.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
 
-  especialize (let x:=Nat.le_antisymm in x) at 2 as hhh;
-    [ admit | match type of hhh with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end ].
-  Undo.
 
-  especialize (let x:=Nat.le_antisymm in x)as hhh at 2;
-    [ admit | match type of hhh with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end ].
-  Undo.
+  
+  Lemma test_espec_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y at 2,1 as ?.
+    + reflexivity.
+    + reflexivity.
+    + exfalso.
+      apply H with 0.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  
+End AS.
+
+
+Module Using.
+
+  Lemma test_espec: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y at 2,1 .
+    + reflexivity.
+    + reflexivity.
+    + exfalso.
+      apply h_eqone with 0.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  
+  Lemma test_espec_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y at 2,1 as h.
+    + reflexivity.
+    + reflexivity.
+    + exfalso.
+      apply h with 0.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  
+  Lemma test_espec_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y at 2,1 as ?.
+    + reflexivity.
+    + reflexivity.
+    + exfalso.
+      apply H with 0.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  
 
-  especialize h_eqone at 2;
-    [ admit | match type of h_eqone with eq_one 2 -> eq_one 1 -> False => idtac end].
-  Undo.
+  Lemma test_espec2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with y at 2 .
+    + reflexivity.
+    + exfalso.
+      apply h_eqone with 1 0.
+      * reflexivity.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec2_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with y at 2 as h.
+    + reflexivity.
+    + exfalso.
+      apply h with 1 0.
+      * reflexivity.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec2_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with y at 2 as ?.
+    + reflexivity.
+    + exfalso.
+      apply H with 1 0.
+      * reflexivity.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  
 
-  especialize (let x:=Nat.le_antisymm in x) at 2;
-    [ admit | match goal with |- (_ <= _ -> _ = _) -> True => idtac | _ => fail "Test failed!" end ].
-  Undo.
+  Lemma test_espec3: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with y , z at 2 .
+    + reflexivity.
+    + exfalso.
+      apply h_eqone with 1.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec3_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with y , z at 2 as h.
+    + reflexivity.
+    + exfalso.
+      apply h with 1.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec3_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with y , z at 2 as ?.
+    + reflexivity.
+    + exfalso.
+      apply H with 1.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  
 
-  especialize h_eqone as ? at 2;
-    [ admit | match type of h_eqone_spec with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
-  especialize h_eqone at 2 as ? ;
-    [ admit | match type of h_eqone_spec with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
+  Lemma test_espec4: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a, y, z at 1 .
+    + reflexivity.
+    + exfalso.
+      apply h_eqone.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec4_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a, y, z at 1 as h.
+    + reflexivity.
+    + exfalso.
+      apply h.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec4_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a, y, z at 1 as ?.
+    + reflexivity.
+    + exfalso.
+      apply H.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
   
-  especialize (let x:=Nat.le_antisymm in x) as ? at 2;
-    [ admit | match type of H_spec with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
+  Lemma test_espec5: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y,z at 1 .
+    + reflexivity.
+    + exfalso.
+      apply h_eqone.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec5_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y,z at 1 as h.
+    + reflexivity.
+    + exfalso.
+      apply h.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec5_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,y,z at 1 as ?.
+    + reflexivity.
+    + exfalso.
+      apply H.
+      * reflexivity.
+      * instantiate (z:=0). reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  
+  Lemma test_espec6: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a at 1 .
+    + reflexivity.
+    + exfalso.
+      apply h_eqone with 1 0.
+      * reflexivity.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec6_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a at 1 as h.
+    + reflexivity.
+    + exfalso.
+      apply h with 1 0.
+      * reflexivity.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+  Lemma test_espec6_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a at 1 as ?.
+    + reflexivity.
+    + exfalso.
+      apply H with 1 0.
+      * reflexivity.
+      * reflexivity.
+      * symmetry.
+        assumption.
+  Qed.
+
+  Lemma test_espec7: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,z at 1,4 .
+    + reflexivity.
+    + rewrite hx.
+      instantiate (z:=0).
+      reflexivity.
+    + exfalso.
+      apply h_eqone with 1.
+      * reflexivity.
+      * reflexivity.
+  Qed.
+
+  Lemma test_espec7_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,z at 1,4 as h.
+    + reflexivity.
+    + rewrite hx.
+      instantiate (z:=0).
+      reflexivity.
+    + exfalso.
+      apply h with 1.
+      * reflexivity.
+      * reflexivity.
+  Qed.
+  Lemma test_espec7_h2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    especialize h_eqone with a,z at 1,4 as ?.
+    + reflexivity.
+    + rewrite hx.
+      instantiate (z:=0).
+      reflexivity.
+    + exfalso.
+      apply H with 1.
+      * reflexivity.
+      * reflexivity.
+  Qed.
+
+  Lemma test_espec8: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    Fail especialize h_eqone with a at 1,4 .
+  Abort.
+
+  Lemma test_espec8_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    Fail especialize h_eqone with a at 1,4 as h.
+  Abort.
+
+  Lemma test_espec8_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    Fail especialize h_eqone with a at 1,4 as ?.
+  Abort.
+
+  Lemma test_espec9: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    Fail especialize h_eqone at 1,4.
+  Abort.
+
+  Lemma test_espec9_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    Fail especialize h_eqone at 1,4 as h.
+  Abort.
+
+  Lemma test_espec9_h: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+  Proof.
+    intros x hx h_eqone.
+    Fail especialize h_eqone at 1,4 as ?.
+  Abort.
+
+End Using.
 
-  especialize (let x:=Nat.le_antisymm in x) at 2 as ? ;
-    [ admit | match type of H_spec with _ <= _ -> _ = _ => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone with eq_one 2 -> eq_one 3 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
 
-  especialize h_eqone at 2 : h;
-    [ admit | match type of h_eqone with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h with 3=1 => idtac | _ => fail "Test failed!" end].
+Lemma test_esepec_6_7: (eq_one 2 -> eq_one 3 ->eq_one 4 ->eq_one 5 ->eq_one 6 ->eq_one 7 ->eq_one 8 -> eq_one 9 -> eq_one 1 -> False) -> True.
+Proof.
+  intros H.
+  especialize H at 3,1,4,5,2,7 as h; [ admit | admit | admit  | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 2 : h;
-    [ admit | match goal with |- (_ <= _ -> _ = _) -> True => idtac | _ => fail "Test failed!" end;
-              match type of h with _ <= _ => idtac | _ => fail "Test failed!" end].
+  especialize H at 3,1,4,5,2,7; [ admit | admit | admit  | admit | admit | admit | match type of H with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac "OK" end].
+  Undo.
+  especialize H at 3,1,4,5,2,7,9 as h; [ admit | admit | admit  | admit | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
+  especialize H at 3,1,4,5,2,7,9; [ admit | admit | admit  | admit | admit | admit | admit | match type of H with eq_one 7 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  exact I.
+Qed.
 
-  especialize h_eqone at 2 : ? ;
-    [ admit | match type of h_eqone with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone_prem with 3=1 => idtac | _ => fail "Test failed!" end].
-  Undo. 
 
-  especialize (let x:=Nat.le_antisymm in x) at 2 : ? ;
-    [ admit | match goal with |- (_ <= _ -> _ = _) -> True => idtac | _ => fail "Test failed!" end;
-              match type of H_prem with _ <= _ => idtac | _ => fail "Test failed!" end].
-  Undo.
+Axiom ex_hyp : (forall (b:bool), forall x: nat, eq_one 1 -> forall y:nat, eq_one 2 ->eq_one 3 ->eq_one 4 ->eq_one x ->eq_one 6 ->eq_one y -> eq_one 8 -> eq_one 9 -> False).
 
+Lemma test_esepec: True.
+Proof.
 
-  especialize h_eqone at 2 as newH : h;
-    [ admit | match type of newH with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h with 3=1 => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) at 2 as h;[ .. | match type of h with forall x: nat, eq_one 1 -> forall y:nat, eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 2 as newH : h;
-    [ admit | match type of newH with (_ <= _ -> _ = _) => idtac | _ => fail "Test failed!" end;
-              match type of h with _ <= _ => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) at 2,3 as h;[  .. | match type of h with forall x: nat, eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone as newH at 2 : h;
-    [ admit | match type of newH with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h with 3=1 => idtac | _ => fail "Test failed!" end].
+  Fail especialize H at 2,3,5 as h. 
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) as newH at 2 : h;
-    [ admit |
-      match type of newH with (_ <= _ -> _ = _) => idtac | _ => fail "Test failed!" end;
-      match type of h with _ <= _ => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x at 2,3,5 as h ;[ ..  | match type of h with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone at 2 as ? : h;
-    [ admit | match type of h_eqone_spec with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h with 3=1 => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x at 2,3,5,6 as h ;[ ..  | match type of h with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 2 as ? : h;
-    [ admit |
-      match type of H_spec with (_ <= _ -> _ = _) => idtac | _ => fail "Test failed!" end;
-      match type of h with _ <= _ => idtac | _ => fail "Test failed!" end].
+  Fail especialize H with x at 2,3,5,7 as h.
+  especialize (ex_hyp true) with x,y at 2,3,5,7 as h ;[ ..  | match type of h with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone as ? at 2 : h;
-    [ admit | match type of h_eqone_spec with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h with 3=1 => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x,y at 2,3,5,7,9 as h ;[ ..  | match type of h with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) as ? at 2 : h;
-    [ admit |
-      match type of H_spec with (_ <= _ -> _ = _) => idtac | _ => fail "Test failed!" end;
-      match type of h with _ <= _ => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x,y at 2,3,1,5,7,9 as h ;[ ..  | match type of h with eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone at 2 as ? : ? ;
-    [ admit | match type of h_eqone_spec with eq_one 2 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end;
-              match type of h_eqone_prem with 3=1 => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x,y at 8,2,3,5,7,9 as h ;[ ..  | match type of h with eq_one 1 -> eq_one 4 -> eq_one 6 -> False => idtac "OK" end].
   Undo.
 
-  especialize (let x:=Nat.le_antisymm in x) at 2 as ? : ? ;
-    [ admit |
-      match type of H_spec with (_ <= _ -> _ = _) => idtac | _ => fail "Test failed!" end;
-      match type of H_prem with _ <= _ => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) at 2 as ?;[ .. | match type of H with forall x: nat, eq_one 1 -> forall y:nat, eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone as ? at 2 : ? ;
-    [ admit | match goal with h_eqone_spec:eq_one 2 -> eq_one 1 -> False,
-                              h_eqone_prem : 3 = 1 |- _ => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) at 2,3 as ?;[  .. | match type of H with forall x: nat, eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) as ? at 2 : ? ;
-    [ admit |
-      match type of H_spec with (_ <= _ -> _ = _) => idtac | _ => fail "Test failed!" end;
-      match type of H_prem with _ <= _ => idtac | _ => fail "Test failed!" end].
+  Fail especialize H at 2,3,5 as ?. 
   Undo.
-
-  especialize h_eqone at 2,3;
-    [ admit | admit| match type of h_eqone with eq_one 2 -> False=> idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x at 2,3,5 as ? ;[ ..  | match type of H with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 1,2;
-    [ admit | admit | match goal with |- (_ = _) -> True => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x at 2,3,5,6 as ? ;[ ..  | match type of H with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone at 3,2;
-    [ admit | admit| match type of h_eqone with eq_one 2 -> False=> idtac | _ => fail "Test failed!" end].
+  Fail especialize H with x at 2,3,5,7 as ?.
+  especialize (ex_hyp true) with x,y at 2,3,5,7 as ? ;[ ..  | match type of H with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 2,1;
-    [ admit | admit | match goal with |- (_ = _) -> True => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x,y at 2,3,5,7,9 as ? ;[ ..  | match type of H with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone as h at 2,3;
-    [ admit | admit| match type of h with eq_one 2 -> False=> idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x,y at 2,3,1,5,7,9 as ? ;[ ..  | match type of H with eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
   Undo.
-
-  especialize (let x:=Nat.le_antisymm in x) at 2,1 as h;
-    [ admit | admit | 
-      match type of h with (_ = _) => idtac | _ => fail "Test failed!" end].
+  especialize (ex_hyp true) with x,y at 8,2,3,5,7,9 as ? ;[ ..  | match type of H with eq_one 1 -> eq_one 4 -> eq_one 6 -> False => idtac "OK" end].
   Undo.
 
-  especialize h_eqone at 2,3 as h;
-    [ admit | admit| match type of h with eq_one 2 -> False=> idtac | _ => fail "Test failed!" end].
-  Undo.
+  Fail especialize (ex_hyp true) at 2.
 
-  especialize (let x:=Nat.le_antisymm in x) as h at 2,1;
-    [ admit | admit | 
-      match type of h with (_ = _) => idtac | _ => fail "Test failed!" end].
   Undo.
-
-  especialize h_eqone at 3,2,1;
-    [ admit | admit | admit |  match type of h_eqone with False=> idtac | _ => fail "Test failed!" end ].
+  generalize (ex_hyp true) as H.
+  intro.
+  especialize H at 2 as h;[ .. | match type of h with forall x: nat, eq_one 1 -> forall y:nat, eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-
-  especialize h_eqone as h at 3,2,1;
-    [ admit | admit | admit |  match type of h with False=> idtac | _ => fail "Test failed!" end ].
+  especialize H at 2,3 as h;[  .. | match type of h with forall x: nat, eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  Fail especialize H at 2,3,5 as h. 
+  Undo.
+  especialize H with x at 2,3,5 as h ;[ ..  | match type of h with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x at 2,3,5,6 as h ;[ ..  | match type of h with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  Fail especialize H with x at 2,3,5,7 as h.
+  especialize H with x,y at 2,3,5,7 as h ;[ ..  | match type of h with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x,y at 2,3,5,7,9 as h ;[ ..  | match type of h with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x,y at 2,3,1,5,7,9 as h ;[ ..  | match type of h with eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x,y at 8,2,3,5,7,9 as h ;[ ..  | match type of h with eq_one 1 -> eq_one 4 -> eq_one 6 -> False => idtac "OK" end].
   Undo.
 
-  especialize h_eqone at 3,2,1 as h;
-    [ admit | admit | admit |  match type of h with False=> idtac | _ => fail "Test failed!" end ].
+  especialize H at 2 as ?;[ .. | match type of H0 with forall x: nat, eq_one 1 -> forall y:nat, eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  especialize H at 2,3 as ?;[  .. | match type of H0 with forall x: nat, eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  Fail especialize H at 2,3,5 as ?. 
+  Undo.
+  especialize H with x at 2,3,5 as ? ;[ ..  | match type of H0 with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x at 2,3,5,6 as ? ;[ ..  | match type of H0 with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  Fail especialize H with x at 2,3,5,7 as ?.
+  especialize H with x,y at 2,3,5,7 as ? ;[ ..  | match type of H0 with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x,y at 2,3,5,7,9 as ? ;[ ..  | match type of H0 with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x,y at 2,3,1,5,7,9 as ? ;[ ..  | match type of H0 with eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x,y at 8,2,3,5,7,9 as ? ;[ ..  | match type of H0 with eq_one 1 -> eq_one 4 -> eq_one 6 -> False => idtac "OK" end].
   Undo.
-  exact I.
-Qed.
 
-Lemma foo2: (eq_one 2 -> eq_one 3 ->eq_one 4 ->eq_one 5 ->eq_one 6 -> eq_one 1 -> False) -> True.
-Proof.
-  intros h_eqone.
-  especialize h_eqone at 3,1,4,5 as h;
-    [ admit | admit | admit  | admit | match type of h with eq_one 3 -> eq_one 1 ->False=> idtac | _ => fail "Test failed!" end  ]. 
+  especialize H at 2;[ .. | match type of H with forall x: nat, eq_one 1 -> forall y:nat, eq_one 3 -> eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
+  Undo.
+  especialize H at 2,3;[  .. | match type of H with forall x: nat, eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-  especialize h_eqone as h at 3,1,4,5;
-    [ admit | admit | admit  | admit | match type of h with eq_one 3 -> eq_one 1 ->False=> idtac | _ => fail "Test failed!" end  ]. 
+  Fail especialize H at 2,3,5. 
   Undo.
-  especialize h_eqone at 3,1,4,5;
-    [ admit | admit | admit  | admit | match type of h_eqone with eq_one 3 -> eq_one 1 ->False=> idtac | _ => fail "Test failed!" end  ]. 
+  especialize H with x at 2,3,5 ;[ ..  | match type of H with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one 6 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-  especialize h_eqone at 3,1,4,5,2;
-    [ admit | admit | admit | admit  | admit | match type of h_eqone with eq_one 1 ->False=> idtac | _ => fail "Test failed!" end  ]. 
+  especialize H with x at 2,3,5,6 ;[ ..  | match type of H with eq_one 1 -> forall y:nat, eq_one 4 -> eq_one _ -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-  especialize h_eqone at 3,1,4,5,2  as h;
-    [ admit | admit | admit | admit  | admit | match type of h with eq_one 1 ->False=> idtac | _ => fail "Test failed!" end  ]. 
+  Fail especialize H with x at 2,3,5,7.
+  especialize H with x,y at 2,3,5,7 ;[ ..  | match type of H with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> eq_one 9 -> False => idtac "OK" end].
   Undo.
-  especialize h_eqone as h at 3,1,4,5,2;
-    [ admit | admit | admit | admit  | admit | match type of h with eq_one 1 ->False=> idtac | _ => fail "Test failed!" end  ]. 
+  especialize H with x,y at 2,3,5,7,9 ;[ ..  | match type of H with eq_one 1 -> eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
   Undo.
+  especialize H with x,y at 2,3,1,5,7,9 ;[ ..  | match type of H with eq_one 4 -> eq_one 6 -> eq_one 8 -> False => idtac "OK" end].
+  Undo.
+  especialize H with x,y at 8,2,3,5,7,9 ;[ ..  | match type of H with eq_one 1 -> eq_one 4 -> eq_one 6 -> False => idtac "OK" end].
+  Undo.
+
   exact I.
 Qed.
 
 
+
 Lemma test_espec_namings: forall n:nat, (eq_one n -> eq_one 1 -> False) -> True.
 Proof.
   intros n h_eqone.
-  especialize Nat.quadmul_le_squareadd at 1 as hh : h.
+  especialize Nat.quadmul_le_squareadd with a at 1 as hh : h.
   { apply le_n. }
-  especialize min_l at 1 as ? : ?.
+  especialize min_l with n,m at 1 as ?.
   { apply (le_n O). }
   especialize h_eqone at 2 as h1 : h2.
   { reflexivity. }
+  unfold eq_one in h2.
   match type of h2 with 1 = 1 => idtac | _ => fail end.
   match type of h1 with eq_one n -> False => idtac | _ => fail end.
   exact I.
 Qed.
 
-Lemma test_esepec_6_7: (eq_one 2 -> eq_one 3 ->eq_one 4 ->eq_one 5 ->eq_one 6 ->eq_one 7 ->eq_one 8 -> eq_one 9 -> eq_one 1 -> False) -> True.
-Proof.
-  intros h_eqone.
-  especialize h_eqone at 3,1,4,5,2,7 as h;
-    [ admit | admit | admit  | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac | _ => fail "Test failed!" end].
-  Undo.
-  especialize h_eqone as h at 3,1,4,5,2,7;
-    [ admit | admit | admit  | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac | _ => fail "Test failed!" end].
-  Undo.
-  especialize h_eqone at 3,1,4,5,2,7;
-    [ admit | admit | admit  | admit | admit | admit | match type of h_eqone with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac | _ => fail "Test failed!" end].
-  Undo.
-  especialize h_eqone at 3,1,4,5,2,7,9 as h;
-    [ admit | admit | admit  | admit | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
-  especialize h_eqone as h at 3,1,4,5,2,7,9;
-    [ admit | admit | admit  | admit | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
-  especialize h_eqone at 3,1,4,5,2,7,9;
-    [ admit | admit | admit  | admit | admit | admit | admit | match type of h_eqone with eq_one 7 -> eq_one 9 -> False => idtac | _ => fail "Test failed!" end].
-  Undo.
-  exact I.
-Qed.
 
 (* "until i" and "at *" *)
 
@@ -375,14 +679,26 @@ Proof.
   
   intros h_eqone.
   (* specialize on term ==> create a new hyp *)
-  especialize (let x:=not_eq_S in x) at *;
-    [ intro ; admit | match type of H_spec with (S _)<>(S _) => idtac | _ => fail "Test failed!" end].
+
+  Fail especialize (let x:=not_eq_S in x) with n,m at *.
+  especialize (let x:=not_eq_S in x) with n,m at * as h;
+    [ .. | match type of h with (S _)<>(S _) => idtac | _ => fail "Test failed!" end].
+  Undo.
+  especialize (let x:=not_eq_S in x) with n,m at * as ?;
+    [ .. | match type of H with (S _)<>(S _) => idtac | _ => fail "Test failed!" end].
+  Undo.
+  Fail especialize (let x:=not_eq_S in x) with n,m until 1.
+  especialize (let x:=not_eq_S in x) with n,m at * as h;
+    [ .. | match type of h with (S _)<>(S _) => idtac | _ => fail "Test failed!" end].
+  Undo.
+  especialize (let x:=Nat.sub_pred_r in x) with n,m until 2 as h;
+    [ .. | match type of h with ?n - Nat.pred ?m = S (?n - ?m) => idtac | _ => fail "Test failed!" end].
   Undo.
-  especialize (let x:=not_eq_S in x) at * as h;
-    [ intro ; admit | match type of h with (S _)<>(S _) => idtac | _ => fail "Test failed!" end].
+  especialize (let x:=Nat.sub_pred_r in x) with n,m until 1 as h;
+    [ .. | match type of h with ?m <= ?n -> ?n - Nat.pred ?m = S (?n - ?m) => idtac | _ => fail "Test failed!" end].
   Undo.
   especialize (let x:=h_eqone in x) at *;
-    [ admit |admit |admit |admit |admit |admit |admit |admit |admit | match type of H_spec with False => idtac | _ => fail "Test failed!" end].
+    [ ..  | match type of H_spec with False => idtac | _ => fail "Test failed!" end].
   Undo.
   (* proveprem_until h_eqone 4. *)
   especialize (let x:= h_eqone in x) until 4;
@@ -393,7 +709,7 @@ Proof.
     [ admit |admit |admit |admit | match type of h_eqone with eq_one 6 -> eq_one 7 -> eq_one 8 -> eq_one 9 -> eq_one 1 -> False => idtac | _ => fail "Test failed!" end].
   Undo.
   especialize h_eqone at * ;
-    [ admit |admit |admit |admit |admit |admit |admit |admit |admit | match type of h_eqone with False => idtac | _ => fail "Test failed!" end].
+    [ .. | match type of h_eqone with False => idtac | _ => fail "Test failed!" end].
   Undo.
   (* unless we give the "as" option *)
   especialize h_eqone at * as h ;
@@ -405,7 +721,6 @@ Proof.
   Undo.
   exact I.
 Qed.
-*)
 
 Require Import LibHyps.LibDecomp.
 
diff --git a/LibHyps/LibHypsTactics.v b/LibHyps/LibHypsTactics.v
index cf3cdb1..1fa3d27 100644
--- a/LibHyps/LibHypsTactics.v
+++ b/LibHyps/LibHypsTactics.v
@@ -4,15 +4,28 @@
 
 Require Export LibHyps.TacNewHyps.
 Require Export LibHyps.LibHypsNaming.
-(* Require Export LibHyps.LibSpecialize. *)
+Require Export LibHyps.LibSpecialize.
 
 (* debug *)
-Ltac pr_goal :=
-  match goal with
-    |- ?g =>
-      let allh := all_hyps in
-      idtac allh " ⊢ " g
-  end.
+Module Prgoal_Notation.
+  Ltac pr_goal :=
+    match goal with
+      |- ?g =>
+        let allh := all_hyps in
+        idtac "[" allh " ⊢ " g "]"
+    end.
+  Notation "X : Y ; Z" := (DCons Y X Z) (right associativity,only printing,format "'[v' X : Y ; '/' Z ']' ") .
+End Prgoal_Notation.
+
+(* example: 
+Import Prgoal_Notation.
+Lemma test_espec2: forall x:nat, x = 1 -> (forall a y z:nat, a = 1 -> y = 1 -> z+y+a = 2 -> z+1 = x -> False) -> x > 1.
+Proof.
+  intros x hx h_eqone.
+  (* specevar h_eqone at y. *)
+  pr_goal.
+pr_goal.
+Abort. *)
 
 (* Default behaviour: generalize hypothesis that we failed to rename,
    so that no automatic names are introduced by mistake. Of course one
@@ -30,7 +43,7 @@ Ltac revert_if_norename H :=
             (* since we are only in prop it is almost never the case
                that something depends on H but if this happens we revert
                everything that does. This needs testing. *)
-            | _ => try revert dependent H
+            | _ => try generalize dependent H
             end
   | _ => idtac
   end.
diff --git a/LibHyps/LibSpecialize.v b/LibHyps/LibSpecialize.v
index 2b8eb52..07ab07f 100644
--- a/LibHyps/LibSpecialize.v
+++ b/LibHyps/LibSpecialize.v
@@ -2,6 +2,46 @@
   This file is part of LibHyps. It is distributed under the MIT
   "expat license". You should have recieved a LICENSE file with it. *)
 
+(* The especialize tactic allows to create subgoals from premises of a
+   hypothesis.
+
+From a hypothesis of the form:
+
+H: forall a b c, A -> B -> C -> X
+
+one can start a goal for either A and/or B and/or C, while making
+evars for a and/pr b and/or c. Duplicating H or not.
+
+especialize H with a at 2.
+
+will start a goal GB of type B[a<-?a] and specialize H with ?a and GB.
+Changing H into:
+
+H: forall b c, A[a<-?a] -> C[a<-?a} -> X[a<-?a]
+
+Note that B must be proved without without supposing A. This tactic
+does not implement the exact logical rule (this is work in progress).
+This limitation is however not a problem in practice: if B needs A
+then the user almost always wants to prove A first.
+
+The tactic supports sevral evars and/or several sibgoals at once:
+
+especialize H with a,b at 1,2.
+etc.
+
+Special "at *" form (inspired by exploit from Compcert=::
+
+especialize H with a,b,c at *.
+
+will start goals for all premises (A, B and C in the example above).
+
+Special "until" form e.g. :
+
+especialize with a,c A until 2.
+
+will start goals for all the 2 first premises  with evars ?a, and ?c. *)
+
+
 (* proveprem H at i as h. Create an assert for the ith dependent
 premiss of hypothesis H and specialize H with the resulting proof. h
 is the (optional) name of the asserted premiss. *)
@@ -16,6 +56,12 @@ Ltac fresh_unfail H :=
     | _ => fresh "H_"
   end.
 
+Ltac fail_if_not_hyp c :=
+  (is_var(c))
+  + ((assert_fails (is_var(c)));
+     fail "especialize: please provide a name for the new hyp (with 'as')").
+
+
 Ltac proveprem_as_prem H i idpremis idnewH :=
   (* prefer this to evar, which is not well "typed" by Ltac (does not
      know that it creates an evar (coq bug?). *)
@@ -23,24 +69,21 @@ Ltac proveprem_as_prem H i idpremis idnewH :=
   assert (idpremis:ev);
   [|specialize H with (i:=idpremis) as idnewH].
 
-Tactic Notation "especialize" constr(H) "at" integer(i) "as" ident(idH) ":" ident(idprem) := proveprem_as_prem H i idprem idH.
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at" integer(i) ":" ident(idprem) := proveprem_as_prem H i idprem idH.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) "as" ident(idH) ":" ident(idprem) := proveprem_as_prem H i idprem idH.
 
 Ltac proveprem_asg_newH H i idpremis :=
   let prefx := fresh_unfail H in
   let idnewH := fresh prefx "spec" in (* FIXME: if H is not freshable? *)
   proveprem_as_prem H i idpremis idnewH.
 
-Tactic Notation "especialize" constr(H) "at" integer(i) "as" "?" ":" ident(idprem) := proveprem_asg_newH H i idprem.
-Tactic Notation "especialize" constr(H) "as" "?" "at" integer(i) ":" ident(idprem) := proveprem_asg_newH H i idprem.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) "as" "?" ":" ident(idprem) := proveprem_asg_newH H i idprem.
 
 Ltac proveprem_as_premg H i idnewH :=
   let prefx := fresh_unfail H in
   let idpremis := fresh prefx "prem" in
   proveprem_as_prem H i idpremis idnewH.
 
-Tactic Notation "especialize" constr(H) "at" integer(i) "as" ident(idH) ":" "?" := proveprem_as_premg H i idH.
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at" integer(i) ":" "?" := proveprem_as_premg H i idH.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) "as" ident(idH) ":" "?" := proveprem_as_premg H i idH.
 
 
 Ltac proveprem_asg_premg H i :=
@@ -49,16 +92,14 @@ Ltac proveprem_asg_premg H i :=
   let idpremis := fresh prefx "prem" in
   proveprem_as_prem H i idpremis idnewH.
 
-Tactic Notation "especialize" constr(H) "at" integer(i) "as" "?" ":" "?" := proveprem_asg_premg H i.
-Tactic Notation "especialize" constr(H) "as" "?" "at" integer(i) ":" "?" := proveprem_asg_premg H i.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) "as" "?" ":" "?" := proveprem_asg_premg H i.
 
 Ltac proveprem_as H i idnewH :=
   let prefx := fresh_unfail H in
   let idpremis := fresh prefx "prem" in
   proveprem_as_prem H i idpremis idnewH;[ | clear idpremis].
 
-Tactic Notation "especialize" constr(H) "at" integer(i) "as" ident(idH) := proveprem_as H i idH.
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at" integer(i) := proveprem_as H i idH.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) "as" ident(idH) := proveprem_as H i idH.
 
 
 Ltac proveprem_asg H i :=
@@ -67,9 +108,7 @@ Ltac proveprem_asg H i :=
   let idpremis := fresh prefx "prem" in
   proveprem_as_prem H i idpremis idnewH;[ | clear idpremis].
 
-Tactic Notation "especialize" constr(H) "at" integer(i) "as" "?" := proveprem_asg H i.
-Tactic Notation "especialize" constr(H) "as" "?" "at" integer(i) := proveprem_asg H i.
-
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) "as" "?" := proveprem_asg H i.
 
 
 (* Version where specialize is not given a name (soeither H is a
@@ -80,14 +119,16 @@ Ltac proveprem_prem H i idpremis :=
   assert (idpremis:ev);
   [|specialize H with (i:=idpremis)].
 
-Tactic Notation "especialize" constr(H) "at" integer(i) ":" ident(idprem) := proveprem_prem H i idprem.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) ":" ident(idprem) :=
+  fail_if_not_hyp H;
+  proveprem_prem H i idprem.
 
 Ltac proveprem_premg H i :=
   let prefx := fresh_unfail H in
   let idpremis := fresh prefx "prem" in
   proveprem_prem H i idpremis.
 
-Tactic Notation "especialize" constr(H) "at" integer(i) ":" "?" := proveprem_premg H i.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) ":" "?" := proveprem_premg H i.
 
 (* same as proveprem_prem but discard the created hypothesis once used in specialization *)
 Ltac proveprem H i :=
@@ -95,13 +136,12 @@ Ltac proveprem H i :=
   let idpremis := fresh prefx "prem" in
   proveprem_prem H i idpremis ; [ | clear idpremis].
 
-Tactic Notation "especialize" constr(H) "at" integer(i) := proveprem H i.
-Tactic Notation "especialize" constr(H) "at" integer(i) := proveprem H i.
-
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) := fail_if_not_hyp H;proveprem H i.
 
 (* Create a subgoal for each dependent premiss of H *)
 Ltac proveprem_all H := (especialize H at 1; [| proveprem_all H]) + idtac.
 
+(* TODO: make the "as" mandatory if G not a hyp. *)
 Tactic Notation "especialize" constr(H) "at" "*" :=
   ((try (is_var(H); fail 1));
    (let prefx := fresh_unfail H in
@@ -122,6 +162,7 @@ Ltac proveprem_until H i :=
   | (S ?i') => (especialize H at 1; [| proveprem_until H i'])
   end.
 
+(* TODO idem: make as mandatory *)
 Tactic Notation "especialize" constr(H) "until" constr(i) :=
   (try (is_var(H); fail 1);
    (let prefx := fresh_unfail H in
@@ -147,8 +188,7 @@ Ltac proveprem_as_2 H idnewH i1 i2 :=
     assert (idprem2:ev2);
     [|specialize H with (i1:=idprem1) (i2:=idprem2) as idnewH ; clear idprem2 idprem1]].
 
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at"  integer(i1) "," integer(i2) := proveprem_as_2 H idH i1 i2.
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2) "as" ident(idH) := proveprem_as_2 H idH i1 i2.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2) "as" ident(idH) := proveprem_as_2 H idH i1 i2.
 
 (* Same but discard the created hypothesis once used in specialization *)
 Ltac proveprem_2 H i1 i2 :=
@@ -162,7 +202,7 @@ Ltac proveprem_2 H i1 i2 :=
     assert (idprem2:ev2);
     [|specialize H with (i1:=idprem1) (i2:=idprem2) ; clear idprem2 idprem1]].
 
-Tactic Notation "especialize" constr(H) "at" integer(i1) "," integer(i2) := proveprem_2 H i1 i2.
+Tactic Notation "especialize" constr(H) "at" int_or_var(i1) "," int_or_var(i2) := proveprem_2 H i1 i2.
 
 Ltac proveprem_as_3 H idnewH i1 i2 i3 :=
   let prefx := fresh_unfail H in
@@ -177,8 +217,7 @@ Ltac proveprem_as_3 H idnewH i1 i2 i3 :=
       [ | assert (idprem3:ev3);
           [ | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) as idnewH ; clear idprem3 idprem2 idprem1 ]]].
 
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at"  integer(i1) "," integer(i2)"," integer(i3) := proveprem_as_3 H idH i1 i2 i3.
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "as" ident(idH) := proveprem_as_3 H idH i1 i2 i3.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "as" ident(idH) := proveprem_as_3 H idH i1 i2 i3.
 
 Ltac proveprem_3 H i1 i2 i3 :=
   let prefx := fresh_unfail H in
@@ -193,7 +232,7 @@ Ltac proveprem_3 H i1 i2 i3 :=
       [ | assert (idprem3:ev3);
           [ | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) ; clear idprem3 idprem2 idprem1 ]]].
 
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) := proveprem_3 H i1 i2 i3.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) := proveprem_3 H i1 i2 i3.
 
 Ltac proveprem_as_4 H idnewH i1 i2 i3 i4 :=
   let prefx := fresh_unfail H in
@@ -212,8 +251,7 @@ Ltac proveprem_as_4 H idnewH i1 i2 i3 i4 :=
         [ | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) as idnewH ;
             clear idprem4 idprem3 idprem2 idprem1 ]]]].
 
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at"  integer(i1) "," integer(i2) "," integer(i3) "," integer(i4) := proveprem_as_4 H idH i1 i2 i3 i4.
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) "as" ident(idH) := proveprem_as_4 H idH i1 i2 i3 i4.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) "as" ident(idH) := proveprem_as_4 H idH i1 i2 i3 i4.
 
 Ltac proveprem_4 H i1 i2 i3 i4 :=
   let prefx := fresh_unfail H in
@@ -232,7 +270,7 @@ Ltac proveprem_4 H i1 i2 i3 i4 :=
         [ | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) ;
             clear idprem4 idprem3 idprem2 idprem1 ]]]].
 
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) := proveprem_4 H i1 i2 i3 i4.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) := proveprem_4 H i1 i2 i3 i4.
 
 
 Ltac proveprem_as_5 H idnewH i1 i2 i3 i4 i5 :=
@@ -255,8 +293,7 @@ Ltac proveprem_as_5 H idnewH i1 i2 i3 i4 i5 :=
           | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) (i5:=idprem5) as idnewH ;
             clear idprem5 idprem4 idprem3 idprem2 idprem1 ]]]]].
 
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at"  integer(i1) "," integer(i2) "," integer(i3) "," integer(i4) "," integer(i5) := proveprem_as_5 H idH i1 i2 i3 i4 i5.
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) "," integer(i5) "as" ident(idH) := proveprem_as_5 H idH i1 i2 i3 i4 i5.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" ident(idH) := proveprem_as_5 H idH i1 i2 i3 i4 i5.
 
 Ltac proveprem_5 H i1 i2 i3 i4 i5 :=
   let prefx := fresh_unfail H in
@@ -278,7 +315,7 @@ Ltac proveprem_5 H i1 i2 i3 i4 i5 :=
           | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) (i5:=idprem5);
             clear idprem5 idprem4 idprem3 idprem2 idprem1 ]]]]].
 
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) "," integer(i5) := proveprem_5 H i1 i2 i3 i4 i5.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) := proveprem_5 H i1 i2 i3 i4 i5.
 
 Ltac proveprem_as_6 H idnewH i1 i2 i3 i4 i5 i6 :=
   let prefx := fresh_unfail H in
@@ -303,8 +340,7 @@ Ltac proveprem_as_6 H idnewH i1 i2 i3 i4 i5 i6 :=
             | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) (i5:=idprem5) (i6:=idprem6) as idnewH ;
               clear idprem6 idprem5 idprem4 idprem3 idprem2 idprem1 ]]]]]].
 
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at"  integer(i1) "," integer(i2) "," integer(i3) "," integer(i4) "," integer(i5) "," integer(i6) := proveprem_as_6 H idH i1 i2 i3 i4 i5 i6.
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) "," integer(i5) "," integer(i6) "as" ident(idH) := proveprem_as_6 H idH i1 i2 i3 i4 i5 i6.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" ident(idH) := proveprem_as_6 H idH i1 i2 i3 i4 i5 i6.
 
 Ltac proveprem_6 H i1 i2 i3 i4 i5 i6 :=
   let prefx := fresh_unfail H in
@@ -329,7 +365,7 @@ Ltac proveprem_6 H i1 i2 i3 i4 i5 i6 :=
           | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) (i5:=idprem5) (i6:=idprem6);
             clear idprem6 idprem5 idprem4 idprem3 idprem2 idprem1 ]]]]]].
 
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) "," integer(i5) "," integer(i6) := proveprem_6 H i1 i2 i3 i4 i5 i6.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) := proveprem_6 H i1 i2 i3 i4 i5 i6.
 
 Ltac proveprem_as_7 H idnewH i1 i2 i3 i4 i5 i6 i7 :=
   let prefx := fresh_unfail H in
@@ -357,8 +393,7 @@ Ltac proveprem_as_7 H idnewH i1 i2 i3 i4 i5 i6 i7 :=
               | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) (i5:=idprem5) (i6:=idprem6) (i7:=idprem7) as idnewH ;
                 clear idprem7 idprem6 idprem5 idprem4 idprem3 idprem2 idprem1 ]]]]]]].
 
-Tactic Notation "especialize" constr(H) "as" ident(idH) "at"  integer(i1) "," integer(i2) "," integer(i3) "," integer(i4) "," integer(i5) "," integer(i6) "," integer(i7) := proveprem_as_7 H idH i1 i2 i3 i4 i5 i6 i7.
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) "," integer(i5) "," integer(i6) "," integer(i7) "as" ident(idH) := proveprem_as_7 H idH i1 i2 i3 i4 i5 i6 i7.
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" ident(idH) := proveprem_as_7 H idH i1 i2 i3 i4 i5 i6 i7.
 
 Ltac proveprem_7 H i1 i2 i3 i4 i5 i6 i7:=
   let prefx := fresh_unfail H in
@@ -386,52 +421,625 @@ Ltac proveprem_7 H i1 i2 i3 i4 i5 i6 i7:=
               | specialize H with (i1:=idprem1) (i2:=idprem2) (i3:=idprem3) (i4:=idprem4) (i5:=idprem5) (i6:=idprem6) (i7:=idprem7);
                 clear idprem7 idprem6 idprem5 idprem4 idprem3 idprem2 idprem1 ]]]]]]].
 
-Tactic Notation "especialize" constr(H) "at"  integer(i1) "," integer(i2)"," integer(i3) "," integer(i4) "," integer(i5) "," integer(i6) "," integer(i7) := proveprem_7 H i1 i2 i3 i4 i5 i6 i7.
-
-
-
-(*
-Definition eq_one (i:nat) := i = 1.
-
-Lemma test_esepec_6_7: (eq_one 2 -> eq_one 3 ->eq_one 4 ->eq_one 5 ->eq_one 6 ->eq_one 7 ->eq_one 8 -> eq_one 9 -> eq_one 1 -> False) -> True.
-Proof.
-  intros H.
-  especialize H at 3,1,4,5,2,7 as h; [ admit | admit | admit  | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac "OK" end].
-  Undo.
-  especialize H as h at 3,1,4,5,2,7; [ admit | admit | admit  | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac "OK" end].
-  Undo.
-  especialize H at 3,1,4,5,2,7; [ admit | admit | admit  | admit | admit | admit | match type of H with eq_one 7 -> eq_one 9 -> eq_one 1 ->False=> idtac "OK" end].
-  Undo.
-  especialize H at 3,1,4,5,2,7,9 as h; [ admit | admit | admit  | admit | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> False => idtac "OK" end].
-  Undo.
-  especialize H as h at 3,1,4,5,2,7,9; [ admit | admit | admit  | admit | admit | admit | admit | match type of h with eq_one 7 -> eq_one 9 -> False => idtac "OK" end].
-  Undo.
-  especialize H at 3,1,4,5,2,7,9; [ admit | admit | admit  | admit | admit | admit | admit | match type of H with eq_one 7 -> eq_one 9 -> False => idtac "OK" end].
-  Undo.
-  exact I.
-Qed.
-
-
-
-
-
-
-(* TEST *)
-
-Lemma foo: (eq_one 2 -> eq_one 1 -> False) -> False.
-Proof.
-  intros H.
-  especialize (le_sind 0) at 1 as hh : h.
-  { admit. }
-  especialize min_l at 1 as ? : ?.
-  { apply (le_n O). }
-  
-  especialize H at 1 as hh : h.
-  { reflexivity. }
-  match type of h with False => idtac "OK" | _ => fail end.
-  assumption.
-Qed.
-*)
-
-
+Tactic Notation "especialize" constr(H) "at"  int_or_var(i1) "," int_or_var(i2)"," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) := proveprem_7 H i1 i2 i3 i4 i5 i6 i7.
+
+
+Tactic Notation "especialize" constr(H) "at" int_or_var(i) "as" "?" :=
+  let nme := fresh in
+  especialize H at i as nme.
+
+Tactic Notation "especialize" constr(H) "at" int_or_var(i1) "," int_or_var(i2) "as" "?" :=
+  let nme := fresh in
+  especialize H at i1,i2 as nme.
+
+Tactic Notation "especialize" constr(H) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "as" "?" :=
+  let nme := fresh in
+  especialize H at i1,i2,i3 as nme.
+
+Tactic Notation "especialize" constr(H) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" "?" :=
+  let nme := fresh in
+  especialize H at i1,i2,i3,i4 as nme.
+
+Tactic Notation "especialize" constr(H) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" "?" :=
+  let nme := fresh in
+  especialize H at i1,i2,i3,i4,i5 as nme.
+
+Tactic Notation "especialize" constr(H) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" "?" :=
+  let nme := fresh in
+  especialize H at i1,i2,i3,i4,i5,i6 as nme.
+
+Tactic Notation "especialize" constr(H) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" "?" :=
+  let nme := fresh in
+  especialize H at i1,i2,i3,i4,i5,i6,i7 as nme.
+
+
+
+
+(* Adding a phase of evar creation for premises that should be solved
+   by side effect of proving others. NOTE that there is no mechanism
+   to ensure that these evar are actually solved when subgoals are
+   proved. You may want to try "unshelve especialize ..." to have a
+   look at created evars.
+
+NOTE: All these tactic notations would be greatly simplified if there
+were a way of iterating on a list_int_sep and/or on list_ident_sep and
+on the list of "with bindindgs". Probablt Ltac2 would be much better
+at this. *)
+
+Ltac spec_evar H id_name :=
+  let idt := fresh id_name "T" in
+  let id := fresh id_name in
+  evar (idt : Type);
+  evar (id : idt);
+  specialize H with (id_name := id); subst id; subst idt.
+
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" "*" :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at * .
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" "*" "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at *.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" "*" "as" "?" :=
+  let nme := fresh in
+  especialize H with id at * as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "until" constr(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H until i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "until" constr(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id until i.
+Tactic Notation "especialize" constr(H) "with" ident(id) "until" constr(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id until i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at i.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id at i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i) ":" ident(hprem) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i : hprem.
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i) "as" ident(H) ":"  ident(hprem) :=
+  specialize oldH as H;
+  especialize H with id at i : hprem.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i) "as" "?" ":"  ident(hprem) :=
+  let nme := fresh in
+  especialize H with id at i as nme : hprem.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i1,i2 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at i1,i2.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "as" "?" :=
+  let nme := fresh in
+  especialize H with id at i1,i2 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i1,i2,i3.
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at i1,i2,i3.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "as" "?" :=
+  let nme := fresh in
+  especialize H with id at i1,i2,i3 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at i1,i2,i3,i4.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" "?" :=
+  let nme := fresh in
+  especialize H with id at i1,i2,i3,i4 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" "?" :=
+  let nme := fresh in
+  especialize H with id at i1,i2,i3,i4,i5 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i1,i2,i3,i4,i5,i6.
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at i1,i2,i3,i4,i5,i6.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" "?" :=
+  let nme := fresh in
+  especialize H with id at i1,i2,i3,i4,i5,i6 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) :=
+  fail_if_not_hyp H;
+  spec_evar H id;
+  especialize H at i1,i2,i3,i4,i5,i6,i7.
+Tactic Notation "especialize" constr(oldH) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id at i1,i2,i3,i4,i5,i6,i7.
+Tactic Notation "especialize" constr(H) "with" ident(id) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" "?" :=
+  let nme := fresh in
+  especialize H with id at i1,i2,i3,i4,i5,i6,i7 as nme.
+
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" "*" :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at *.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" "*" "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at *.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" "*" "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at * as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "until" constr(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 until i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "until" constr(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 until i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "until" constr(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 until i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i) ":" ident(hprem) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i : hprem.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i) "as" ident(H) ":" ident(hprem) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i : hprem.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i) "as" "?" ":" ident(hprem) :=
+  let nme := fresh in
+  especialize H with id1,id2 at i as nme : hprem.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i1,i2 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i1,i2 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at i1,i2 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i1,i2,i3 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i1,i2,i3 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at i1,i2,i3 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at i1,i2,i3,i4 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at i1,i2,i3,i4,i5 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at i1,i2,i3,i4,i5,i6 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2 at i1,i2,i3,i4,i5,i6,i7 as nme.
+
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" "*" :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at *.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" "*" "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at *.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" "*" "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at * as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "until" constr(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 until i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "until" constr(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 until i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "until" constr(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 until i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i) ":" ident(hprem) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i : hprem.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i) "as" ident(H) ":" ident(hprem) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i : hprem.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i) "as" "?" ":" ident(hprem) :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i as nme : hprem.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i1,i2.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i1,i2 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i1,i2 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i1,i2,i3 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i1,i2,i3 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i1,i2,i3 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i1,i2,i3,i4 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i1,i2,i3,i4,i5 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i1,i2,i3,i4,i5,i6 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3 at i1,i2,i3,i4,i5,i6,i7 as nme.
+
+
+
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" "*" :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at *.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" "*" "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at *.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" "*" "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at * as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "until" constr(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 until i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "until" constr(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 until i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "until" constr(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 until i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i) ":" ident(hprem) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i : hprem.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i) "as" ident(H) ":" ident(hprem) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i : hprem.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i) "as" "?" ":" ident(hprem) :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i as nme : hprem.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i1,i2 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i1,i2 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i1,i2 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i1,i2,i3 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i1,i2,i3 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i1,i2,i3 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4,i5 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4,i5,i6 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4 at i1,i2,i3,i4,i5,i6,i7 as nme.
+
+
+
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" "*" :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at *.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" "*" "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at *.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" "*" "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at * as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "until" constr(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 until i.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "until" constr(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 until i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "until" constr(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 until i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i) ":" ident(hprem) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i : hprem.
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i) "as" ident(H) ":" ident(hprem) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i : hprem.
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i) "as" "?" ":" ident(hprem) :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i as nme : hprem.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i1,i2 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i1,i2 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i1,i2 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i1,i2 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i1,i2 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i1,i2 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i1,i2,i3 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2)  "," int_or_var(i3) "," int_or_var(i4) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4,i5 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4,i5 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4,i5,i6 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4,i5,i6 as nme.
+
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) :=
+  fail_if_not_hyp H;
+  spec_evar H id1;
+  especialize H with id2,id3,id4,id5 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(oldH) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" ident(H) :=
+  specialize oldH as H;
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4,i5,i6,i7 .
+Tactic Notation "especialize" constr(H) "with" ident(id1) "," ident(id2) "," ident(id3) "," ident(id4) "," ident(id5) "at" int_or_var(i1) "," int_or_var(i2) "," int_or_var(i3) "," int_or_var(i4) "," int_or_var(i5) "," int_or_var(i6) "," int_or_var(i7) "as" "?" :=
+  let nme := fresh in
+  especialize H with id1,id2,id3,id4,id5 at i1,i2,i3,i4,i5,i6,i7 as nme.
 
diff --git a/_CoqProject b/_CoqProject
index f385406..142c6d3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,6 +2,7 @@
 
 LibHyps/LibHypsNaming.v
 LibHyps/LibHypsTactics.v
+LibHyps/LibSpecialize.v
 LibHyps/LibDecomp.v
 LibHyps/TacNewHyps.v
 LibHyps/LibHyps.v
diff --git a/configure.sh b/configure.sh
index e29b32f..a3691c9 100755
--- a/configure.sh
+++ b/configure.sh
@@ -3,7 +3,7 @@
 FILES=`find . -name "*.v" -exec echo {} \;`
 echo "-R LibHyps LibHyps" > _CoqProject
 echo "" >> _CoqProject
-for i in `find LibHyps -name "*.v"| grep -v LibHypsNaming2 | grep -v LibSpecialize.v | grep -v LibHypsExamples | grep -v LibHypsDemo | grep -v LibHypsTest | grep -v LibHypsRegression`; do
+for i in `find LibHyps -name "*.v"| grep -v LibHypsNaming2 | grep -v LibEspecialize. | grep -v LibHypsExamples | grep -v LibHypsDemo | grep -v LibHypsTest | grep -v LibHypsRegression`; do
   echo $i >> _CoqProject
 done
 coq_makefile -f _CoqProject -o Makefile