diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 7f1f0f1a35815877a55c4a4cbc9d9f9a4effebeb..517f9857173e4c91d9fcb76e029d08d280b7ce11 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -223,6 +223,7 @@ sig
 
   val pool : ?copy:pool -> unit -> pool
   val fresh : pool -> ?basename:string -> tau -> var
+  val alpha : pool -> var -> var
   val add_var : pool -> var -> unit
   val add_vars : pool -> Vars.t -> unit
 
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index 1b95285882dde1a81db416d4eb23ac4b1537fa58..2cba2c899f7ba69309810d33649ca10ffa297a04 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -130,8 +130,8 @@ let bind ~side bindings property : Tactical.process =
       let open Conditions in
       instance_have ?title:s.descr ~at:s.id bindings property
 
-let filter x e =
-  try F.Tau.equal (F.tau_of_var x) (F.typeof e)
+let filter tau e =
+  try F.Tau.equal tau (F.typeof e)
   with Not_found -> true (* allowed to not restrict usage *)
 
 let fieldname ~range k x =
@@ -159,7 +159,7 @@ class instance =
           let range = match tau with L.Int -> true | _ -> false in
           let tooltip = fieldname ~range env.index x in
           env.feedback#update_field
-            ~tooltip ~range ~enabled:true ~filter:(filter x) fd ;
+            ~tooltip ~range ~enabled:true ~filter:(filter tau) fd ;
           let lemma = F.QED.e_unbind x phi in
           let bindings,property = self#wrap env lemma fields in
           (x,v) :: bindings , property
diff --git a/src/plugins/wp/TacInstance.mli b/src/plugins/wp/TacInstance.mli
index 46e523c1676e82d938b9e0bea9b1c5ba6871127b..00d5adfe2c1df87a551cd3ed6acfe50d0d0b05b6 100644
--- a/src/plugins/wp/TacInstance.mli
+++ b/src/plugins/wp/TacInstance.mli
@@ -29,7 +29,7 @@ open Strategy
 val tactical : Tactical.t
 val fields : selection field list
 val params : parameter list
-val filter : var -> term -> bool
+val filter : tau -> term -> bool
 
 type bindings = (var * selection) list
 
diff --git a/src/plugins/wp/TacLemma.ml b/src/plugins/wp/TacLemma.ml
index 343dbe4ffb0a2d90ae354604162b821c96e81ba4..3f24df008655edc83a529553a9c985c01f38c55b 100644
--- a/src/plugins/wp/TacLemma.ml
+++ b/src/plugins/wp/TacLemma.ml
@@ -90,6 +90,12 @@ let search,psearch =
   Tactical.search ~id:"lemma" ~title:"Lemma" ~descr:"Lemma to Instantiate"
     ~browse ~find:Definitions.find_name ()
 
+
+let fresh pool { l_forall ; l_lemma } =
+  let vars = List.map (F.alpha pool) l_forall in
+  let sigma = Lang.subst l_forall (List.map F.e_var vars) in
+  vars , F.p_subst sigma l_lemma
+
 class instance =
   object(self)
     inherit Tactical.make ~id:"Wp.lemma"
@@ -111,7 +117,7 @@ class instance =
           env.feedback#update_field ~enabled:true
             ~title ~tooltip:env.descr
             ~range:(match tau with L.Int -> true | _ -> false)
-            ~filter:(TacInstance.filter x) fd ;
+            ~filter:(TacInstance.filter tau) fd ;
           let bindings,lemma = self#wrap env xs fields in
           (x,value)::bindings , lemma
       | _ ->
@@ -125,17 +131,16 @@ class instance =
             | None ->
                 self#hide feedback TacInstance.fields ;
                 Not_configured
-            | Some l ->
-                let descr = l.Tactical.descr in
-                let lemma = l.value.l_lemma in
+            | Some Tactical.{ title ; value = dlem } ->
+                let fields = TacInstance.fields in
+                let vars,lemma = fresh feedback#pool dlem in
+                let descr = Pretty_utils.to_string F.pp_pred lemma in
                 let bindings,lemma =
-                  self#wrap { feedback ; descr ; lemma }
-                    l.value.l_forall TacInstance.fields in
+                  self#wrap { feedback ; descr ; lemma } vars fields in
                 match TacInstance.cardinal 1000 bindings with
                 | Some n ->
                     if n > 1 then
                       feedback#set_descr "Generates %d instances" n ;
-                    let title = l.title in
                     let at = Tactical.at selection in
                     Applicable
                       (TacInstance.instance_have ~title ?at bindings lemma)