diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 935f3729c9ff646c6f0db50a934cc630d81cf53a..a903d576c77d8433ef71f16fae66f649658aea17 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2306,7 +2306,7 @@ struct
         | Lambda, _ -> true
         | Forall, x | Exists, x -> Vars.mem x e.vars
       ) qxs in
-    let xs = List.map (fun (_q, x) -> x) qxs in
+    let xs = List.rev_map (fun (_q, x) -> x) qxs in
     let e = lc_close_xs xs e in
     List.fold_right (fun (q, x) e -> c_bind q (tau_of_var x) e) qxs e