diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index fda9a5b9687999af4deca80a15f9cf01acbfe98e..a451922eb1f2411ea7fb1f72e7a2e906f9f8a4c0 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -306,6 +306,9 @@ sig
   (** Bind the given variable if it appears free in the term,
       or return the term unchanged. *)
 
+  val lc_open : var -> lc_term -> term
+  [@@deprecated "Use e_unbind instead"]
+
   val e_unbind : var -> lc_term -> term
   (** Opens the top-most bound variable with a (fresh) variable.
       Can be only applied on top-most lc-term from `Bind(_,_,_)`,
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index e6311444b090280f27eabfff85f9cd1e6fa30f45..1c3ca9819c35e78e420af817cd891e54c527bb2c 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2004,7 +2004,7 @@ struct
     | Bind(q,t,e) -> c_bind q t (f e)
 
   (* Alpha-convert free-variable x with the top-most bound variable *)
-  let lc_bind x (lc : lc_term) : lc_term =
+  let lc_close x (lc : lc_term) : lc_term =
     let rec walk mu x lc =
       if Vars.mem x lc.vars then
         get mu (lc_alpha (walk mu x)) lc
@@ -2170,7 +2170,7 @@ struct
                   possible to insert a recursive call to let-intro
                   it will use a new instance of e_subst_var that
                   will work on a different sigma *)
-               c_bind q t (lc_bind x e)
+               c_bind q t (lc_close x e)
              else e
           ) (subst sigma alpha e) qs
 
@@ -2302,7 +2302,7 @@ struct
       match q with Forall | Exists -> Vars.mem x e.vars | Lambda -> true in
     if do_bind then
       match let_intro_case q x e with
-      | None -> c_bind q (tau_of_var x) (lc_bind x e)
+      | None -> c_bind q (tau_of_var x) (lc_close x e)
       | Some v -> e_subst_var x v e (* case [let x = v ; e] *)
     else e