diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 99e54cad0af764e053ee1dafc7e361387e30b2e1..0c05374f3a184680de0625a57c77d8cbced021aa 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -1950,10 +1950,11 @@ struct
   let rec lc_open m k v e =
     if not (Bvars.contains k e.bind) then e else
       match e.repr with
-      | Bvar _ -> v
+      | Bvar _ -> v (* e.bind is a singleton that can only contains k *)
       | _ ->
-          try cache_find m e
-          with Not_found -> cache_bind m e (rebuild (lc_open m k v) e)
+          if is_simple e then e else
+            try cache_find m e
+            with Not_found -> cache_bind m e (rebuild (lc_open m k v) e)
 
   let lc_open_term t e =
     let k = Bvars.order e.bind in