diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index ed1d943b2ea982fa1d6d2e4b7ed4ea8c10a93675..3c644728933415a304505636d4c94e62ee1146a0 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -317,13 +317,42 @@ sig
   (** {3 Generalized Substitutions} *)
 
   type sigma
-  val sigma : unit -> sigma
+  val sigma : ?pool:pool -> unit -> sigma
 
-  val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
-  [@@deprecated "Might be unsafe in presence of binders"]
+  module Subst :
+  sig
+    type t = sigma
+    val create : ?pool:pool -> unit -> t
+    val fresh : t -> tau -> var
+    val get : t -> term -> term
+
+    val add : t -> term -> term -> unit
+    (** Must bind lc-closed terms, or raise Invalid_argument *)
+
+    val add_map : t -> term Tmap.t -> unit
+    (** Must bind lc-closed terms, or raise Invalid_argument *)
+
+    val add_fun : t -> (term -> term) -> unit
+    (** Must bind lc-closed terms, or raise Invalid_argument *)
+
+    val add_var : t -> var -> unit
+    (** To the pool *)
+
+    val add_vars : t -> Vars.t -> unit
+    (** To the pool *)
+
+    val add_term : t -> term -> unit
+    (** To the pool *)
+  end
+
+  val e_subst : sigma -> term -> term
+  (**
+     The environment sigma must be prepared with the desired substitution.
+     Its pool of fresh variables must covers the entire domain and co-domain
+     of the substitution, and the transformed values.
+  *)
 
   val e_subst_var : var -> term -> term -> term
-  [@@deprecated "Might be unsafe in presence of binders"]
 
   (** {3 Locally Nameless Representation} *)
 
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 85b8d29ba67df8b372c5b61b8f7bef6b78541c5f..e3100ca96c64460ae07f1f78504e32faa24505f7 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -1989,36 +1989,131 @@ struct
     | Bvar _ | Bind _ | Apply _ -> assert false
 
   (* -------------------------------------------------------------------------- *)
-  (* --- General Substitutions                                              --- *)
+  (* --- General Substitution                                               --- *)
   (* -------------------------------------------------------------------------- *)
 
-  type sigma = term cache
+  type sigma = {
+    pool : pool ;
+    mutable shared : sfun ;
+  } and sfun =
+      | EMPTY
+      | FUN of (term -> term) * sfun
+      | MAP of term Tmap.t * sfun
 
-  let sigma () = cache ()
+  module Subst =
+  struct
+    type t = sigma
+
+    let create ?pool () = {
+      pool = POOL.create ?copy:pool () ;
+      shared = EMPTY ;
+    }
+
+    let fresh sigma t = fresh sigma.pool t
+
+    let check v =
+      if not (lc_closed v) then raise (Invalid_argument "Qed.Sigma")
+
+    let checked v = check v ; v
+
+    let rec compute e = function
+      | EMPTY -> raise Not_found
+      | FUN(f,EMPTY) -> checked (f e)
+      | MAP(m,EMPTY) -> Tmap.find e m
+      | FUN(f,s) -> (try checked (f e) with Not_found -> compute e s)
+      | MAP(m,s) -> (try Tmap.find e m with Not_found -> compute e s)
+
+    let get sigma a = compute a sigma.shared
+
+    let add sigma a b =
+      check a ; check b ;
+      sigma.shared <- match sigma.shared with
+        | MAP(m,s) -> MAP (Tmap.add a b m,s)
+        | (FUN _ | EMPTY) as s -> MAP (Tmap.add a b Tmap.empty,s)
+
+    let add_map sigma m =
+      if not (Tmap.is_empty m) then
+        begin
+          Tmap.iter (fun a b -> check a ; check b) m ;
+          sigma.shared <- MAP(m,sigma.shared)
+        end
+
+    let add_fun sigma f =
+      sigma.shared <- FUN(f,sigma.shared)
+
+    let add_var sigma x = add_var sigma.pool x
+    let add_term sigma e = add_vars sigma.pool e.vars
+    let add_vars sigma xs = add_vars sigma.pool xs
 
