diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml
index 18a75360..38470073 100644
--- a/src/base/Proof_quip.ml
+++ b/src/base/Proof_quip.ml
@@ -237,7 +237,7 @@ end = struct
           Array.iter add_needed_step exprs;
           let p = lazy (
             let exprs = Util.array_to_list_map L_terms.find exprs in
-            P.bool_c rule exprs
+            P.nn @@ P.bool_c rule exprs
           ) in
           L_proofs.add lid p;