diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index c7ff0db3acdc207684492fc08455a8111d4fa73c..6d25e58831d4c409588c960b3d9431cb77f3f5d0 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -380,9 +380,11 @@ sig
   (** {3 Recursion Scheme} *)
 
   val e_map  : pool -> (term -> term) -> term -> term
+  (** Open and close binders *)
+
   val e_iter : pool -> (term -> unit) -> term -> unit
+  (** Open binders *)
 
-  val lc_map : (term -> term) -> term -> term
   val lc_iter : (term -> unit) -> term -> unit
 
   (** {3 Partial Typing} *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index be689edb26fdd79ffb821691afa863c633ad2582..75a6867a0a72bf4465650fd31ae582317bddd8fa 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2329,6 +2329,8 @@ struct
     | Rget(r,f) -> e_getfield r f
     | Rdef fvs -> e_record fvs
 
+  let lc_iter f e = repr_iter f e.repr
+
   let e_map pool f e =
     match e.repr with
     | Apply(a,xs) -> e_apply (f a) (List.map f xs)
@@ -2338,13 +2340,6 @@ struct
         e_bind q x (f (lc_open x e))
     | _ -> rebuild f e
 
-  let lc_map f e =
-    match e.repr with
-    | Apply(a,xs) -> e_apply (f a) (List.map f xs)
-    | _ -> rebuild f e
-
-  let lc_iter f e = repr_iter f e.repr
-
   let e_iter pool f e =
     match e.repr with
     | Bind(_,t,e) ->
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 1426136e80caf7ebef1842ec670fa978fdd66d80..a0e859f8d2091fff7a61bd1b98f4e6ea16503c2c 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -985,7 +985,7 @@ struct
     mutable cst : bool Tmap.t ;
     mutable dom : Vars.t ; (* support of defs *)
     mutable def : term Tmap.t ; (* defs *)
-    mutable mem : term Tmap.t ; (* defs+memo *)
+    mutable cache : F.sigma option ; (* memo *)
   }
 
   let rec is_cst s e = match F.repr e with
@@ -1012,6 +1012,7 @@ struct
         s.dom <- Vars.union (F.vars a) s.dom ;
         s.def <- Tmap.add a e s.def ;
         s.def <- Tmap.add p p s.def ;
+        s.cache <- None ;
       end
 
   let rec assume s p = match F.repr p with
@@ -1025,13 +1026,16 @@ struct
     | Have p | When p | Core p | Init p -> assume s (F.e_prop p)
     | Type _ | Branch _ | Either _ | State _ -> ()
 
-  let rec e_apply s e =
-    try Tmap.find e s.mem
-    with Not_found ->
-      let e' = F.QED.lc_map (e_apply s) e in
-      s.mem <- Tmap.add e e' s.mem ; e'
+  let subst s =
+    match s.cache with
+    | Some m -> m
+    | None ->
+        let m = Lang.sigma () in
+        F.Subst.add_map m s.def ;
+        s.cache <- Some m ; m
 
-  let p_apply s p = F.p_bool (e_apply s (F.e_prop p))
+  let e_apply s e = F.e_subst (subst s) e
+  let p_apply s p = F.p_subst (subst s) p
 
   let rec c_apply s = function
     | State m -> State (Mstate.apply (e_apply s) m)
@@ -1052,13 +1056,12 @@ struct
   let simplify (hs,p) =
     let s = {
       cst = Tmap.empty ;
-      mem = Tmap.empty ;
       def = Tmap.empty ;
       dom = Vars.empty ;
+      cache = None ;
     } in
     try
       List.iter (fun h -> collect s h.condition) hs ;
-      s.mem <- s.def ;
       let hs = List.map (s_apply s) hs in
       let p = p_apply s p in
       hs , p
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 7769f37de54a3e829cb3ce2effe381e771632b6b..45ff8a2953c6a2df02afed5fb8ab100230adbded 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -371,7 +371,11 @@ class virtual visitor main =
       if not (Tset.mem t terms) then
         begin
           self#repr ~bool:false (F.repr t) ;
-          F.p_iter self#vpred self#vterm p
+          F.lc_iter
+            (fun e ->
+               if F.is_prop e
+               then self#vpred (F.p_bool e)
+               else self#vterm e) t
         end
 
     method private vdefinition = function
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 21e9a0e9e7177b5478d0caa946f1f8decef8c06e..4996cc10890733f2cf17ff7c8c47057dade44838 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -785,13 +785,6 @@ struct
   let varsp = vars
   let p_expr = repr
   let e_expr = repr
-  let p_iter fp fe p =
-    match QED.repr p with
-    | True | False | Kint _ | Kreal _ | Fvar _ | Bvar _ -> ()
-    | Eq(a,b) | Neq(a,b) when is_prop a && is_prop b -> fp a ; fp b
-    | Eq _ | Neq _ | Leq _ | Lt _ | Times _ | Add _ | Mul _ | Div _ | Mod _
-    | Acst _ | Aget _ | Aset _ | Rget _ | Rdef _ | Fun _ | Apply _ -> lc_iter fe p
-    | And _ | Or _ | Imply _ | If _ | Not _ | Bind _ -> lc_iter fp p
 
   let pp_tau = Pretty.pp_tau
   let context_pp = Context.create "Lang.F.pp"
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 409bbedae1e94713f81b136a0655f6ddc058ec15..537df0b7c7607c05f5fab8075b6a0198b356acf7 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -392,13 +392,13 @@ sig
 
   val p_expr : pred -> pred QED.expression
   val e_expr : pred -> term QED.expression
-  val p_iter : (pred -> unit) -> (term -> unit) -> pred -> unit
+
+  (* val p_iter : (pred -> unit) -> (term -> unit) -> pred -> unit *)
 
   (** {3 Binders} *)
 
   val lc_closed : term -> bool
   val lc_iter : (term -> unit) -> term -> unit
-  val lc_map : (term -> term) -> term -> term
 
   (** {3 Utilities} *)