-  let rec gsubst mu f e =
+  end
+
+  let sigma = Subst.create
+
+  let rec subst sigma alpha e =
+    let mu = cache () in
+    compute mu sigma alpha e
+
+  and incache mu sigma alpha e =
+    get mu (compute mu sigma alpha) e
+
+  and compute mu sigma alpha e =
+    try Subst.get sigma e with Not_found ->
+    let r =
+      match e.repr with
+      | Bvar(k,_) -> Intmap.find k alpha
+      | Bind _ ->
+          (* Not in cache *)
+          bind sigma alpha [] e
+      | Apply(e,es) ->
+          let phi = incache mu sigma alpha in
+          apply sigma Intmap.empty (phi e) (List.map phi es)
+      | _ -> rebuild (incache mu sigma alpha) e
+    in
+    (if lc_closed e && lc_closed r then Subst.add sigma e r) ; r
+
+  and bind sigma alpha qs e =
     match e.repr with
-    | True | False | Kint _ | Kreal _ | Bvar _ -> e
-    | _ -> get mu (fun e ->
-        let e0 = rebuild (gsubst mu f) e in
-        if lc_closed e0 then
-          try f e0 with Not_found -> e0
-        else e0
-      ) e
-
-  let e_subst ?sigma f e =
-    let cache = match sigma with None -> ref Tmap.empty | Some c -> c in
-    gsubst cache f e
+    | Bind(q,t,a) ->
+        let k = Bvars.order a.bind in
+        let x = Subst.fresh sigma t in
+        let alpha = Intmap.add k (e_var x) alpha in
+        let qs = (q,x) :: qs in
+        bind sigma alpha qs a
+    | _ ->
+        List.fold_left
+          (fun e (q,x) ->
+             if Vars.mem x e.vars then
+               let t = tau_of_var x in
+               c_bind q t (lc_bind x e)
+             else e
+          ) (subst sigma alpha e) qs
+
+  and apply sigma beta f vs =
+    match f.repr, vs with
+    | Bind(_,_,g) , v::vs ->
+        let k = Bvars.order g.bind in
+        apply sigma (Intmap.add k v beta) g vs
+    | _ ->
+        subst sigma beta f
+
+  let e_subst sigma e =
+    subst sigma Intmap.empty e
 
   let e_subst_var x v e =
-    let rec walk mu x e =
-      if Vars.mem x e.vars then
-        get mu (rebuild (walk mu x)) e
-      else e
-    in
-    let cache = cache () in
-    set cache (e_var x) v ;
-    walk cache x e
+    if not (Vars.mem x e.vars) then e else
+    if Bvars.is_empty v.bind && Bvars.is_empty e.bind then
+      let rec walk mu x e =
+        if Vars.mem x e.vars then
+          get mu (rebuild (walk mu x)) e
+        else e
+      in
+      let cache = cache () in
+      set cache (e_var x) v ;
+      walk cache x e
+    else
+      let sigma = Subst.create () in
+      Subst.add sigma (e_var x) v ;
+      subst sigma Intmap.empty e
 
   (* -------------------------------------------------------------------------- *)
   (* --- Binders                                                            --- *)
diff --git a/src/plugins/wp/CfgCompiler.ml b/src/plugins/wp/CfgCompiler.ml
index 6109ac2d892a28f893ed5805e24735bdc900c479..f270951710659edcae6417637815e41af5da9dce 100644
--- a/src/plugins/wp/CfgCompiler.ml
+++ b/src/plugins/wp/CfgCompiler.ml
@@ -168,17 +168,14 @@ struct
 
   let node = Node.create
 
