From 3523794498e9ac8b86eeec8e1a2147e9abe997b6 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 30 Jun 2020 13:33:39 +0200
Subject: Remove two axioms

---
 src/cnf/Cnf.v | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'src/cnf/Cnf.v')

diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v
index ec18c15..d6a6640 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.v
@@ -287,14 +287,6 @@ Section CHECKER.
      match goal with |- context [Lit.interp rho ?x] => 
      destruct (Lit.interp rho x);trivial end.
 
-  Axiom afold_left_and : forall a,
-    afold_left bool int true andb (Lit.interp rho) a =
-    List.forallb (Lit.interp rho) (to_list a).
-
-  Axiom afold_left_or : forall a,
-    afold_left bool int false orb (Lit.interp rho) a =
-    C.interp rho (to_list a).
-
   Axiom afold_right_impb : forall a,
     (afold_right bool int true implb (Lit.interp rho) a) =
     C.interp rho (to_list (or_of_imp a)).
-- 
cgit