[qed] possible extensions of e-subst with let-intro

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