From 7d7099475804f06faae03f3031eb6c326ec56b9a Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 14 Nov 2021 22:50:05 -0500
Subject: [PATCH] fix(proof): add neg-normalization

---
 src/base/Proof_quip.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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;