diff --git a/src/plugins/qed/logic.mli b/src/plugins/qed/logic.mli
index a59161af28f80b0b0239375df045a90820d706bb..fbbff0fa8f56f3878135fd986d86aba077cf19a2 100644
--- a/src/plugins/qed/logic.mli
+++ b/src/plugins/qed/logic.mli
@@ -330,6 +330,9 @@ sig
   val e_forall : var list -> term -> term
   val e_exists : var list -> term -> term
   val e_lambda : var list -> term -> term
+  val e_close_forall : term -> term
+  val e_close_exists : term -> term
+  val e_close_lambda : term -> term
   val e_apply : term -> term list -> term
 
   val e_bind : binder -> var -> term -> term
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index a903d576c77d8433ef71f16fae66f649658aea17..95654f4b6ec5667a8fbbecd0027c0d1ec1c39970 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2161,19 +2161,28 @@ struct
     walk mu x lc
 
   (* Alpha-convert free-variables in xs with the top-most bound variables *)
-  let lc_close_xs xs (lc : lc_term) : lc_term =
+  (* Only activate flag subset if lc.vars is a subset of xs *)
+  let lc_close_xs ?(subset = false) xs (lc : lc_term) : lc_term =
     let mu = cache () in
     let i = ref (Bvars.order lc.bind) in
     List.rev xs |> List.iter (fun x ->
         set mu (e_var x) (c_bvar !i (tau_of_var x));
         i := !i +1
       );
-    let xs = List.fold_left (fun xs x -> Vars.add x xs) Vars.empty xs in
-    let rec walk mu lc =
-      if Vars.intersect xs lc.vars then
-        get mu (lc_alpha (walk mu)) lc
-      else lc in
-    walk mu lc
+    (* if Vars.subset lc.vars xs then*)
+    if subset then
+      let rec walk mu lc =
+        if not (Vars.is_empty lc.vars) then
+          get mu (lc_alpha (walk mu)) lc
+        else lc in
+      walk mu lc
+    else
+      let xs = List.fold_left (fun xs x -> Vars.add x xs) Vars.empty xs in
+      let rec walk mu lc =
+        if Vars.intersect xs lc.vars then
+          get mu (lc_alpha (walk mu)) lc
+        else lc in
+      walk mu lc
 
   (* Alpha-convert top-most bound variable with free-variable x *)
   let lc_open x (lc : lc_term) : lc_term =
@@ -2550,6 +2559,20 @@ struct
   let e_exists = bind_xs Exists
   let e_lambda = bind_xs Lambda
 
+  let bind_all q e =
+    let e = Vars.fold (fun x e ->
+        match let_intro_case q x e with
+        | None -> e
+        | Some v -> e_subst_var x v e
+      ) e.vars e in
+    let xs = List.sort POOL.compare (Vars.elements e.vars) in
+    let e = lc_close_xs ~subset:true xs e in
+    List.fold_left (fun e x -> c_bind q (tau_of_var x) e) e (List.rev xs)
+
+  let e_close_forall = bind_all Forall
+  let e_close_exists = bind_all Exists
+  let e_close_lambda = bind_all Lambda
+
   (* -------------------------------------------------------------------------- *)
   (* --- Iterators                                                          --- *)
   (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index eabb6008c81ca45170de446d1244c53128f7e8e7..7869f466d863f94344ca26fb4337f80d7d76551e 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -825,7 +825,7 @@ struct
   let e_vars e = List.sort Var.compare (Vars.elements (vars e))
   let p_vars = e_vars
   let p_call = e_fun ~result:Prop
-  let p_close p = p_forall (p_vars p) p
+  let p_close = e_close_forall
 
   let occurs x t = Vars.mem x (vars t)
   let intersect a b = Vars.intersect (vars a) (vars b)