-  let identify subst ~src ~tgt =
+  let identify sigma ~src ~tgt =
     S.iter2
       (fun _chunk u v ->
          match u,v with
-         | Some x , Some y ->
-             subst := F.Tmap.add (F.e_var x) (F.e_var y) !subst
+         | Some x , Some y -> F.Subst.add sigma (F.e_var x) (F.e_var y)
          | _ -> ())
       src tgt
 
-  let assoc m e = F.Tmap.find e m
-
   module E = struct
     type t = S.t sequence * F.pred
     let pretty fmt (_seq,p) = Format.fprintf fmt "effect: @[%a@]" F.pp_pred p
@@ -186,10 +183,10 @@ struct
     let create seq p = seq,p
 
     let relocate tgt (src,p) =
-      let subst = ref F.Tmap.empty in
-      identify subst ~src:src.pre ~tgt:tgt.pre ;
-      identify subst ~src:src.post ~tgt:tgt.post ;
-      tgt , F.p_subst (assoc !subst) p
+      let sigma = Lang.sigma () in
+      identify sigma ~src:src.pre ~tgt:tgt.pre ;
+      identify sigma ~src:src.post ~tgt:tgt.post ;
+      tgt , F.p_subst sigma p
 
     let reads (seq,_) = S.domain seq.pre
     let writes (seq,_) = S.writes seq
@@ -200,14 +197,14 @@ struct
     let get = snd
     let create seq p = seq,p
     let relocate tgt (src,p) =
-      let subst = ref F.Tmap.empty in
-      identify subst ~src ~tgt ;
-      tgt , F.p_subst (assoc !subst) p
+      let sigma = Lang.sigma () in
+      identify sigma ~src ~tgt ;
+      tgt , F.p_subst sigma p
     let reads (src,_) = S.domain src
     let equal (s1,p1) (s2,p2) =
-      let subst = ref F.Tmap.empty in
-      identify subst ~src:s1 ~tgt:s2 ;
-      F.eqp (F.p_subst (assoc !subst) p1) p2
+      let sigma = Lang.sigma () in
+      identify sigma ~src:s1 ~tgt:s2 ;
+      F.eqp (F.p_subst sigma p1) p2
   end
 
   module P = struct
@@ -219,17 +216,17 @@ struct
     let create smap p = smap,p
 
     let relocate tgt (src,p) =
-      let subst = ref F.Tmap.empty in
+      let sigma = Lang.sigma () in
       Node.Map.iter2
         (fun n src tgt ->
            match src,tgt with
-           | Some src , Some tgt -> identify subst ~src ~tgt
+           | Some src , Some tgt -> identify sigma ~src ~tgt
            | Some _, None ->
                invalid_arg (Format.asprintf "P.relocate: tgt is smaller than src at %a" Node.pp n)
            | _ -> ())
         src tgt ;
       let tgt = Node.Map.inter (fun _ _ tgt -> tgt) src tgt in
-      tgt , F.p_subst (assoc !subst) p
+      tgt , F.p_subst sigma p
 
     let reads (smap,_) = Node.Map.map (fun _ s -> S.domain s) smap
     let nodes (smap,_) = Node.Map.fold (fun k _ acc -> Node.Set.add k acc) smap Node.Set.empty
@@ -257,16 +254,16 @@ struct
     let reads (smap,_) = Node.Map.map (fun _ s -> S.domain s) smap
 
     let relocate tgt (src,p) =
-      let subst = ref F.Tmap.empty in
+      let sigma = Lang.sigma () in
       Node.Map.iter2
         (fun _ src tgt ->
            match src,tgt with
-           | Some src , Some tgt -> identify subst ~src ~tgt
+           | Some src , Some tgt -> identify sigma ~src ~tgt
            | Some _, None -> invalid_arg "T.relocate: tgt is smaller than src"
            | _ -> ())
         src tgt ;
       let tgt = Node.Map.inter (fun _ _ tgt -> tgt) src tgt in
