diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index df4a10e3c34824b0bf43cbe4e7462d94420a8b90..a1798c378127a35ba93c8a3f37ec0cf02a272f47 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2166,10 +2166,17 @@ struct
         let qs = (q,x) :: qs in
         bind sigma alpha qs a
     | _ ->
+        (* HERE:
+           This final binding of variables could be parallelized
+           if Bvars is precise enough *)
         List.fold_left
           (fun e (q,x) ->
              if Vars.mem x e.vars then
                let t = tau_of_var x in
+               (* HERE:
+                  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)
              else e
           ) (subst sigma alpha e) qs