-      tgt , F.e_subst (assoc !subst) p
+      tgt , F.e_subst sigma p
 
     let init node_set f =
       let node_map = Node.Set.fold (fun x m ->
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 874efe45760d3ff83e47c462cc606fdae5f2054a..02fb5bd932695b843df0a9557da408896b87f560 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -1023,19 +1023,19 @@ let mask_simplifier =
 
     method simplify_exp e =
       if Tmap.is_empty magnitude then e else
-        F.e_subst self#rewrite e
+        Lang.e_subst self#rewrite e
 
     method simplify_hyp p =
       if Tmap.is_empty magnitude then p else
-        F.p_subst self#rewrite p
+        Lang.p_subst self#rewrite p
 
     method simplify_branch p =
       if Tmap.is_empty magnitude then p else
-        F.p_subst self#rewrite p
+        Lang.p_subst self#rewrite p
 
     method simplify_goal p =
       if Tmap.is_empty magnitude then p else
-        F.p_subst self#rewrite p
+        Lang.p_subst self#rewrite p
 
   end
 
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 3362fc39f4d25f1e4e29eea574d771ba64ce37a0..bb722f0377a051c9b03abb0d6b1d30b9abfc6947 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1706,8 +1706,6 @@ let replace ~at step sequent =
 (* --- Replace                                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
-let subst f s =
-  let sigma = F.sigma () in
-  map_sequent (F.p_subst ~sigma f) s
+let subst f s = map_sequent (Lang.p_subst f) s
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 3051ed18a418894640df2e2d9e1f912d80a38a97..b0a2fcc180178a62dd00c03ec456b22f3552068d 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -909,6 +909,39 @@ let local ?pool ?vars ?gamma f =
   let gamma = match gamma with None -> { hyps=[] ; vars=[] } | Some g -> g in
   Context.bind cpool pool (Context.bind cgamma gamma f)
 
+let sigma () = F.sigma ~pool:(Context.get cpool) ()
+
+let alpha () =
+  let sigma = sigma () in
+  let alpha = ref Tmap.empty in
+  let lookup e x =
+    try Tmap.find e !alpha with Not_found ->
+      let y = F.Subst.fresh sigma (F.tau_of_var x) in
+      let ey = e_var y in alpha := Tmap.add e ey !alpha; ey in
+  let compute e =
+    match F.repr e with
+    | Fvar x -> lookup e x
+    | _ -> raise Not_found in
+  F.Subst.add_fun sigma compute ;
+  sigma
+
+let subst xs vs =
+  let bind w x v = Tmap.add (e_var x) v w in
+  let vmap =
+    try List.fold_left2 bind Tmap.empty xs vs
+    with _ -> raise (Invalid_argument "Wp.Lang.Subst.sigma")
+  in
+  let sigma = sigma () in
+  F.Subst.add_map sigma vmap ; sigma
+
+let e_subst f =
+  let sigma = sigma () in
+  F.Subst.add_fun sigma f ; F.e_subst sigma
+
+let p_subst f =
+  let sigma = sigma () in
+  F.Subst.add_fun sigma f ; F.p_subst sigma
+
 (* -------------------------------------------------------------------------- *)
 (* --- Hypotheses                                                         --- *)
 (* -------------------------------------------------------------------------- *)
@@ -941,64 +974,6 @@ let variables g = List.rev g.vars
 let get_hypotheses () = (Context.get cgamma).hyps
 let get_variables () = (Context.get cgamma).vars
 
-(* -------------------------------------------------------------------------- *)
-(* --- Alpha Conversion                                                   --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Alpha =
-struct
-
-  module Vmap = FCMap.Make(Var)
-
-  type t = var Vmap.t ref
-
-  let create () = ref Vmap.empty
-
-  let get w x =
-    try Vmap.find x !w
-    with Not_found ->
-      let y = freshen x in
-      w := Vmap.add x y !w ; y
-
-  let iter f w = Vmap.iter f !w
-
-  let convert w = e_subst
-      (fun e -> match QED.repr e with
-         | Logic.Fvar x -> e_var (get w x)
-         | _ -> raise Not_found)
-
-  let convertp = convert
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Substitution                                                       --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Subst =
-struct
-  type sigma = {
-    e_apply : F.term -> F.term ;
-    p_apply : F.pred -> F.pred ;
-  }
-
-  let sigma xs vs =
-    let bind w x v = Tmap.add (e_var x) v w in
-    let vmap =
-      try List.fold_left2 bind Tmap.empty xs vs
-      with _ -> raise (Invalid_argument "Wp.Lang.Subst.sigma")
-    in
-    let lookup e = Tmap.find e vmap in
-    let sigma = F.sigma () in
-    let e_apply = F.e_subst ~sigma lookup in
-    let p_apply = F.p_subst ~sigma lookup in
-    { e_apply ; p_apply }
-
-  let e_apply s e = s.e_apply e
-  let p_apply s p = s.p_apply p
-
-end
-
 (* -------------------------------------------------------------------------- *)
 (* --- Simplifier                                                         --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index e594b3720e9bce4b72f90903addb6f8e64f71e80..4053e2e390833cd0c422266090946e3c6d300f0e 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -343,10 +343,18 @@ sig
   val p_exists : var list -> pred -> pred
   val p_bind : binder -> var -> pred -> pred
 
-  type sigma = QED.sigma
-  val sigma : unit -> sigma
-  val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
-  val p_subst : ?sigma:sigma -> (term -> term) -> pred -> pred
+  type sigma
+
+  module Subst :
+  sig
+    val get : sigma -> term -> term
+    val add : sigma -> term -> term -> unit
+    val add_map : sigma -> term Tmap.t -> unit
+    val add_fun : sigma -> (term -> term) -> unit
+  end
+
+  val e_subst : sigma -> term -> term
+  val p_subst : sigma -> pred -> pred
   val p_apply : var -> term -> pred -> pred
 
   val e_vars : term -> var list (** Sorted *)
@@ -524,33 +532,14 @@ val has_gamma : unit -> bool
 val get_hypotheses : unit -> pred list
 val get_variables : unit -> var list
 
-(** {2 Alpha Conversion} *)
+(** {2 Substitutions} *)
 
-module Alpha :
-sig
-
-  type t
-  val create : unit -> t
-  val get : t -> var -> var
-  val iter : (var -> var -> unit) -> t -> unit
+val sigma : unit -> F.sigma (** uses current pool *)
+val alpha : unit -> F.sigma (** freshen all variables *)
+val subst : F.var list -> F.term list -> F.sigma (** replace variables *)
 
-  val convert : t -> term -> term
-  val convertp : t -> pred -> pred
-
-end
-
-(** {2 Substitution} *)
-
-module Subst :
-sig
-
-  type sigma
-
-  val sigma : F.var list -> F.term list -> sigma
-  val e_apply : sigma -> F.term -> F.term
-  val p_apply : sigma -> F.pred -> F.pred
-
-end
+val e_subst : (term -> term) -> term -> term (** uses current pool *)
+val p_subst : (term -> term) -> pred -> pred (** uses current pool *)
 
 (** {2 Simplifiers} *)
 
diff --git a/src/plugins/wp/Letify.ml b/src/plugins/wp/Letify.ml
index 5425a3318f23b3f8ffcd14df933ddc7794e0f3ac..66b14fda0524576c744bfb9c1e68eef3f7dd0351 100644
--- a/src/plugins/wp/Letify.ml
+++ b/src/plugins/wp/Letify.ml
@@ -120,18 +120,17 @@ struct
     | _ ->
         clause env h
 
-  let lookup mu e = Tmap.find e mu
   let subst mu =
-    let sigma = F.sigma () in
-    F.p_subst ~sigma (lookup mu)
+    let sigma = Lang.sigma () in
+    F.Subst.add_map sigma mu ; F.p_subst sigma
 
   let e_apply env =
-    let sigma = F.sigma () in
-    F.e_subst ~sigma (lookup env.domain)
+    let sigma = Lang.sigma () in
+    F.Subst.add_map sigma env.domain ; F.e_subst sigma
 
   let p_apply env =
-    let sigma = F.sigma () in
-    F.p_subst ~sigma (lookup env.domain)
+    let sigma = Lang.sigma () in
+    F.Subst.add_map sigma env.domain ; F.p_subst sigma
 
   [@@@ warning "-32"]
   let pp_sigma fmt s =
@@ -147,7 +146,7 @@ struct
   let pretty fmt env = pp_sigma fmt env.domain
 
   let assume env p =
-    let p = F.p_subst (lookup env.domain) p in
+    let p = p_apply env p in
     walk env (F.e_prop p) ; p
 
   let top () = { ground = Tmap.empty ; domain = Tmap.empty }
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index bff1208655630614a4bee6cb0adebf08c1c5f037..449ff8002c848c0ddfc444520482a7cc5fb44799 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -33,9 +33,11 @@ let definition f es =
   let d = find_symbol f in
   match d.d_definition with
   | Function(_,_,u) ->
-      Subst.(e_apply (sigma d.d_params es) u)
+      let sigma = Lang.subst d.d_params es in
+      F.e_subst sigma u
   | Predicate(_,p) ->
-      F.e_prop (Subst.(p_apply (sigma d.d_params es) p))
+      let sigma = Lang.subst d.d_params es in
+      F.e_prop (F.p_subst sigma p)
   | _ ->
       raise Not_found
 
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 7a9212ebaee5782462b178c33633f3b37741d27c..553313a2eca2a823baa289b19ac60295ec659bc4 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1208,9 +1208,9 @@ struct
     let guards = Lang.get_hypotheses () in
     let hyps = Conditions.assume ~descr:"Bisimulation" (p_conj guards) vc.hyps in
     let p = F.p_hyps (Conditions.extract hyps) vc.goal in
-    let alpha = Alpha.create () in
-    let a_hs = List.map (Alpha.convertp alpha) hs in
-    let a_p = Alpha.convertp alpha p in
+    let alpha = Lang.alpha () in
+    let a_hs = List.map (F.p_subst alpha) hs in
+    let a_p = F.p_subst alpha p in
     let p = p_hyps a_hs a_p in
     { vc with
       goal = p ; vars = F.varsp p ;
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 782b9a5425dfb48bfc7d165900d6733b75a2b27b..c0509b33f9f604d7808942b4e4bd0f321a9c0545 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -224,17 +224,22 @@ struct
     g.obligation <- Conditions.close g.sequent
 
   let dkey = Wp_parameters.register_category "prover"
+
+  let safecompute g =
+    begin
+      g.simplified <- true ;
+      let timer = ref 0.0 in
+      Wp_parameters.debug ~dkey "Simplify goal" ;
+      Command.time ~rmax:timer preprocess g ;
+      Wp_parameters.debug ~dkey "Simplification time: %a"
+        Rformat.pp_time !timer ;
+      g.time <- !timer ;
+    end
+
   let compute g =
     if not g.simplified then
-      begin
-        g.simplified <- true ;
-        let timer = ref 0.0 in
-        Wp_parameters.debug ~dkey "Simplify goal" ;
-        Command.time ~rmax:timer preprocess g ;
-        Wp_parameters.debug ~dkey "Simplification time: %a"
-          Rformat.pp_time !timer ;
-        g.time <- !timer ;
-      end
+      Lang.local ~vars:(Conditions.vars_seq g.sequent)
+        safecompute g
 
   let compute_proof g = compute g ; g.obligation
   let compute_descr g = compute g ; g.sequent