[micromega] native support for boolean operators

The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.

16 files changed, 2833 insertions, 1482 deletions

diff --git a/doc/changelog/04-tactics/11906-micromega-booleans.rst b/doc/changelog/04-tactics/11906-micromega-booleans.rst
new file mode 100644
index 0000000000..39d1525ac3
--- /dev/null
+++ b/doc/changelog/04-tactics/11906-micromega-booleans.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`.
+  (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.)
+  (`#11906 <https://github.com/coq/coq/pull/11906>`_,  by Frédéric Besson).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 77bf58aac6..717b0deb43 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -64,16 +64,23 @@ arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\math
 The syntax of the formulas is the following:
 
  .. productionlist:: F
-   F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F
+   F : A ∣ P | True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F | F = F
    A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p
    p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n
 
-where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
+where :math:`F` is interpreted over either `Prop` or `bool`,
+:math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
 operators :math:`−, +, ×` are respectively subtraction, addition, and product;
 :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition.
 For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of
 rationals ``==``.
 
+When :math:`F` is interpreted over `bool`, the boolean operators are
+`&&`, `||`, `Bool.eqb`, `Bool.implb`, `Bool.negb` and the comparisons
+in :math:`A` are also interpreted over the booleans (e.g., for
+:math:`\mathbb{Z}`, we have `Z.eqb`, `Z.gtb`, `Z.ltb`, `Z.geb`,
+`Z.leb`).
+
 For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational
 constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the
 following expressions:
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 0f8d941b41..44bc20e55f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -86,20 +86,30 @@ type 'cst formula =
 type 'cst clause = ('cst Mc.nFormula, tag * EConstr.constr) Mc.clause
 type 'cst cnf = ('cst Mc.nFormula, tag * EConstr.constr) Mc.cnf
 
+let pp_kind o = function
+  | Mc.IsProp -> output_string o "Prop"
+  | Mc.IsBool -> output_string o "bool"
+
+let kind_is_prop = function Mc.IsProp -> true | Mc.IsBool -> false
+
 let rec pp_formula o (f : 'cst formula) =
   Mc.(
     match f with
-    | TT -> output_string o "tt"
-    | FF -> output_string o "ff"
-    | X c -> output_string o "X "
-    | A (_, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t
-    | Cj (f1, f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2
-    | D (f1, f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2
-    | I (f1, n, f2) ->
-      Printf.fprintf o "I(%a,%s,%a)" pp_formula f1
+    | TT k -> output_string o (if kind_is_prop k then "True" else "true")
+    | FF k -> output_string o (if kind_is_prop k then "False" else "false")
+    | X (k, c) -> Printf.fprintf o "X %a" pp_kind k
+    | A (_, _, (t, _)) -> Printf.fprintf o "A(%a)" Tag.pp t
+    | AND (_, f1, f2) ->
+      Printf.fprintf o "AND(%a,%a)" pp_formula f1 pp_formula f2
+    | OR (_, f1, f2) -> Printf.fprintf o "OR(%a,%a)" pp_formula f1 pp_formula f2
+    | IMPL (_, f1, n, f2) ->
+      Printf.fprintf o "IMPL(%a,%s,%a)" pp_formula f1
         (match n with Some id -> Names.Id.to_string id | None -> "")
         pp_formula f2
-    | N f -> Printf.fprintf o "N(%a)" pp_formula f)
+    | NOT (_, f) -> Printf.fprintf o "NOT(%a)" pp_formula f
+    | IFF (_, f1, f2) ->
+      Printf.fprintf o "IFF(%a,%a)" pp_formula f1 pp_formula f2
+    | EQ (f1, f2) -> Printf.fprintf o "EQ(%a,%a)" pp_formula f1 pp_formula f2)
 
 (**
   * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
@@ -142,6 +152,14 @@ module M = struct
   let coq_iff = lazy (constr_of_ref "core.iff.type")
   let coq_True = lazy (constr_of_ref "core.True.type")
   let coq_False = lazy (constr_of_ref "core.False.type")
+  let coq_bool = lazy (constr_of_ref "core.bool.type")
+  let coq_true = lazy (constr_of_ref "core.bool.true")
+  let coq_false = lazy (constr_of_ref "core.bool.false")
+  let coq_andb = lazy (constr_of_ref "core.bool.andb")
+  let coq_orb = lazy (constr_of_ref "core.bool.orb")
+  let coq_implb = lazy (constr_of_ref "core.bool.implb")
+  let coq_eqb = lazy (constr_of_ref "core.bool.eqb")
+  let coq_negb = lazy (constr_of_ref "core.bool.negb")
   let coq_cons = lazy (constr_of_ref "core.list.cons")
   let coq_nil = lazy (constr_of_ref "core.list.nil")
   let coq_list = lazy (constr_of_ref "core.list.type")
@@ -186,11 +204,18 @@ module M = struct
   let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof")
   let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof")
   let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof")
+  let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp")
+  let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool")
   let coq_Zgt = lazy (constr_of_ref "num.Z.gt")
   let coq_Zge = lazy (constr_of_ref "num.Z.ge")
   let coq_Zle = lazy (constr_of_ref "num.Z.le")
   let coq_Zlt = lazy (constr_of_ref "num.Z.lt")
-  let coq_Eq = lazy (constr_of_ref "core.eq.type")
+  let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb")
+  let coq_Zgeb = lazy (constr_of_ref "num.Z.geb")
+  let coq_Zleb = lazy (constr_of_ref "num.Z.leb")
+  let coq_Zltb = lazy (constr_of_ref "num.Z.ltb")
+  let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb")
+  let coq_eq = lazy (constr_of_ref "core.eq.type")
   let coq_Zplus = lazy (constr_of_ref "num.Z.add")
   let coq_Zminus = lazy (constr_of_ref "num.Z.sub")
   let coq_Zopp = lazy (constr_of_ref "num.Z.opp")
@@ -248,13 +273,16 @@ module M = struct
 
   let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT")
   let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF")
-  let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj")
-  let coq_Or = lazy (constr_of_ref "micromega.GFormula.D")
-  let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N")
+  let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND")
+  let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR")
+  let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT")
   let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A")
   let coq_X = lazy (constr_of_ref "micromega.GFormula.X")
-  let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I")
+  let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL")
+  let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF")
+  let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ")
   let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type")
+  let coq_eKind = lazy (constr_of_ref "micromega.eKind")
 
   (**
     * Initialization : a few Caml symbols are derived from other libraries;
@@ -557,52 +585,56 @@ module M = struct
         (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l)
     with Not_found -> raise ParseError
 
-  let zop_table =
+  let zop_table_prop =
     [ (coq_Zgt, Mc.OpGt)
     ; (coq_Zge, Mc.OpGe)
     ; (coq_Zlt, Mc.OpLt)
     ; (coq_Zle, Mc.OpLe) ]
 
-  let rop_table =
+  let zop_table_bool =
+    [ (coq_Zgtb, Mc.OpGt)
+    ; (coq_Zgeb, Mc.OpGe)
+    ; (coq_Zltb, Mc.OpLt)
+    ; (coq_Zleb, Mc.OpLe)
+    ; (coq_Zeqb, Mc.OpEq) ]
+
+  let rop_table_prop =
     [ (coq_Rgt, Mc.OpGt)
     ; (coq_Rge, Mc.OpGe)
     ; (coq_Rlt, Mc.OpLt)
     ; (coq_Rle, Mc.OpLe) ]
 
-  let qop_table = [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)]
+  let rop_table_bool = []
+
+  let qop_table_prop =
+    [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)]
+
+  let qop_table_bool = []
 
   type gl = {env : Environ.env; sigma : Evd.evar_map}
 
   let is_convertible gl t1 t2 = Reductionops.is_conv gl.env gl.sigma t1 t2
 
-  let parse_zop gl (op, args) =
+  let parse_operator table_prop table_bool has_equality typ gl k (op, args) =
     let sigma = gl.sigma in
     match args with
-    | [|a1; a2|] -> (assoc_const sigma op zop_table, a1, a2)
+    | [|a1; a2|] ->
+      ( assoc_const sigma op
+          (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool)
+      , a1
+      , a2 )
     | [|ty; a1; a2|] ->
       if
-        EConstr.eq_constr sigma op (Lazy.force coq_Eq)
-        && is_convertible gl ty (Lazy.force coq_Z)
+        has_equality
+        && EConstr.eq_constr sigma op (Lazy.force coq_eq)
+        && is_convertible gl ty (Lazy.force typ)
       then (Mc.OpEq, args.(1), args.(2))
       else raise ParseError
     | _ -> raise ParseError
 
-  let parse_rop gl (op, args) =
-    let sigma = gl.sigma in
-    match args with
-    | [|a1; a2|] -> (assoc_const sigma op rop_table, a1, a2)
-    | [|ty; a1; a2|] ->
-      if
-        EConstr.eq_constr sigma op (Lazy.force coq_Eq)
-        && is_convertible gl ty (Lazy.force coq_R)
-      then (Mc.OpEq, a1, a2)
-      else raise ParseError
-    | _ -> raise ParseError
-
-  let parse_qop gl (op, args) =
-    if Array.length args = 2 then
-      (assoc_const gl.sigma op qop_table, args.(0), args.(1))
-    else raise ParseError
+  let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z
+  let parse_rop = parse_operator rop_table_prop [] true coq_R
+  let parse_qop = parse_operator qop_table_prop [] false coq_R
 
   type 'a op =
     | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr)
@@ -622,7 +654,7 @@ module M = struct
 
   module Env = struct
     type t =
-      { vars : EConstr.t list
+      { vars : (EConstr.t * Mc.kind) list
       ; (* The list represents a mapping from EConstr.t to indexes. *)
         gl : gl
             (* The evar_map may be updated due to unification of universes *) }
@@ -642,16 +674,16 @@ module M = struct
         | exception Univ.UniverseInconsistency _ -> None )
       | None -> None
 
-    let compute_rank_add env v =
+    let compute_rank_add env v is_prop =
       let rec _add gl vars n v =
         match vars with
-        | [] -> (gl, [v], n)
-        | e :: l -> (
+        | [] -> (gl, [(v, is_prop)], n)
+        | (e, b) :: l -> (
           match eq_constr gl e v with
           | Some gl' -> (gl', vars, n)
           | None ->
             let gl, l', n = _add gl l (n + 1) v in
-            (gl, e :: l', n) )
+            (gl, (e, b) :: l', n) )
       in
       let gl', vars', n = _add env.gl env.vars 1 v in
       ({vars = vars'; gl = gl'}, CamlToCoq.positive n)
@@ -661,7 +693,7 @@ module M = struct
       let rec _get_rank env n =
         match env with
         | [] -> raise (Invalid_argument "get_rank")
-        | e :: l -> (
+        | (e, _) :: l -> (
           match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1)
           )
       in
@@ -682,7 +714,7 @@ module M = struct
     let pp gl env =
       let ppl =
         List.mapi
-          (fun i e ->
+          (fun i (e, _) ->
             Pp.str "x"
             ++ Pp.int (i + 1)
             ++ Pp.str ":"
@@ -703,7 +735,7 @@ module M = struct
       Feedback.msg_debug
         (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env gl.env gl.sigma term);
     let parse_variable env term =
-      let env, n = Env.compute_rank_add env term in
+      let env, n = Env.compute_rank_add env term Mc.IsBool in
       (Mc.PEX n, env)
     in
     let rec parse_expr env term =
@@ -730,13 +762,13 @@ module M = struct
                 (power, env)
               with ParseError ->
                 (* if the exponent is a variable *)
-                let env, n = Env.compute_rank_add env term in
+                let env, n = Env.compute_rank_add env term Mc.IsBool in
                 (Mc.PEX n, env) )
             | Ukn s ->
               if debug then (
                 Printf.printf "unknown op: %s\n" s;
                 flush stdout );
-              let env, n = Env.compute_rank_add env term in
+              let env, n = Env.compute_rank_add env term Mc.IsBool in
               (Mc.PEX n, env) )
           | _ -> parse_variable env term )
         | _ -> parse_variable env term )
@@ -878,7 +910,7 @@ module M = struct
         Mc.PEpow (expr, exp))
       rop_spec
 
-  let parse_arith parse_op parse_expr env cstr gl =
+  let parse_arith parse_op parse_expr (k : Mc.kind) env cstr gl =
     let sigma = gl.sigma in
     if debug then
       Feedback.msg_debug
@@ -887,7 +919,7 @@ module M = struct
         ++ fnl () );
     match EConstr.kind sigma cstr with
     | App (op, args) ->
-      let op, lhs, rhs = parse_op gl (op, args) in
+      let op, lhs, rhs = parse_op gl k (op, args) in
       let e1, env = parse_expr gl env lhs in
       let e2, env = parse_expr gl env rhs in
       ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env)
@@ -899,13 +931,16 @@ module M = struct
 
   (* generic parsing of arithmetic expressions *)
 
-  let mkC f1 f2 = Mc.Cj (f1, f2)
-  let mkD f1 f2 = Mc.D (f1, f2)
-  let mkIff f1 f2 = Mc.Cj (Mc.I (f1, None, f2), Mc.I (f2, None, f1))
-  let mkI f1 f2 = Mc.I (f1, None, f2)
+  let mkAND b f1 f2 = Mc.AND (b, f1, f2)
+  let mkOR b f1 f2 = Mc.OR (b, f1, f2)
+  let mkIff b f1 f2 = Mc.IFF (b, f1, f2)
+  let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2)
+  let mkEQ f1 f2 = Mc.EQ (f1, f2)
 
-  let mkformula_binary g term f1 f2 =
-    match (f1, f2) with Mc.X _, Mc.X _ -> Mc.X term | _ -> g f1 f2
+  let mkformula_binary b g term f1 f2 =
+    match (f1, f2) with
+    | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term)
+    | _ -> g f1 f2
 
   (**
     * This is the big generic function for formula parsers.
@@ -915,83 +950,129 @@ module M = struct
     let sort = Retyping.get_sort_of env sigma term in
     Sorts.is_prop sort
 
+  type formula_op =
+    { op_and : EConstr.t
+    ; op_or : EConstr.t
+    ; op_iff : EConstr.t
+    ; op_not : EConstr.t
+    ; op_tt : EConstr.t
+    ; op_ff : EConstr.t }
+
+  let prop_op =
+    lazy
+      { op_and = Lazy.force coq_and
+      ; op_or = Lazy.force coq_or
+      ; op_iff = Lazy.force coq_iff
+      ; op_not = Lazy.force coq_not
+      ; op_tt = Lazy.force coq_True
+      ; op_ff = Lazy.force coq_False }
+
+  let bool_op =
+    lazy
+      { op_and = Lazy.force coq_andb
+      ; op_or = Lazy.force coq_orb
+      ; op_iff = Lazy.force coq_eqb
+      ; op_not = Lazy.force coq_negb
+      ; op_tt = Lazy.force coq_true
+      ; op_ff = Lazy.force coq_false }
+
   let parse_formula gl parse_atom env tg term =
     let sigma = gl.sigma in
-    let is_prop term = is_prop gl.env gl.sigma term in
-    let parse_atom env tg t =
+    let parse_atom b env tg t =
       try
-        let at, env = parse_atom env t gl in
-        (Mc.A (at, (tg, t)), env, Tag.next tg)
-      with ParseError ->
-        if is_prop t then (Mc.X t, env, tg) else raise ParseError
+        let at, env = parse_atom b env t gl in
+        (Mc.A (b, at, (tg, t)), env, Tag.next tg)
+      with ParseError -> (Mc.X (b, t), env, tg)
     in
-    let rec xparse_formula env tg term =
+    let prop_op = Lazy.force prop_op in
+    let bool_op = Lazy.force bool_op in
+    let eq = Lazy.force coq_eq in
+    let bool = Lazy.force coq_bool in
+    let rec xparse_formula op k env tg term =
       match EConstr.kind sigma term with
       | App (l, rst) -> (
         match rst with
-        | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) ->
-          let f, env, tg = xparse_formula env tg a in
-          let g, env, tg = xparse_formula env tg b in
-          (mkformula_binary mkC term f g, env, tg)
-        | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_or) ->
-          let f, env, tg = xparse_formula env tg a in
-          let g, env, tg = xparse_formula env tg b in
-          (mkformula_binary mkD term f g, env, tg)
-        | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) ->
-          let f, env, tg = xparse_formula env tg a in
-          (Mc.N f, env, tg)
-        | [|a; b|] when EConstr.eq_constr sigma l (Lazy.force coq_iff) ->
-          let f, env, tg = xparse_formula env tg a in
-          let g, env, tg = xparse_formula env tg b in
-          (mkformula_binary mkIff term f g, env, tg)
-        | _ -> parse_atom env tg term )
+        | [|a; b|] when EConstr.eq_constr sigma l op.op_and ->
+          let f, env, tg = xparse_formula op k env tg a in
+          let g, env, tg = xparse_formula op k env tg b in
+          (mkformula_binary k (mkAND k) term f g, env, tg)
+        | [|a; b|] when EConstr.eq_constr sigma l op.op_or ->
+          let f, env, tg = xparse_formula op k env tg a in
+          let g, env, tg = xparse_formula op k env tg b in
+          (mkformula_binary k (mkOR k) term f g, env, tg)
+        | [|a; b|] when EConstr.eq_constr sigma l op.op_iff ->
+          let f, env, tg = xparse_formula op k env tg a in
+          let g, env, tg = xparse_formula op k env tg b in
+          (mkformula_binary k (mkIff k) term f g, env, tg)
+        | [|ty; a; b|]
+          when EConstr.eq_constr sigma l eq && is_convertible gl ty bool ->
+          let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in
+          let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in
+          (mkformula_binary Mc.IsProp mkEQ term f g, env, tg)
+        | [|a|] when EConstr.eq_constr sigma l op.op_not ->
+          let f, env, tg = xparse_formula op k env tg a in
+          (Mc.NOT (k, f), env, tg)
+        | _ -> parse_atom k env tg term )
       | Prod (typ, a, b)
-        when typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b ->
-        let f, env, tg = xparse_formula env tg a in
-        let g, env, tg = xparse_formula env tg b in
-        (mkformula_binary mkI term f g, env, tg)
+        when kind_is_prop k
+             && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b)
+        ->
+        let f, env, tg = xparse_formula op k env tg a in
+        let g, env, tg = xparse_formula op k env tg b in
+        (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg)
       | _ ->
-        if EConstr.eq_constr sigma term (Lazy.force coq_True) then
-          (Mc.TT, env, tg)
-        else if EConstr.eq_constr sigma term (Lazy.force coq_False) then
-          Mc.(FF, env, tg)
-        else if is_prop term then (Mc.X term, env, tg)
-        else raise ParseError
+        if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg)
+        else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg)
+        else (Mc.X (k, term), env, tg)
     in
-    xparse_formula env tg (*Reductionops.whd_zeta*) term
+    xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term
+
+  (*  let dump_bool b = Lazy.force (if b then coq_true else coq_false)*)
+
+  let dump_kind k =
+    Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool)
 
   let dump_formula typ dump_atom f =
     let app_ctor c args =
       EConstr.mkApp
         ( Lazy.force c
         , Array.of_list
-            ( typ :: EConstr.mkProp :: Lazy.force coq_unit
+            ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit
             :: Lazy.force coq_unit :: args ) )
     in
     let rec xdump f =
       match f with
-      | Mc.TT -> app_ctor coq_TT []
-      | Mc.FF -> app_ctor coq_FF []
-      | Mc.Cj (x, y) -> app_ctor coq_And [xdump x; xdump y]
-      | Mc.D (x, y) -> app_ctor coq_Or [xdump x; xdump y]
-      | Mc.I (x, _, y) ->
-        app_ctor coq_Impl
-          [ xdump x
+      | Mc.TT k -> app_ctor coq_TT [dump_kind k]
+      | Mc.FF k -> app_ctor coq_FF [dump_kind k]
+      | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y]
+      | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y]
+      | Mc.IMPL (k, x, _, y) ->
+        app_ctor coq_IMPL
+          [ dump_kind k
+          ; xdump x
           ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|])
           ; xdump y ]
-      | Mc.N x -> app_ctor coq_Neg [xdump x]
-      | Mc.A (x, _) -> app_ctor coq_Atom [dump_atom x; Lazy.force coq_tt]
-      | Mc.X t -> app_ctor coq_X [t]
+      | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x]
+      | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y]
+      | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y]
+      | Mc.A (k, x, _) ->
+        app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt]
+      | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t]
     in
     xdump f
 
   let prop_env_of_formula gl form =
     Mc.(
       let rec doit env = function
-        | TT | FF | A (_, _) -> env
-        | X t -> fst (Env.compute_rank_add env t)
-        | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) -> doit (doit env f1) f2
-        | N f -> doit env f
+        | TT _ | FF _ | A (_, _, _) -> env
+        | X (b, t) -> fst (Env.compute_rank_add env t b)
+        | AND (b, f1, f2)
+         |OR (b, f1, f2)
+         |IMPL (b, f1, _, f2)
+         |IFF (b, f1, f2) ->
+          doit (doit env f1) f2
+        | NOT (b, f) -> doit env f
+        | EQ (f1, f2) -> doit (doit env f1) f2
       in
       doit (Env.empty gl) form)
 
@@ -1008,11 +1089,15 @@ module M = struct
     in
     Mc.(
       let rec doit = function
-        | TT | FF | X _ -> ISet.empty
-        | A (a, (t, c)) -> vars_of_atom a
-        | Cj (f1, f2) | D (f1, f2) | I (f1, _, f2) ->
+        | TT _ | FF _ | X _ -> ISet.empty
+        | A (_, a, (t, c)) -> vars_of_atom a
+        | AND (_, f1, f2)
+         |OR (_, f1, f2)
+         |IMPL (_, f1, _, f2)
+         |IFF (_, f1, f2)
+         |EQ (f1, f2) ->
           ISet.union (doit f1) (doit f2)
-        | N f -> doit f
+        | NOT (_, f) -> doit f
       in
       doit form)
 
@@ -1026,7 +1111,8 @@ module M = struct
     ; dump_mul : EConstr.constr
     ; dump_pow : EConstr.constr
     ; dump_pow_arg : Mc.n -> EConstr.constr
-    ; dump_op : (Mc.op2 * EConstr.constr) list }
+    ; dump_op_prop : (Mc.op2 * EConstr.constr) list
+    ; dump_op_bool : (Mc.op2 * EConstr.constr) list }
 
   let dump_zexpr =
     lazy
@@ -1038,7 +1124,9 @@ module M = struct
       ; dump_mul = Lazy.force coq_Zmult
       ; dump_pow = Lazy.force coq_Zpower
       ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)))
-      ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table }
+      ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop
+      ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool
+      }
 
   let dump_qexpr =
     lazy
@@ -1050,7 +1138,9 @@ module M = struct
       ; dump_mul = Lazy.force coq_Qmult
       ; dump_pow = Lazy.force coq_Qpower
       ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)))
-      ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table }
+      ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop
+      ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool
+      }
 
   let rec dump_Rcst_as_R cst =
     match cst with
@@ -1087,7 +1177,9 @@ module M = struct
       ; dump_mul = Lazy.force coq_Rmult
       ; dump_pow = Lazy.force coq_Rpower
       ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n)))
-      ; dump_op = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table }
+      ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop
+      ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool
+      }
 
   let prodn n env b =
     let rec prodrec = function
@@ -1105,6 +1197,10 @@ module M = struct
 
 *)
 
+  let eKind = function
+    | Mc.IsProp -> EConstr.mkProp
+    | Mc.IsBool -> Lazy.force coq_bool
+
   let make_goal_of_formula gl dexpr form =
     let vars_idx =
       List.mapi
@@ -1120,7 +1216,7 @@ module M = struct
     in
     let props_n =
       List.mapi
-        (fun i _ -> (fresh_prop "__p" (i + 1), EConstr.mkProp))
+        (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k))
         (Env.elements props)
     in
     let var_name_pos =
@@ -1129,8 +1225,7 @@ module M = struct
     let dump_expr i e =
       let rec dump_expr = function
         | Mc.PEX n ->
-          EConstr.mkRel
-            (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx)
+          EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx)
         | Mc.PEc z -> dexpr.dump_cst z
         | Mc.PEadd (e1, e2) ->
           EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|])
@@ -1144,31 +1239,70 @@ module M = struct
       in
       dump_expr e
     in
-    let mkop op e1 e2 =
-      try
-        EConstr.mkApp
-          (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|])
+    let mkop_prop op e1 e2 =
+      try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|])
+      with Not_found ->
+        EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|])
+    in
+    let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} =
+      mkop_prop fop (dump_expr i flhs) (dump_expr i frhs)
+    in
+    let mkop_bool op e1 e2 =
+      try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|])
       with Not_found ->
-        EConstr.mkApp (Lazy.force coq_Eq, [|dexpr.interp_typ; e1; e2|])
+        EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|])
     in
-    let dump_cstr i {Mc.flhs; Mc.fop; Mc.frhs} =
-      mkop fop (dump_expr i flhs) (dump_expr i frhs)
+    let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} =
+      mkop_bool fop (dump_expr i flhs) (dump_expr i frhs)
     in
-    let rec xdump pi xi f =
+    let rec xdump_prop pi xi f =
       match f with
-      | Mc.TT -> Lazy.force coq_True
-      | Mc.FF -> Lazy.force coq_False
-      | Mc.Cj (x, y) ->
-        EConstr.mkApp (Lazy.force coq_and, [|xdump pi xi x; xdump pi xi y|])
-      | Mc.D (x, y) ->
-        EConstr.mkApp (Lazy.force coq_or, [|xdump pi xi x; xdump pi xi y|])
-      | Mc.I (x, _, y) ->
-        EConstr.mkArrow (xdump pi xi x) Sorts.Relevant
-          (xdump (pi + 1) (xi + 1) y)
-      | Mc.N x ->
-        EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False)
-      | Mc.A (x, _) -> dump_cstr xi x
-      | Mc.X t ->
+      | Mc.TT _ -> Lazy.force coq_True
+      | Mc.FF _ -> Lazy.force coq_False
+      | Mc.AND (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|])
+      | Mc.OR (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|])
+      | Mc.IFF (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|])
+      | Mc.IMPL (_, x, _, y) ->
+        EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant
+          (xdump_prop (pi + 1) (xi + 1) y)
+      | Mc.NOT (_, x) ->
+        EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant
+          (Lazy.force coq_False)
+      | Mc.EQ (x, y) ->
+        EConstr.mkApp
+          ( Lazy.force coq_eq
+          , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] )
+      | Mc.A (_, x, _) -> dump_cstr_prop xi x
+      | Mc.X (_, t) ->
+        let idx = Env.get_rank props t in
+        EConstr.mkRel (pi + idx)
+    and xdump_bool pi xi f =
+      match f with
+      | Mc.TT _ -> Lazy.force coq_true
+      | Mc.FF _ -> Lazy.force coq_false
+      | Mc.AND (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.OR (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.IFF (_, x, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.IMPL (_, x, _, y) ->
+        EConstr.mkApp
+          (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|])
+      | Mc.NOT (_, x) ->
+        EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|])
+      | Mc.EQ (x, y) -> assert false
+      | Mc.A (_, x, _) -> dump_cstr_bool xi x
+      | Mc.X (_, t) ->
         let idx = Env.get_rank props t in
         EConstr.mkRel (pi + idx)
     in
@@ -1179,12 +1313,12 @@ module M = struct
       let idx = Env.get_rank props p in
       EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx))
     in
-    let form' = Mc.mapX subst_prop form in
+    let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in
     ( prodn nb_props
         (List.map (fun (x, y) -> (Name.Name x, y)) props_n)
         (prodn nb_vars
            (List.map (fun (x, y) -> (Name.Name x, y)) vars_n)
-           (xdump (List.length vars_n) 0 form))
+           (xdump_prop (List.length vars_n) 0 form))
     , List.rev props_n
     , List.rev var_name_pos
     , form' )
@@ -1339,7 +1473,9 @@ let qq_domain_spec =
     ; coeff_eq = Mc.qeq_bool }
 
 let max_tag f =
-  1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0))
+  1
+  + Tag.to_int
+      (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) Mc.IsProp f (Tag.from 0))
 
 (** Naive topological sort of constr according to the subterm-ordering *)
 
@@ -1364,7 +1500,9 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*)
             (set
                [ ( "__ff"
                  , ff
-                 , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) )
+                 , EConstr.mkApp
+                     ( Lazy.force coq_Formula
+                     , [|formula_typ; Lazy.force coq_IsProp|] ) )
                ; ( "__varmap"
                  , vm
                  , EConstr.mkApp (Lazy.force coq_VarMap, [|spec.typ|]) )
@@ -1527,37 +1665,73 @@ let abstract_formula : TagSet.t -> 'a formula -> 'a formula =
  fun hyps f ->
   let to_constr =
     Mc.
-      { mkTT = Lazy.force coq_True
-      ; mkFF = Lazy.force coq_False
-      ; mkA = (fun a (tg, t) -> t)
-      ; mkCj =
+      { mkTT =
+          (let coq_True = Lazy.force coq_True in
+           let coq_true = Lazy.force coq_true in
+           function Mc.IsProp -> coq_True | Mc.IsBool -> coq_true)
+      ; mkFF =
+          (let coq_False = Lazy.force coq_False in
+           let coq_false = Lazy.force coq_false in
+           function Mc.IsProp -> coq_False | Mc.IsBool -> coq_false)
+      ; mkA = (fun k a (tg, t) -> t)
+      ; mkAND =
           (let coq_and = Lazy.force coq_and in
-           fun x y -> EConstr.mkApp (coq_and, [|x; y|]))
-      ; mkD =
+           let coq_andb = Lazy.force coq_andb in
+           fun k x y ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_and | Mc.IsBool -> coq_andb)
+               , [|x; y|] ))
+      ; mkOR =
           (let coq_or = Lazy.force coq_or in
-           fun x y -> EConstr.mkApp (coq_or, [|x; y|]))
-      ; mkI = (fun x y -> EConstr.mkArrow x Sorts.Relevant y)
-      ; mkN =
+           let coq_orb = Lazy.force coq_orb in
+           fun k x y ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_or | Mc.IsBool -> coq_orb)
+               , [|x; y|] ))
+      ; mkIMPL =
+          (fun k x y ->
+            match k with
+            | Mc.IsProp -> EConstr.mkArrow x Sorts.Relevant y
+            | Mc.IsBool -> EConstr.mkApp (Lazy.force coq_implb, [|x; y|]))
+      ; mkIFF =
+          (let coq_iff = Lazy.force coq_iff in
+           let coq_eqb = Lazy.force coq_eqb in
+           fun k x y ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_iff | Mc.IsBool -> coq_eqb)
+               , [|x; y|] ))
+      ; mkNOT =
           (let coq_not = Lazy.force coq_not in
-           fun x -> EConstr.mkApp (coq_not, [|x|])) }
+           let coq_negb = Lazy.force coq_negb in
+           fun k x ->
+             EConstr.mkApp
+               ( (match k with Mc.IsProp -> coq_not | Mc.IsBool -> coq_negb)
+               , [|x|] ))
+      ; mkEQ =
+          (let coq_eq = Lazy.force coq_eq in
+           fun x y -> EConstr.mkApp (coq_eq, [|Lazy.force coq_bool; x; y|])) }
   in
-  Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true f
+  Mc.abst_form to_constr (fun (t, _) -> TagSet.mem t hyps) true Mc.IsProp f
 
 (* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2   *)
 let rec abstract_wrt_formula f1 f2 =
   Mc.(
     match (f1, f2) with
-    | X c, _ -> X c
+    | X (b, c), _ -> X (b, c)
     | A _, A _ -> f2
-    | Cj (a, b), Cj (a', b') ->
-      Cj (abstract_wrt_formula a a', abstract_wrt_formula b b')
-    | D (a, b), D (a', b') ->
-      D (abstract_wrt_formula a a', abstract_wrt_formula b b')
-    | I (a, _, b), I (a', x, b') ->
-      I (abstract_wrt_formula a a', x, abstract_wrt_formula b b')
-    | FF, FF -> FF
-    | TT, TT -> TT
-    | N x, N y -> N (abstract_wrt_formula x y)
+    | AND (b, f1, f2), AND (_, f1', f2') ->
+      AND (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | OR (b, f1, f2), OR (_, f1', f2') ->
+      OR (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | IMPL (b, f1, _, f2), IMPL (_, f1', x, f2') ->
+      IMPL (b, abstract_wrt_formula f1 f1', x, abstract_wrt_formula f2 f2')
+    | IFF (b, f1, f2), IFF (_, f1', f2') ->
+      IFF (b, abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | EQ (f1, f2), EQ (f1', f2') ->
+      EQ (abstract_wrt_formula f1 f1', abstract_wrt_formula f2 f2')
+    | FF b, FF _ -> FF b
+    | TT b, TT _ -> TT b
+    | NOT (b, x), NOT (_, y) -> NOT (b, abstract_wrt_formula x y)
     | _ -> failwith "abstract_wrt_formula")
 
 (**
@@ -1577,7 +1751,7 @@ let formula_hyps_concl hyps concl =
     (fun (id, f) (cc, ids) ->
       match f with
       | Mc.X _ -> (cc, ids)
-      | _ -> (Mc.I (f, Some id, cc), id :: ids))
+      | _ -> (Mc.IMPL (Mc.IsProp, f, Some id, cc), id :: ids))
     hyps (concl, [])
 
 (* let time str f x =
@@ -1595,7 +1769,7 @@ let micromega_tauto pre_process cnf spec prover env
   let mt = CamlToCoq.positive (max_tag ff) in
   (* Construction of cnf *)
   let pre_ff = pre_process mt (ff : 'a formula) in
-  let cnf_ff, cnf_ff_tags = cnf pre_ff in
+  let cnf_ff, cnf_ff_tags = cnf Mc.IsProp pre_ff in
   match witness_list_tags prover cnf_ff with
   | Model m -> Model m
   | Unknown -> Unknown
@@ -1621,7 +1795,7 @@ let micromega_tauto pre_process cnf spec prover env
     in
     let ff' = abstract_formula deps ff in
     let pre_ff' = pre_process mt ff' in
-    let cnf_ff', _ = cnf pre_ff' in
+    let cnf_ff', _ = cnf Mc.IsProp pre_ff' in
     if debug then begin
       output_string stdout "\n";
       Printf.printf "TForm    : %a\n" pp_formula ff;
@@ -1647,7 +1821,7 @@ let micromega_tauto pre_process cnf spec prover env
            | Some res -> ()
        end ; *)
     let res' = compact_proofs spec.coeff_eq cnf_ff res cnf_ff' in
-    let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in
+    let ff', res', ids = (ff', res', Mc.ids_of_formula Mc.IsProp ff') in
     let res' = dump_list spec.proof_typ spec.dump_proof res' in
     Prf (ids, ff', res')
 
@@ -1719,9 +1893,11 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac =
                   env' ff_arith ]
           in
           let goal_props =
-            List.rev (Env.elements (prop_env_of_formula gl0 ff'))
+            List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff')))
+          in
+          let goal_vars =
+            List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars
           in
-          let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in
           let arith_args = goal_props @ goal_vars in
           let kill_arith = Tacticals.New.tclTHEN tac_arith tac in
           (*
@@ -1773,7 +1949,9 @@ let micromega_order_changer cert env ff =
             (set
                [ ( "__ff"
                  , ff
-                 , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) )
+                 , EConstr.mkApp
+                     ( Lazy.force coq_Formula
+                     , [|formula_typ; Lazy.force coq_IsProp|] ) )
                ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|]))
                ; ("__wit", cert, cert_typ) ]
                (Tacmach.New.pf_concl gl))
@@ -1805,11 +1983,16 @@ let micromega_genr prover tac =
         let hyps' =
           List.map
             (fun (n, f) ->
-              (n, Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) f))
+              ( n
+              , Mc.map_bformula Mc.IsProp
+                  (Micromega.map_Formula Micromega.q_of_Rcst)
+                  f ))
             hyps
         in
         let concl' =
-          Mc.map_bformula (Micromega.map_Formula Micromega.q_of_Rcst) concl
+          Mc.map_bformula Mc.IsProp
+            (Micromega.map_Formula Micromega.q_of_Rcst)
+            concl
         in
         match
           micromega_tauto
@@ -1847,9 +2030,11 @@ let micromega_genr prover tac =
               ; micromega_order_changer res' env' ff_arith ]
           in
           let goal_props =
-            List.rev (Env.elements (prop_env_of_formula gl0 ff'))
+            List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff')))
+          in
+          let goal_vars =
+            List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars
           in
-          let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in
           let arith_args = goal_props @ goal_vars in
           let kill_arith = Tacticals.New.tclTHEN tac_arith tac in
           (* Tacticals.New.tclTHEN
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index d17a0aabb7..b231779c7b 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -967,39 +967,49 @@ let rec norm_aux cO cI cadd cmul csub copp ceqb = function
   ppow_N cO cI cadd cmul ceqb (fun p -> p)
     (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0
 
+type kind =
+| IsProp
+| IsBool
+
 type ('tA, 'tX, 'aA, 'aF) gFormula =
-| TT
-| FF
-| X of 'tX
-| A of 'tA * 'aA
-| Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-| D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-| N of ('tA, 'tX, 'aA, 'aF) gFormula
-| I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option
+| TT of kind
+| FF of kind
+| X of kind * 'tX
+| A of kind * 'tA * 'aA
+| AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula
+| IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option
    * ('tA, 'tX, 'aA, 'aF) gFormula
+| IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+| EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
 
 (** val mapX :
-    ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4)
-    gFormula **)
-
-let rec mapX f = function
-| X x -> X (f x)
-| Cj (f1, f2) -> Cj ((mapX f f1), (mapX f f2))
-| D (f1, f2) -> D ((mapX f f1), (mapX f f2))
-| N f1 -> N (mapX f f1)
-| I (f1, o, f2) -> I ((mapX f f1), o, (mapX f f2))
+    (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1,
+    'a2, 'a3, 'a4) gFormula **)
+
+let rec mapX f _ = function
+| X (k0, x) -> X (k0, (f k0 x))
+| AND (k0, f1, f2) -> AND (k0, (mapX f k0 f1), (mapX f k0 f2))
+| OR (k0, f1, f2) -> OR (k0, (mapX f k0 f1), (mapX f k0 f2))
+| NOT (k0, f1) -> NOT (k0, (mapX f k0 f1))
+| IMPL (k0, f1, o, f2) -> IMPL (k0, (mapX f k0 f1), o, (mapX f k0 f2))
+| IFF (k0, f1, f2) -> IFF (k0, (mapX f k0 f1), (mapX f k0 f2))
+| EQ (f1, f2) -> EQ ((mapX f IsBool f1), (mapX f IsBool f2))
 | x -> x
 
 (** val foldA :
-    ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **)
+    ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **)
 
-let rec foldA f f0 acc =
+let rec foldA f _ f0 acc =
   match f0 with
-  | A (_, an) -> f acc an
-  | Cj (f1, f2) -> foldA f f1 (foldA f f2 acc)
-  | D (f1, f2) -> foldA f f1 (foldA f f2 acc)
-  | N f1 -> foldA f f1 acc
-  | I (f1, _, f2) -> foldA f f1 (foldA f f2 acc)
+  | A (_, _, an) -> f acc an
+  | AND (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | OR (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | NOT (k0, f1) -> foldA f k0 f1 acc
+  | IMPL (k0, f1, _, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | IFF (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc)
+  | EQ (f1, f2) -> foldA f IsBool f1 (foldA f IsBool f2 acc)
   | _ -> acc
 
 (** val cons_id : 'a1 option -> 'a1 list -> 'a1 list **)
@@ -1009,37 +1019,50 @@ let cons_id id l =
   | Some id0 -> id0::l
   | None -> l
 
-(** val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **)
+(** val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **)
 
-let rec ids_of_formula = function
-| I (_, id, f') -> cons_id id (ids_of_formula f')
+let rec ids_of_formula _ = function
+| IMPL (k0, _, id, f') -> cons_id id (ids_of_formula k0 f')
 | _ -> []
 
-(** val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **)
+(** val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **)
 
-let rec collect_annot = function
-| A (_, a) -> a::[]
-| Cj (f1, f2) -> app (collect_annot f1) (collect_annot f2)
-| D (f1, f2) -> app (collect_annot f1) (collect_annot f2)
-| N f0 -> collect_annot f0
-| I (f1, _, f2) -> app (collect_annot f1) (collect_annot f2)
+let rec collect_annot _ = function
+| A (_, _, a) -> a::[]
+| AND (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| OR (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| NOT (k0, f0) -> collect_annot k0 f0
+| IMPL (k0, f1, _, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| IFF (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2)
+| EQ (f1, f2) -> app (collect_annot IsBool f1) (collect_annot IsBool f2)
 | _ -> []
 
-type 'a bFormula = ('a, __, unit0, unit0) gFormula
+type rtyp = __
+
+type eKind = __
+
+type 'a bFormula = ('a, eKind, unit0, unit0) gFormula
 
 (** val map_bformula :
-    ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5)
-    gFormula **)
-
-let rec map_bformula fct = function
-| TT -> TT
-| FF -> FF
-| X p -> X p
-| A (a, t0) -> A ((fct a), t0)
-| Cj (f1, f2) -> Cj ((map_bformula fct f1), (map_bformula fct f2))
-| D (f1, f2) -> D ((map_bformula fct f1), (map_bformula fct f2))
-| N f0 -> N (map_bformula fct f0)
-| I (f1, a, f2) -> I ((map_bformula fct f1), a, (map_bformula fct f2))
+    kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4,
+    'a5) gFormula **)
+
+let rec map_bformula _ fct = function
+| TT k -> TT k
+| FF k -> FF k
+| X (k, p) -> X (k, p)
+| A (k, a, t0) -> A (k, (fct a), t0)
+| AND (k0, f1, f2) ->
+  AND (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2))
+| OR (k0, f1, f2) ->
+  OR (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2))
+| NOT (k0, f0) -> NOT (k0, (map_bformula k0 fct f0))
+| IMPL (k0, f1, a, f2) ->
+  IMPL (k0, (map_bformula k0 fct f1), a, (map_bformula k0 fct f2))
+| IFF (k0, f1, f2) ->
+  IFF (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2))
+| EQ (f1, f2) ->
+  EQ ((map_bformula IsBool fct f1), (map_bformula IsBool fct f2))
 
 type ('x, 'annot) clause = ('x * 'annot) list
 
@@ -1147,7 +1170,7 @@ let is_cnf_ff = function
 let and_cnf_opt f1 f2 =
   if if is_cnf_ff f1 then true else is_cnf_ff f2
   then cnf_ff
-  else and_cnf f1 f2
+  else if is_cnf_tt f2 then f1 else and_cnf f1 f2
 
 (** val or_cnf_opt :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1,
@@ -1158,36 +1181,89 @@ let or_cnf_opt unsat deduce f1 f2 =
   then cnf_tt
   else if is_cnf_ff f2 then f1 else or_cnf unsat deduce f1 f2
 
-(** val xcnf :
-    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
-    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5)
-    tFormula -> ('a2, 'a3) cnf **)
-
-let rec xcnf unsat deduce normalise1 negate0 pol0 = function
-| TT -> if pol0 then cnf_tt else cnf_ff
-| FF -> if pol0 then cnf_ff else cnf_tt
-| X _ -> cnf_ff
-| A (x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0
-| Cj (e1, e2) ->
+(** val mk_and :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_and unsat deduce rEC k pol0 f1 f2 =
   if pol0
-  then and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-  else or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-| D (e1, e2) ->
+  then and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2)
+  else or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2)
+
+(** val mk_or :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_or unsat deduce rEC k pol0 f1 f2 =
   if pol0
-  then or_cnf_opt unsat deduce (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-  else and_cnf_opt (xcnf unsat deduce normalise1 negate0 pol0 e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-| N e -> xcnf unsat deduce normalise1 negate0 (negb pol0) e
-| I (e1, _, e2) ->
+  then or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2)
+  else and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2)
+
+(** val mk_impl :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_impl unsat deduce rEC k pol0 f1 f2 =
   if pol0
-  then or_cnf_opt unsat deduce
-         (xcnf unsat deduce normalise1 negate0 (negb pol0) e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
-  else and_cnf_opt (xcnf unsat deduce normalise1 negate0 (negb pol0) e1)
-         (xcnf unsat deduce normalise1 negate0 pol0 e2)
+  then or_cnf_opt unsat deduce (rEC (negb pol0) k f1) (rEC pol0 k f2)
+  else and_cnf_opt (rEC (negb pol0) k f1) (rEC pol0 k f2)
+
+(** val mk_iff :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3,
+    'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let mk_iff unsat deduce rEC k pol0 f1 f2 =
+  or_cnf_opt unsat deduce
+    (and_cnf_opt (rEC (negb pol0) k f1) (rEC false k f2))
+    (and_cnf_opt (rEC pol0 k f1) (rEC true k f2))
+
+(** val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option **)
+
+let is_bool _ = function
+| TT _ -> Some true
+| FF _ -> Some false
+| _ -> None
+
+(** val xcnf :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
+    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4,
+    'a5) tFormula -> ('a2, 'a3) cnf **)
+
+let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function
+| TT _ -> if pol0 then cnf_tt else cnf_ff
+| FF _ -> if pol0 then cnf_ff else cnf_tt
+| X (_, _) -> cnf_ff
+| A (_, x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0
+| AND (k0, e1, e2) ->
+  mk_and unsat deduce (fun x x0 x1 ->
+    xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2
+| OR (k0, e1, e2) ->
+  mk_or unsat deduce (fun x x0 x1 ->
+    xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2
+| NOT (k0, e) -> xcnf unsat deduce normalise1 negate0 (negb pol0) k0 e
+| IMPL (k0, e1, _, e2) ->
+  mk_impl unsat deduce (fun x x0 x1 ->
+    xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2
+| IFF (k0, e1, e2) ->
+  (match is_bool k0 e2 with
+   | Some isb ->
+     xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0)
+       k0 e1
+   | None ->
+     mk_iff unsat deduce (fun x x0 x1 ->
+       xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2)
+| EQ (e1, e2) ->
+  (match is_bool IsBool e2 with
+   | Some isb ->
+     xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0)
+       IsBool e1
+   | None ->
+     mk_iff unsat deduce (fun x x0 x1 ->
+       xcnf unsat deduce normalise1 negate0 x x0 x1) IsBool pol0 e1 e2)
 
 (** val radd_term :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2)
@@ -1271,141 +1347,311 @@ let ror_cnf_opt unsat deduce f1 f2 =
 let ratom c a =
   if if is_cnf_ff c then true else is_cnf_tt c then c,(a::[]) else c,[]
 
-(** val rxcnf :
-    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
-    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5)
-    tFormula -> ('a2, 'a3) cnf * 'a3 list **)
-
-let rec rxcnf unsat deduce normalise1 negate0 polarity = function
-| TT -> if polarity then cnf_tt,[] else cnf_ff,[]
-| FF -> if polarity then cnf_ff,[] else cnf_tt,[]
-| X _ -> cnf_ff,[]
-| A (x, t0) -> ratom (if polarity then normalise1 x t0 else negate0 x t0) t0
-| Cj (e1, e2) ->
-  let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in
-  let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+(** val rxcnf_and :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_and unsat deduce rXCNF polarity k e1 e2 =
+  let e3,t1 = rXCNF polarity k e1 in
+  let e4,t2 = rXCNF polarity k e2 in
   if polarity
   then (and_cnf_opt e3 e4),(rev_append t1 t2)
   else let f',t' = ror_cnf_opt unsat deduce e3 e4 in
        f',(rev_append t1 (rev_append t2 t'))
-| D (e1, e2) ->
-  let e3,t1 = rxcnf unsat deduce normalise1 negate0 polarity e1 in
-  let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+
+(** val rxcnf_or :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_or unsat deduce rXCNF polarity k e1 e2 =
+  let e3,t1 = rXCNF polarity k e1 in
+  let e4,t2 = rXCNF polarity k e2 in
   if polarity
   then let f',t' = ror_cnf_opt unsat deduce e3 e4 in
        f',(rev_append t1 (rev_append t2 t'))
   else (and_cnf_opt e3 e4),(rev_append t1 t2)
-| N e -> rxcnf unsat deduce normalise1 negate0 (negb polarity) e
-| I (e1, _, e2) ->
-  let e3,t1 = rxcnf unsat deduce normalise1 negate0 (negb polarity) e1 in
+
+(** val rxcnf_impl :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_impl unsat deduce rXCNF polarity k e1 e2 =
+  let e3,t1 = rXCNF (negb polarity) k e1 in
   if polarity
   then if is_cnf_ff e3
-       then rxcnf unsat deduce normalise1 negate0 polarity e2
-       else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+       then rXCNF polarity k e2
+       else let e4,t2 = rXCNF polarity k e2 in
             let f',t' = ror_cnf_opt unsat deduce e3 e4 in
             f',(rev_append t1 (rev_append t2 t'))
-  else let e4,t2 = rxcnf unsat deduce normalise1 negate0 polarity e2 in
+  else let e4,t2 = rXCNF polarity k e2 in
        (and_cnf_opt e3 e4),(rev_append t1 t2)
 
-type ('term, 'annot, 'tX) to_constrT = { mkTT : 'tX; mkFF : 'tX;
-                                         mkA : ('term -> 'annot -> 'tX);
-                                         mkCj : ('tX -> 'tX -> 'tX);
-                                         mkD : ('tX -> 'tX -> 'tX);
-                                         mkI : ('tX -> 'tX -> 'tX);
-                                         mkN : ('tX -> 'tX) }
+(** val rxcnf_iff :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1,
+    'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list) -> bool -> kind ->
+    ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2,
+    'a3) cnf * 'a3 list **)
+
+let rxcnf_iff unsat deduce rXCNF polarity k e1 e2 =
+  let c1,t1 = rXCNF (negb polarity) k e1 in
+  let c2,t2 = rXCNF false k e2 in
+  let c3,t3 = rXCNF polarity k e1 in
+  let c4,t4 = rXCNF true k e2 in
+  let f',t' = ror_cnf_opt unsat deduce (and_cnf_opt c1 c2) (and_cnf_opt c3 c4)
+  in
+  f',(rev_append t1 (rev_append t2 (rev_append t3 (rev_append t4 t'))))
+
+(** val rxcnf :
+    ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
+    cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4,
+    'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list **)
+
+let rec rxcnf unsat deduce normalise1 negate0 polarity _ = function
+| TT _ -> if polarity then cnf_tt,[] else cnf_ff,[]
+| FF _ -> if polarity then cnf_ff,[] else cnf_tt,[]
+| X (_, _) -> cnf_ff,[]
+| A (_, x, t0) ->
+  ratom (if polarity then normalise1 x t0 else negate0 x t0) t0
+| AND (k0, e1, e2) ->
+  rxcnf_and unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| OR (k0, e1, e2) ->
+  rxcnf_or unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| NOT (k0, e) -> rxcnf unsat deduce normalise1 negate0 (negb polarity) k0 e
+| IMPL (k0, e1, _, e2) ->
+  rxcnf_impl unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| IFF (k0, e1, e2) ->
+  rxcnf_iff unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
+| EQ (e1, e2) ->
+  rxcnf_iff unsat deduce (fun x x0 x1 ->
+    rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity IsBool e1 e2
+
+type ('term, 'annot, 'tX) to_constrT = { mkTT : (kind -> 'tX);
+                                         mkFF : (kind -> 'tX);
+                                         mkA : (kind -> 'term -> 'annot ->
+                                               'tX);
+                                         mkAND : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkOR : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkIMPL : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkIFF : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkNOT : (kind -> 'tX -> 'tX);
+                                         mkEQ : ('tX -> 'tX -> 'tX) }
 
 (** val aformula :
-    ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **)
-
-let rec aformula to_constr = function
-| TT -> to_constr.mkTT
-| FF -> to_constr.mkFF
-| X p -> p
-| A (x, t0) -> to_constr.mkA x t0
-| Cj (f1, f2) ->
-  to_constr.mkCj (aformula to_constr f1) (aformula to_constr f2)
-| D (f1, f2) -> to_constr.mkD (aformula to_constr f1) (aformula to_constr f2)
-| N f0 -> to_constr.mkN (aformula to_constr f0)
-| I (f1, _, f2) ->
-  to_constr.mkI (aformula to_constr f1) (aformula to_constr f2)
-
-(** val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **)
-
-let is_X = function
-| X p -> Some p
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 **)
+
+let rec aformula to_constr _ = function
+| TT b -> to_constr.mkTT b
+| FF b -> to_constr.mkFF b
+| X (_, p) -> p
+| A (b, x, t0) -> to_constr.mkA b x t0
+| AND (k0, f1, f2) ->
+  to_constr.mkAND k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| OR (k0, f1, f2) ->
+  to_constr.mkOR k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| NOT (k0, f0) -> to_constr.mkNOT k0 (aformula to_constr k0 f0)
+| IMPL (k0, f1, _, f2) ->
+  to_constr.mkIMPL k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| IFF (k0, f1, f2) ->
+  to_constr.mkIFF k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
+| EQ (f1, f2) ->
+  to_constr.mkEQ (aformula to_constr IsBool f1) (aformula to_constr IsBool f2)
+
+(** val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option **)
+
+let is_X _ = function
+| X (_, p) -> Some p
 | _ -> None
 
 (** val abs_and :
-    ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
-    'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
-    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4)
-    gFormula **)
-
-let abs_and to_constr f1 f2 c =
-  match is_X f1 with
-  | Some _ -> X (aformula to_constr (c f1 f2))
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) ->
+    ('a1, 'a3, 'a2, 'a4) gFormula **)
+
+let abs_and to_constr k f1 f2 c =
+  match is_X k f1 with
+  | Some _ -> X (k, (aformula to_constr k (c k f1 f2)))
   | None ->
-    (match is_X f2 with
-     | Some _ -> X (aformula to_constr (c f1 f2))
-     | None -> c f1 f2)
+    (match is_X k f2 with
+     | Some _ -> X (k, (aformula to_constr k (c k f1 f2)))
+     | None -> c k f1 f2)
 
 (** val abs_or :
-    ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
-    'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
-    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4)
-    gFormula **)
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) ->
+    ('a1, 'a3, 'a2, 'a4) gFormula **)
 
-let abs_or to_constr f1 f2 c =
-  match is_X f1 with
+let abs_or to_constr k f1 f2 c =
+  match is_X k f1 with
   | Some _ ->
-    (match is_X f2 with
-     | Some _ -> X (aformula to_constr (c f1 f2))
-     | None -> c f1 f2)
-  | None -> c f1 f2
+    (match is_X k f2 with
+     | Some _ -> X (k, (aformula to_constr k (c k f1 f2)))
+     | None -> c k f1 f2)
+  | None -> c k f1 f2
+
+(** val abs_not :
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula)
+    -> ('a1, 'a3, 'a2, 'a4) gFormula **)
+
+let abs_not to_constr k f1 c =
+  match is_X k f1 with
+  | Some _ -> X (k, (aformula to_constr k (c k f1)))
+  | None -> c k f1
 
 (** val mk_arrow :
-    'a4 option -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4)
-    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
+    'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
 
-let mk_arrow o f1 f2 =
+let mk_arrow o k f1 f2 =
   match o with
-  | Some _ -> (match is_X f1 with
-               | Some _ -> f2
-               | None -> I (f1, o, f2))
-  | None -> I (f1, None, f2)
+  | Some _ ->
+    (match is_X k f1 with
+     | Some _ -> f2
+     | None -> IMPL (k, f1, o, f2))
+  | None -> IMPL (k, f1, None, f2)
+
+(** val abst_simpl :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3,
+    'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let rec abst_simpl to_constr needA _ = function
+| A (k, x, t0) ->
+  if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0))
+| AND (k0, f1, f2) ->
+  AND (k0, (abst_simpl to_constr needA k0 f1),
+    (abst_simpl to_constr needA k0 f2))
+| OR (k0, f1, f2) ->
+  OR (k0, (abst_simpl to_constr needA k0 f1),
+    (abst_simpl to_constr needA k0 f2))
+| NOT (k0, f0) -> NOT (k0, (abst_simpl to_constr needA k0 f0))
+| IMPL (k0, f1, o, f2) ->
+  IMPL (k0, (abst_simpl to_constr needA k0 f1), o,
+    (abst_simpl to_constr needA k0 f2))
+| IFF (k0, f1, f2) ->
+  IFF (k0, (abst_simpl to_constr needA k0 f1),
+    (abst_simpl to_constr needA k0 f2))
+| EQ (f1, f2) ->
+  EQ ((abst_simpl to_constr needA IsBool f1),
+    (abst_simpl to_constr needA IsBool f2))
+| x -> x
 
-(** val abst_form :
-    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> ('a1, 'a2, 'a3,
-    'a4) tFormula -> ('a1, 'a3, 'a2, 'a4) gFormula **)
-
-let rec abst_form to_constr needA pol0 = function
-| TT -> if pol0 then TT else X to_constr.mkTT
-| FF -> if pol0 then X to_constr.mkFF else FF
-| X p -> X p
-| A (x, t0) -> if needA t0 then A (x, t0) else X (to_constr.mkA x t0)
-| Cj (f1, f2) ->
-  let f3 = abst_form to_constr needA pol0 f1 in
-  let f4 = abst_form to_constr needA pol0 f2 in
+(** val abst_and :
+    ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4)
+    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2,
+    'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+    'a4) tFormula **)
+
+let abst_and to_constr rEC pol0 k f1 f2 =
   if pol0
-  then abs_and to_constr f3 f4 (fun x x0 -> Cj (x, x0))
-  else abs_or to_constr f3 f4 (fun x x0 -> Cj (x, x0))
-| D (f1, f2) ->
-  let f3 = abst_form to_constr needA pol0 f1 in
-  let f4 = abst_form to_constr needA pol0 f2 in
+  then abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 ->
+         AND (x, x0, x1))
+  else abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> AND
+         (x, x0, x1))
+
+(** val abst_or :
+    ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4)
+    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2,
+    'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3,
+    'a4) tFormula **)
+
+let abst_or to_constr rEC pol0 k f1 f2 =
   if pol0
-  then abs_or to_constr f3 f4 (fun x x0 -> D (x, x0))
-  else abs_and to_constr f3 f4 (fun x x0 -> D (x, x0))
-| N f0 ->
-  let f1 = abst_form to_constr needA (negb pol0) f0 in
-  (match is_X f1 with
-   | Some a -> X (to_constr.mkN a)
-   | None -> N f1)
-| I (f1, o, f2) ->
-  let f3 = abst_form to_constr needA (negb pol0) f1 in
-  let f4 = abst_form to_constr needA pol0 f2 in
+  then abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR
+         (x, x0, x1))
+  else abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR
+         (x, x0, x1))
+
+(** val abst_impl :
+    ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4)
+    tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let abst_impl to_constr rEC pol0 o k f1 f2 =
   if pol0
-  then abs_or to_constr f3 f4 (mk_arrow o)
-  else abs_and to_constr f3 f4 (mk_arrow o)
+  then abs_or to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o)
+  else abs_and to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o)
+
+(** val or_is_X :
+    kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    bool **)
+
+let or_is_X k f1 f2 =
+  match is_X k f1 with
+  | Some _ -> true
+  | None -> (match is_X k f2 with
+             | Some _ -> true
+             | None -> false)
+
+(** val abs_iff :
+    ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
+    'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
+    'a2, 'a3, 'a4) tFormula **)
+
+let abs_iff to_constr k nf1 ff2 f1 tf2 r def =
+  if (&&) (or_is_X k nf1 ff2) (or_is_X k f1 tf2)
+  then X (r, (aformula to_constr r def))
+  else def
+
+(** val abst_iff :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1,
+    'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind
+    -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+    ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let abst_iff to_constr needA rEC pol0 k f1 f2 =
+  abs_iff to_constr k (rEC (negb pol0) k f1) (rEC false k f2) (rEC pol0 k f1)
+    (rEC true k f2) k (IFF (k, (abst_simpl to_constr needA k f1),
+    (abst_simpl to_constr needA k f2)))
+
+(** val abst_eq :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1,
+    'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool ->
+    ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
+    'a2, 'a3, 'a4) tFormula **)
+
+let abst_eq to_constr needA rEC pol0 f1 f2 =
+  abs_iff to_constr IsBool (rEC (negb pol0) IsBool f1) (rEC false IsBool f2)
+    (rEC pol0 IsBool f1) (rEC true IsBool f2) IsProp (EQ
+    ((abst_simpl to_constr needA IsBool f1),
+    (abst_simpl to_constr needA IsBool f2)))
+
+(** val abst_form :
+    ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2,
+    'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
+
+let rec abst_form to_constr needA pol0 _ = function
+| TT k -> if pol0 then TT k else X (k, (to_constr.mkTT k))
+| FF k -> if pol0 then X (k, (to_constr.mkFF k)) else FF k
+| X (k, p) -> X (k, p)
+| A (k, x, t0) ->
+  if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0))
+| AND (k0, f1, f2) ->
+  abst_and to_constr (abst_form to_constr needA) pol0 k0 f1 f2
+| OR (k0, f1, f2) ->
+  abst_or to_constr (abst_form to_constr needA) pol0 k0 f1 f2
+| NOT (k0, f0) ->
+  abs_not to_constr k0 (abst_form to_constr needA (negb pol0) k0 f0)
+    (fun x x0 -> NOT (x, x0))
+| IMPL (k0, f1, o, f2) ->
+  abst_impl to_constr (abst_form to_constr needA) pol0 o k0 f1 f2
+| IFF (k0, f1, f2) ->
+  abst_iff to_constr needA (abst_form to_constr needA) pol0 k0 f1 f2
+| EQ (f1, f2) ->
+  abst_eq to_constr needA (abst_form to_constr needA) pol0 f1 f2
 
 (** val cnf_checker :
     (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **)
@@ -1421,10 +1667,10 @@ let rec cnf_checker checker f l =
 (** val tauto_checker :
     ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
     cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 ->
-    bool) -> ('a1, __, 'a3, unit0) gFormula -> 'a4 list -> bool **)
+    bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool **)
 
 let tauto_checker unsat deduce normalise1 negate0 checker f w =
-  cnf_checker checker (xcnf unsat deduce normalise1 negate0 true f) w
+  cnf_checker checker (xcnf unsat deduce normalise1 negate0 true IsProp f) w
 
 (** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **)
 
@@ -1969,10 +2215,11 @@ let negate t0 tg =
   if zunsat f then cnf_tt else cnf_of_list0 tg (xnegate0 f)
 
 (** val cnfZ :
-    (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list **)
+    kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1)
+    cnf * 'a1 list **)
 
-let cnfZ f =
-  rxcnf zunsat zdeduce normalise0 negate true f
+let cnfZ k f =
+  rxcnf zunsat zdeduce normalise0 negate true k f
 
 (** val ceiling : z -> z -> z **)
 
@@ -2178,10 +2425,11 @@ let normQ =
     qminus qopp qeq_bool
 
 (** val cnfQ :
-    (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list **)
+    kind -> (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1)
+    cnf * 'a1 list **)
 
-let cnfQ f =
-  rxcnf qunsat qdeduce qnormalise qnegate true f
+let cnfQ k f =
+  rxcnf qunsat qdeduce qnormalise qnegate true k f
 
 (** val qTautoChecker : q formula bFormula -> qWitness list -> bool **)
 
@@ -2255,4 +2503,5 @@ let rdeduce =
 
 let rTautoChecker f w =
   tauto_checker runsat rdeduce rnormalise rnegate (fun cl ->
-    rWeakChecker (map fst cl)) (map_bformula (map_Formula q_of_Rcst) f) w
+    rWeakChecker (map fst cl))
+    (map_bformula IsProp (map_Formula q_of_Rcst) f) w
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 4200c80574..53f62e0f5b 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -88,6 +88,15 @@ end
 
 val zeq_bool : z -> z -> bool
 
+type 'c pExpr =
+  | PEc of 'c
+  | PEX of positive
+  | PEadd of 'c pExpr * 'c pExpr
+  | PEsub of 'c pExpr * 'c pExpr
+  | PEmul of 'c pExpr * 'c pExpr
+  | PEopp of 'c pExpr
+  | PEpow of 'c pExpr * n
+
 type 'c pol =
   | Pc of 'c
   | Pinj of positive * 'c pol
@@ -209,15 +218,6 @@ val psquare :
   -> 'a1 pol
   -> 'a1 pol
 
-type 'c pExpr =
-  | PEc of 'c
-  | PEX of positive
-  | PEadd of 'c pExpr * 'c pExpr
-  | PEsub of 'c pExpr * 'c pExpr
-  | PEmul of 'c pExpr * 'c pExpr
-  | PEopp of 'c pExpr
-  | PEpow of 'c pExpr * n
-
 val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
 
 val ppow_pos :
@@ -254,29 +254,46 @@ val norm_aux :
   -> 'a1 pExpr
   -> 'a1 pol
 
+type kind = IsProp | IsBool
+
 type ('tA, 'tX, 'aA, 'aF) gFormula =
-  | TT
-  | FF
-  | X of 'tX
-  | A of 'tA * 'aA
-  | Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-  | D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
-  | N of ('tA, 'tX, 'aA, 'aF) gFormula
-  | I of
-      ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula
+  | TT of kind
+  | FF of kind
+  | X of kind * 'tX
+  | A of kind * 'tA * 'aA
+  | AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+  | OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+  | NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula
+  | IMPL of
+      kind
+      * ('tA, 'tX, 'aA, 'aF) gFormula
+      * 'aF option
+      * ('tA, 'tX, 'aA, 'aF) gFormula
+  | IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
+  | EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
 
 val mapX :
-  ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
+     (kind -> 'a2 -> 'a2)
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) gFormula
+  -> ('a1, 'a2, 'a3, 'a4) gFormula
+
+val foldA :
+  ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
 
-val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
 val cons_id : 'a1 option -> 'a1 list -> 'a1 list
-val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
-val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
+val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
+val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
 
-type 'a bFormula = ('a, __, unit0, unit0) gFormula
+type rtyp = __
+type eKind = __
+type 'a bFormula = ('a, eKind, unit0, unit0) gFormula
 
 val map_bformula :
-  ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula
+     kind
+  -> ('a1 -> 'a2)
+  -> ('a1, 'a3, 'a4, 'a5) gFormula
+  -> ('a2, 'a3, 'a4, 'a5) gFormula
 
 type ('x, 'annot) clause = ('x * 'annot) list
 type ('x, 'annot) cnf = ('x, 'annot) clause list
@@ -334,12 +351,55 @@ val or_cnf_opt :
   -> ('a1, 'a2) cnf
   -> ('a1, 'a2) cnf
 
+val mk_and :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val mk_or :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val mk_impl :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val mk_iff :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf)
+  -> kind
+  -> bool
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf
+
+val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option
+
 val xcnf :
      ('a2 -> bool)
   -> ('a2 -> 'a2 -> 'a2 option)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> bool
+  -> kind
   -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf
 
@@ -387,49 +447,199 @@ val ror_cnf_opt :
 
 val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list
 
+val rxcnf_and :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
+val rxcnf_or :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
+val rxcnf_impl :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
+val rxcnf_iff :
+     ('a2 -> bool)
+  -> ('a2 -> 'a2 -> 'a2 option)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a3, 'a4, 'a5) tFormula
+      -> ('a2, 'a3) cnf * 'a3 list)
+  -> bool
+  -> kind
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a1, 'a3, 'a4, 'a5) tFormula
+  -> ('a2, 'a3) cnf * 'a3 list
+
 val rxcnf :
      ('a2 -> bool)
   -> ('a2 -> 'a2 -> 'a2 option)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> bool
+  -> kind
   -> ('a1, 'a3, 'a4, 'a5) tFormula
   -> ('a2, 'a3) cnf * 'a3 list
 
 type ('term, 'annot, 'tX) to_constrT =
-  { mkTT : 'tX
-  ; mkFF : 'tX
-  ; mkA : 'term -> 'annot -> 'tX
-  ; mkCj : 'tX -> 'tX -> 'tX
-  ; mkD : 'tX -> 'tX -> 'tX
-  ; mkI : 'tX -> 'tX -> 'tX
-  ; mkN : 'tX -> 'tX }
+  { mkTT : kind -> 'tX
+  ; mkFF : kind -> 'tX
+  ; mkA : kind -> 'term -> 'annot -> 'tX
+  ; mkAND : kind -> 'tX -> 'tX -> 'tX
+  ; mkOR : kind -> 'tX -> 'tX -> 'tX
+  ; mkIMPL : kind -> 'tX -> 'tX -> 'tX
+  ; mkIFF : kind -> 'tX -> 'tX -> 'tX
+  ; mkNOT : kind -> 'tX -> 'tX
+  ; mkEQ : 'tX -> 'tX -> 'tX }
 
 val aformula :
-  ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
 
-val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
+val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
 
 val abs_and :
      ('a1, 'a2, 'a3) to_constrT
+  -> kind
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> (   ('a1, 'a2, 'a3, 'a4) tFormula
+  -> (   kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula)
   -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val abs_or :
      ('a1, 'a2, 'a3) to_constrT
+  -> kind
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> (   ('a1, 'a2, 'a3, 'a4) tFormula
+  -> (   kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula
       -> ('a1, 'a2, 'a3, 'a4) tFormula)
   -> ('a1, 'a3, 'a2, 'a4) gFormula
 
+val abs_not :
+     ('a1, 'a2, 'a3) to_constrT
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> ('a1, 'a3, 'a2, 'a4) gFormula
+
 val mk_arrow :
      'a4 option
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_simpl :
+     ('a1, 'a2, 'a3) to_constrT
+  -> ('a2 -> bool)
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_and :
+     ('a1, 'a2, 'a3) to_constrT
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_or :
+     ('a1, 'a2, 'a3) to_constrT
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_impl :
+     ('a1, 'a2, 'a3) to_constrT
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> 'a4 option
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val or_is_X :
+  kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool
+
+val abs_iff :
+     ('a1, 'a2, 'a3) to_constrT
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_iff :
+     ('a1, 'a2, 'a3) to_constrT
+  -> ('a2 -> bool)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
+
+val abst_eq :
+     ('a1, 'a2, 'a3) to_constrT
+  -> ('a2 -> bool)
+  -> (   bool
+      -> kind
+      -> ('a1, 'a2, 'a3, 'a4) tFormula
+      -> ('a1, 'a2, 'a3, 'a4) tFormula)
+  -> bool
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
@@ -438,8 +648,9 @@ val abst_form :
      ('a1, 'a2, 'a3) to_constrT
   -> ('a2 -> bool)
   -> bool
+  -> kind
+  -> ('a1, 'a2, 'a3, 'a4) tFormula
   -> ('a1, 'a2, 'a3, 'a4) tFormula
-  -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val cnf_checker :
   (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
@@ -450,7 +661,7 @@ val tauto_checker :
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> ('a1 -> 'a3 -> ('a2, 'a3) cnf)
   -> (('a2 * 'a3) list -> 'a4 -> bool)
-  -> ('a1, __, 'a3, unit0) gFormula
+  -> ('a1, rtyp, 'a3, unit0) gFormula
   -> 'a4 list
   -> bool
 
@@ -661,7 +872,9 @@ val xnegate0 : z nFormula -> z nFormula list
 val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
 
 val cnfZ :
-  (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list
+     kind
+  -> (z formula, 'a1, 'a2, 'a3) tFormula
+  -> (z nFormula, 'a1) cnf * 'a1 list
 
 val ceiling : z -> z -> z
 
@@ -698,7 +911,9 @@ val qdeduce : q nFormula -> q nFormula -> q nFormula option
 val normQ : q pExpr -> q pol
 
 val cnfQ :
-  (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list
+     kind
+  -> (q formula, 'a1, 'a2, 'a3) tFormula
+  -> (q nFormula, 'a1) cnf * 'a1 list
 
 val qTautoChecker : q formula bFormula -> qWitness list -> bool
 
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 41579d5792..fa7b4aa480 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -248,10 +248,12 @@ module EBinOpT = struct
       source1 : EConstr.t
     ; source2 : EConstr.t
     ; source3 : EConstr.t
-    ; target : EConstr.t
-    ; inj1 : EInjT.t (* InjTyp source1 target *)
-    ; inj2 : EInjT.t (* InjTyp source2 target *)
-    ; inj3 : EInjT.t (* InjTyp source3 target *)
+    ; target1 : EConstr.t
+    ; target2 : EConstr.t
+    ; target3 : EConstr.t
+    ; inj1 : EInjT.t (* InjTyp source1 target1 *)
+    ; inj2 : EInjT.t (* InjTyp source2 target2 *)
+    ; inj3 : EInjT.t (* InjTyp source3 target3 *)
     ; bop : EConstr.t (* BOP *)
     ; tbop : EConstr.t (* TBOP *)
     ; tbopinj : EConstr.t (* TBOpInj *)
@@ -272,7 +274,8 @@ module EUnOpT = struct
   type t =
     { source1 : EConstr.t
     ; source2 : EConstr.t
-    ; target : EConstr.t
+    ; target1 : EConstr.t
+    ; target2 : EConstr.t
     ; uop : EConstr.t
     ; inj1_t : EInjT.t
     ; inj2_t : EInjT.t
@@ -392,24 +395,26 @@ module EBinOp = struct
   let table = table
 
   let mk_elt evd i a =
-    let i1 = get_inj evd a.(5) in
-    let i2 = get_inj evd a.(6) in
-    let i3 = get_inj evd a.(7) in
-    let tbop = a.(8) in
+    let i1 = get_inj evd a.(7) in
+    let i2 = get_inj evd a.(8) in
+    let i3 = get_inj evd a.(9) in
+    let tbop = a.(10) in
     { source1 = a.(0)
     ; source2 = a.(1)
     ; source3 = a.(2)
-    ; target = a.(3)
+    ; target1 = a.(3)
+    ; target2 = a.(4)
+    ; target3 = a.(5)
     ; inj1 = i1
     ; inj2 = i2
     ; inj3 = i3
-    ; bop = a.(4)
-    ; tbop = a.(8)
-    ; tbopinj = a.(9)
+    ; bop = a.(6)
+    ; tbop
+    ; tbopinj = a.(11)
     ; classify_binop =
-        classify_op (mkconvert_binop i1 i2 i3) i1.EInjT.inj a.(4) tbop }
+        classify_op (mkconvert_binop i1 i2 i3) i3.EInjT.inj a.(6) tbop }
 
-  let get_key = 4
+  let get_key = 6
   let cast x = BinOp x
   let dest = function BinOp x -> Some x | _ -> None
 end
@@ -452,23 +457,24 @@ module EUnOp = struct
   let dest = function UnOp x -> Some x | _ -> None
 
   let mk_elt evd i a =
-    let i1 = get_inj evd a.(4) in
-    let i2 = get_inj evd a.(5) in
-    let uop = a.(3) in
-    let tuop = a.(6) in
+    let i1 = get_inj evd a.(5) in
+    let i2 = get_inj evd a.(6) in
+    let uop = a.(4) in
+    let tuop = a.(7) in
     { source1 = a.(0)
     ; source2 = a.(1)
-    ; target = a.(2)
+    ; target1 = a.(2)
+    ; target2 = a.(3)
     ; uop
     ; inj1_t = i1
     ; inj2_t = i2
     ; tuop
-    ; tuopinj = a.(7)
+    ; tuopinj = a.(8)
     ; is_construct = EConstr.isConstruct evd uop
-    ; classify_unop = classify_op (mkconvert_unop i1 i2) i1.EInjT.inj uop tuop
+    ; classify_unop = classify_op (mkconvert_unop i1 i2) i2.EInjT.inj uop tuop
     }
 
-  let get_key = 3
+  let get_key = 4
 end
 
 module EBinRel = struct
@@ -788,7 +794,8 @@ let app_unop evd src unop arg prf =
             ( force mkapp
             , [| unop.source1
                ; unop.source2
-               ; unop.target
+               ; unop.target1
+               ; unop.target2
                ; unop.uop
                ; unop.inj1_t.EInjT.inj
                ; unop.inj2_t.EInjT.inj
@@ -859,7 +866,9 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 =
             , [| binop.source1
                ; binop.source2
                ; binop.source3
-               ; binop.target
+               ; binop.target1
+               ; binop.target2
+               ; binop.target3
                ; binop.bop
                ; binop.inj1.EInjT.inj
                ; binop.inj2.EInjT.inj
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index d70978fabe..9e10786fcd 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -130,6 +130,8 @@ Definition eqb (b1 b2:bool) : bool :=
     | false, false => true
   end.
 
+Register eqb as core.bool.eqb.
+
 Lemma eqb_subst :
   forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2.
 Proof.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index cba90043d5..8ab12ae534 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -73,6 +73,7 @@ Infix "&&" := andb : bool_scope.
 
 Register andb as core.bool.andb.
 Register orb as core.bool.orb.
+Register implb as core.bool.implb.
 Register xorb as core.bool.xorb.
 Register negb as core.bool.negb.
 
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 1729b9f85e..a566348dd5 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -47,6 +47,8 @@ Register mul as num.Z.mul.
 Register pow as num.Z.pow.
 Register of_nat as num.Z.of_nat.
 
+
+
 (** When including property functors, only inline t eq zero one two *)
 
 Set Inline Level 30.
@@ -81,6 +83,11 @@ Register le as num.Z.le.
 Register lt as num.Z.lt.
 Register ge as num.Z.ge.
 Register gt as num.Z.gt.
+Register leb as num.Z.leb.
+Register ltb as num.Z.ltb.
+Register geb as num.Z.geb.
+Register gtb as num.Z.gtb.
+Register eqb as num.Z.eqb.
 
 (** * Decidability of equality. *)
 
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v
index 3d955fec4f..b2c5884ed7 100644
--- a/theories/micromega/Lia.v
+++ b/theories/micromega/Lia.v
@@ -19,7 +19,6 @@ Require Import BinNums.
 Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
-
 Ltac zchecker :=
   intros ?__wit ?__varmap ?__ff ;
   exact (ZTautoChecker_sound __ff __wit
@@ -30,7 +29,6 @@ Ltac lia := Zify.zify; xlia zchecker.
                
 Ltac nia := Zify.zify; xnlia zchecker.
 
-
 (* Local Variables: *)
 (* coding: utf-8 *)
 (* End: *)
diff --git a/theories/micromega/QMicromega.v b/theories/micromega/QMicromega.v
index 1fbc5a648a..90ed0ab9d2 100644
--- a/theories/micromega/QMicromega.v
+++ b/theories/micromega/QMicromega.v
@@ -1,7 +1,7 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
 (*         *     GNU Lesser General Public License Version 2.1          *)
@@ -107,7 +107,7 @@ Proof.
   apply QNpower.
 Qed.
 
-Definition Qeval_op2 (o : Op2) : Q -> Q -> Prop :=
+Definition Qeval_pop2 (o : Op2) : Q -> Q -> Prop :=
 match o with
 | OpEq =>  Qeq
 | OpNEq => fun x y  => ~ x == y
@@ -117,13 +117,63 @@ match o with
 | OpGt => fun x y => Qlt y x
 end.
 
-Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) :=
-  let (lhs,o,rhs) := ff in Qeval_op2 o (Qeval_expr e lhs) (Qeval_expr e rhs).
+
+Definition Qlt_bool (x y : Q) :=
+  (Qnum x * QDen y <? Qnum y * QDen x)%Z.
+
+Definition Qeval_bop2 (o : Op2) : Q -> Q -> bool :=
+  match o with
+  | OpEq  => Qeq_bool
+  | OpNEq => fun x y => negb (Qeq_bool x y)
+  | OpLe  => Qle_bool
+  | OpGe  => fun x y => Qle_bool y x
+  | OpLt  => Qlt_bool
+  | OpGt  => fun x y => Qlt_bool y x
+  end.
+
+Lemma Qlt_bool_iff : forall q1 q2,
+    Qlt_bool q1 q2 = true <-> q1 < q2.
+Proof.
+  unfold Qlt_bool.
+  unfold Qlt. intros.
+  apply Z.ltb_lt.
+Qed.
+
+Lemma pop2_bop2 :
+  forall (op : Op2) (q1 q2 : Q), is_true (Qeval_bop2 op q1 q2) <-> Qeval_pop2 op q1 q2.
+Proof.
+  unfold is_true.
+  destruct op ; simpl; intros.
+  - apply Qeq_bool_iff.
+  - rewrite <- Qeq_bool_iff.
+    rewrite negb_true_iff.
+    destruct (Qeq_bool q1 q2) ; intuition congruence.
+  - apply Qle_bool_iff.
+  - apply Qle_bool_iff.
+  - apply Qlt_bool_iff.
+  - apply Qlt_bool_iff.
+Qed.
+
+Definition Qeval_op2 (k:Tauto.kind) :  Op2 ->  Q -> Q -> Tauto.rtyp k:=
+  if k as k0 return (Op2 -> Q -> Q -> Tauto.rtyp k0)
+  then Qeval_pop2 else Qeval_bop2.
+
+
+Lemma Qeval_op2_hold : forall k op q1 q2,
+    Tauto.hold k (Qeval_op2 k op q1 q2) <-> Qeval_pop2 op q1 q2.
+Proof.
+  destruct k.
+  simpl ; tauto.
+  simpl. apply pop2_bop2.
+Qed.
+
+Definition Qeval_formula (e:PolEnv Q) (k: Tauto.kind) (ff : Formula Q) :=
+  let (lhs,o,rhs) := ff in Qeval_op2 k o (Qeval_expr e lhs) (Qeval_expr e rhs).
 
 Definition Qeval_formula' :=
   eval_formula  Qplus Qmult Qminus Qopp Qeq Qle Qlt (fun x => x) (fun x => x) (pow_N 1 Qmult).
 
-Lemma Qeval_formula_compat : forall env f, Qeval_formula env f <-> Qeval_formula' env f.
+ Lemma Qeval_formula_compat : forall env b f, Tauto.hold b (Qeval_formula env b f) <-> Qeval_formula' env f.
 Proof.
   intros.
   unfold Qeval_formula.
@@ -131,6 +181,8 @@ Proof.
   repeat rewrite Qeval_expr_compat.
   unfold Qeval_formula'.
   unfold Qeval_expr'.
+  simpl.
+  rewrite Qeval_op2_hold.
   split ; destruct Fop ; simpl; auto.
 Qed.
 
@@ -186,10 +238,10 @@ Definition qdeduce := nformula_plus_nformula 0 Qplus Qeq_bool.
 Definition normQ  := norm 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
 Declare Equivalent Keys normQ RingMicromega.norm.
 
-Definition cnfQ (Annot TX AF: Type) (f: TFormula (Formula Q) Annot TX AF) :=
+Definition cnfQ (Annot:Type) (TX: Tauto.kind -> Type)  (AF: Type) (k: Tauto.kind) (f: TFormula (Formula Q) Annot TX AF k) :=
   rxcnf qunsat qdeduce (Qnormalise Annot) (Qnegate Annot) true f.
 
-Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness)  : bool :=
+Definition QTautoChecker  (f : BFormula (Formula Q) Tauto.isProp) (w: list QWitness)  : bool :=
   @tauto_checker (Formula Q) (NFormula Q) unit
   qunsat qdeduce
   (Qnormalise unit)
@@ -208,8 +260,11 @@ Proof.
     destruct t.
     apply (check_inconsistent_sound Qsor QSORaddon) ; auto.
   - unfold qdeduce. intros. revert H. apply (nformula_plus_nformula_correct Qsor QSORaddon);auto.
-  - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now  eapply (cnf_normalise_correct Qsor QSORaddon);eauto.
-  - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now eapply (cnf_negate_correct Qsor QSORaddon);eauto.
+  - intros.
+    rewrite Qeval_formula_compat.
+    eapply (cnf_normalise_correct Qsor QSORaddon)  ; eauto.
+  - intros. rewrite Tauto.hold_eNOT. rewrite Qeval_formula_compat.
+    now eapply (cnf_negate_correct Qsor QSORaddon);eauto.
   - intros t w0.
     unfold eval_tt.
     intros.
diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v
index fd8903eac9..09b44f145d 100644
--- a/theories/micromega/RMicromega.v
+++ b/theories/micromega/RMicromega.v
@@ -1,7 +1,7 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
 (*         *     GNU Lesser General Public License Version 2.1          *)
@@ -15,14 +15,13 @@
 (************************************************************************)
 
 Require Import OrderedRing.
-Require Import RingMicromega.
+Require Import QMicromega RingMicromega.
 Require Import Refl.
-Require Import Raxioms Rfunctions RIneq Rpow_def.
+Require Import Sumbool Raxioms Rfunctions RIneq Rpow_def.
 Require Import QArith.
 Require Import Qfield.
 Require Import Qreals.
 Require Import DeclConstant.
-Require Import Ztac.
 
 Require Setoid.
 (*Declare ML Module "micromega_plugin".*)
@@ -344,16 +343,17 @@ Proof.
       apply Qeq_bool_eq in C2.
       rewrite C2.
       simpl.
-      rewrite Qpower0.
+      assert (z <> 0%Z).
+      { intro ; subst. apply Z.lt_irrefl in C1. auto. }
+      rewrite Qpower0 by auto.
       apply Q2R_0.
-      intro ; subst ; slia C1 C1.
     + rewrite Q2RpowerRZ.
       rewrite IHc.
       reflexivity.
       rewrite andb_false_iff in C.
       destruct C.
       simpl. apply Z.ltb_ge in H.
-      right ; normZ. slia H H0.
+      right. Ztac.normZ. Ztac.slia H H0.
       left ; apply Qeq_bool_neq; auto.
     + simpl.
       rewrite <- IHc.
@@ -382,7 +382,7 @@ Definition INZ (n:N) : R :=
 Definition Reval_expr := eval_pexpr  Rplus Rmult Rminus Ropp R_of_Rcst N.to_nat pow.
 
 
-Definition Reval_op2 (o:Op2) : R -> R -> Prop :=
+Definition Reval_pop2 (o:Op2) : R -> R -> Prop :=
     match o with
       | OpEq =>  @eq R
       | OpNEq => fun x y  => ~ x = y
@@ -392,27 +392,91 @@ Definition Reval_op2 (o:Op2) : R -> R -> Prop :=
       | OpGt => Rgt
     end.
 
+Definition sumboolb {A B : Prop} (x : @sumbool A B) : bool :=
+  if x then true else false.
 
-Definition Reval_formula (e: PolEnv R) (ff : Formula Rcst) :=
-  let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs).
+
+Definition Reval_bop2 (o : Op2) : R -> R -> bool :=
+  match o with
+  | OpEq  => fun x y => sumboolb (Req_EM_T x y)
+  | OpNEq => fun x y => negb (sumboolb (Req_EM_T x y))
+  | OpLe  => fun x y => (sumboolb (Rle_lt_dec x y))
+  | OpGe  => fun x y => (sumboolb (Rge_gt_dec x y))
+  | OpLt  => fun x y => (sumboolb (Rlt_le_dec x y))
+  | OpGt  => fun x y => (sumboolb (Rgt_dec x y))
+  end.
+
+Lemma pop2_bop2 :
+  forall (op : Op2) (r1 r2 : R), is_true (Reval_bop2 op r1 r2) <-> Reval_pop2 op r1 r2.
+Proof.
+  unfold is_true.
+  destruct op ; simpl; intros;
+  match goal with
+  | |- context[sumboolb (?F ?X ?Y)] =>
+    destruct (F X Y) ; simpl; intuition try congruence
+  end.
+  - apply Rlt_not_le in r. tauto.
+  - apply Rgt_not_ge in r. tauto.
+  - apply Rlt_not_le in H. tauto.
+Qed.
+
+Definition Reval_op2 (k: Tauto.kind) :  Op2 ->  R -> R -> Tauto.rtyp k:=
+  if k as k0 return (Op2 -> R -> R -> Tauto.rtyp k0)
+  then Reval_pop2 else Reval_bop2.
+
+Lemma Reval_op2_hold : forall b op q1 q2,
+    Tauto.hold b (Reval_op2 b op q1 q2) <-> Reval_pop2 op q1 q2.
+Proof.
+  destruct b.
+  simpl ; tauto.
+  simpl. apply pop2_bop2.
+Qed.
+
+Definition Reval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Rcst) :=
+  let (lhs,o,rhs) := ff in Reval_op2 k o (Reval_expr e lhs) (Reval_expr e rhs).
 
 
 Definition Reval_formula' :=
   eval_sformula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst.
 
-Definition QReval_formula := 
-  eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow .
+Lemma Reval_pop2_eval_op2 : forall o e1 e2,
+  Reval_pop2 o e1 e2  <->
+  eval_op2 eq Rle Rlt o e1 e2.
+Proof.
+  destruct o ; simpl ; try tauto.
+  split.
+  apply Rge_le.
+  apply Rle_ge.
+Qed.
 
-Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.
+Lemma Reval_formula_compat : forall env b f, Tauto.hold b (Reval_formula env b f) <-> Reval_formula' env f.
 Proof.
   intros.
   unfold Reval_formula.
   destruct f.
   unfold Reval_formula'.
-  unfold Reval_expr.
-  split ; destruct Fop ; simpl ; auto.
-  apply Rge_le.
-  apply Rle_ge.
+  simpl.
+  rewrite Reval_op2_hold.
+  apply Reval_pop2_eval_op2.
+Qed.
+
+Definition QReval_expr := eval_pexpr Rplus Rmult Rminus Ropp Q2R to_nat pow.
+
+Definition QReval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Q) :=
+  let (lhs,o,rhs) := ff in Reval_op2 k o (QReval_expr e lhs) (QReval_expr e rhs).
+
+
+Definition QReval_formula' :=
+  eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow.
+
+Lemma QReval_formula_compat : forall env b f, Tauto.hold b (QReval_formula env b f) <-> QReval_formula' env f.
+Proof.
+  intros.
+  unfold QReval_formula.
+  destruct f.
+  unfold QReval_formula'.
+  rewrite Reval_op2_hold.
+  apply Reval_pop2_eval_op2.
 Qed.
 
 Definition Qeval_nformula :=
@@ -451,7 +515,7 @@ Definition runsat := check_inconsistent 0%Q Qeq_bool Qle_bool.
 
 Definition rdeduce := nformula_plus_nformula 0%Q Qplus Qeq_bool.
 
-Definition RTautoChecker (f : BFormula (Formula Rcst)) (w: list RWitness)  : bool :=
+Definition RTautoChecker (f : BFormula (Formula Rcst) Tauto.isProp) (w: list RWitness)  : bool :=
   @tauto_checker (Formula Q) (NFormula Q)
   unit runsat rdeduce
   (Rnormalise unit) (Rnegate unit)
@@ -463,18 +527,20 @@ Proof.
   unfold RTautoChecker.
   intros TC env.
   apply tauto_checker_sound with (eval:=QReval_formula) (eval':=    Qeval_nformula) (env := env) in TC.
-  - change (eval_f (fun x : Prop => x) (QReval_formula env))
+  - change (eval_f e_rtyp (QReval_formula env))
       with
         (eval_bf  (QReval_formula env)) in TC.
     rewrite eval_bf_map in TC.
     unfold eval_bf in TC.
     rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto.
-  intro.
-  unfold QReval_formula.
-  rewrite <- eval_formulaSC  with (phiS := R_of_Rcst).
-  rewrite Reval_formula_compat.
-  tauto.
-  intro. rewrite Q_of_RcstR. reflexivity.
+    intros.
+    apply Tauto.hold_eiff.
+    rewrite QReval_formula_compat.
+    unfold QReval_formula'.
+    rewrite <- eval_formulaSC  with (phiS := R_of_Rcst).
+    rewrite Reval_formula_compat.
+    tauto.
+    intro. rewrite Q_of_RcstR. reflexivity.
   -
   apply Reval_nformula_dec.
   - destruct t.
@@ -482,8 +548,12 @@ Proof.
   - unfold rdeduce.
     intros. revert H.
     eapply (nformula_plus_nformula_correct Rsor QSORaddon); eauto.
-  - now apply (cnf_normalise_correct Rsor QSORaddon).
-  - intros. now eapply (cnf_negate_correct Rsor QSORaddon); eauto.
+  -
+    intros.
+    rewrite QReval_formula_compat.
+    eapply (cnf_normalise_correct Rsor QSORaddon) ; eauto.
+  - intros. rewrite Tauto.hold_eNOT. rewrite QReval_formula_compat.
+    now eapply (cnf_negate_correct Rsor QSORaddon); eauto.
   - intros t w0.
     unfold eval_tt.
     intros.
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index 6e89089355..dddced5739 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -17,49 +17,64 @@
 Require Import List.
 Require Import Refl.
 Require Import Bool.
+Require Import Relation_Definitions Setoid.
 
 Set Implicit Arguments.
 
+(** Formulae are either interpreted over Prop or bool. *)
+Inductive kind : Type :=
+|isProp
+|isBool.
+
+Register isProp as micromega.kind.isProp.
+Register isBool as micromega.kind.isBool.
+
 
 Section S.
   Context {TA  : Type}. (* type of interpreted atoms *)
-  Context {TX  : Type}. (* type of uninterpreted terms (Prop) *)
+  Context {TX  : kind -> Type}. (* type of uninterpreted terms (Prop) *)
   Context {AA  : Type}. (* type of annotations for atoms *)
   Context {AF  : Type}. (* type of formulae identifiers *)
 
-   Inductive GFormula  : Type :=
-  | TT   : GFormula
-  | FF   : GFormula
-  | X    : TX -> GFormula
-  | A    : TA -> AA -> GFormula
-  | Cj   : GFormula  -> GFormula  -> GFormula
-  | D    : GFormula  -> GFormula  -> GFormula
-  | N    : GFormula  -> GFormula
-  | I    : GFormula  -> option AF -> GFormula  -> GFormula.
+  Inductive GFormula  : kind -> Type :=
+  | TT   : forall (k: kind), GFormula k
+  | FF   : forall (k: kind), GFormula k
+  | X    : forall (k: kind), TX k -> GFormula k
+  | A    : forall (k: kind), TA -> AA -> GFormula k
+  | AND  : forall (k: kind), GFormula k -> GFormula k -> GFormula k
+  | OR   : forall (k: kind), GFormula k -> GFormula k -> GFormula k
+  | NOT  : forall (k: kind), GFormula k -> GFormula k
+  | IMPL : forall (k: kind), GFormula k -> option AF -> GFormula k -> GFormula k
+  | IFF  : forall (k: kind), GFormula k -> GFormula k -> GFormula k
+  | EQ   : GFormula isBool -> GFormula isBool -> GFormula isProp.
 
   Register TT as micromega.GFormula.TT.
   Register FF as micromega.GFormula.FF.
   Register X  as micromega.GFormula.X.
   Register A  as micromega.GFormula.A.
-  Register Cj as micromega.GFormula.Cj.
-  Register D  as micromega.GFormula.D.
-  Register N  as micromega.GFormula.N.
-  Register I  as micromega.GFormula.I.
+  Register AND as micromega.GFormula.AND.
+  Register OR  as micromega.GFormula.OR.
+  Register NOT  as micromega.GFormula.NOT.
+  Register IMPL  as micromega.GFormula.IMPL.
+  Register IFF  as micromega.GFormula.IFF.
+  Register EQ  as micromega.GFormula.EQ.
 
 
   Section MAPX.
-    Variable F : TX -> TX.
+    Variable F : forall k, TX k -> TX k.
 
-    Fixpoint mapX (f : GFormula) : GFormula :=
+    Fixpoint mapX (k:kind) (f : GFormula k) : GFormula k :=
       match f with
-      | TT => TT
-      | FF => FF
-      | X x => X (F x)
-      | A a an => A a an
-      | Cj f1 f2 => Cj (mapX f1) (mapX f2)
-      | D f1 f2  => D (mapX f1) (mapX f2)
-      | N f      => N (mapX f)
-      | I f1 o f2 => I (mapX f1) o (mapX f2)
+      | TT k => TT k
+      | FF k => FF k
+      | X x => X (F  x)
+      | A k a an => A k a an
+      | AND f1 f2 => AND (mapX f1) (mapX f2)
+      | OR f1 f2  => OR (mapX f1) (mapX f2)
+      | NOT f     => NOT (mapX f)
+      | IMPL f1 o f2 => IMPL (mapX f1) o (mapX f2)
+      | IFF f1 f2    => IFF (mapX f1) (mapX f2)
+      | EQ f1 f2           => EQ (mapX f1) (mapX f2)
       end.
 
   End MAPX.
@@ -68,16 +83,17 @@ Section S.
     Variable ACC : Type.
     Variable F : ACC -> AA -> ACC.
 
-    Fixpoint foldA (f : GFormula) (acc : ACC) : ACC :=
+    Fixpoint foldA (k: kind) (f : GFormula k) (acc : ACC) : ACC :=
       match f with
-      | TT => acc
-      | FF => acc
+      | TT _ => acc
+      | FF _ => acc
       | X x => acc
-      | A a an => F acc an
-      | Cj f1 f2
-      | D f1 f2
-      | I f1 _ f2 => foldA f1 (foldA f2 acc)
-      | N f      => foldA f acc
+      | A _ a an => F acc an
+      | AND f1 f2
+      | OR f1 f2
+      | IFF f1 f2
+      | IMPL f1 _ f2 | EQ f1 f2 => foldA f1 (foldA f2 acc)
+      | NOT f     => foldA f acc
       end.
 
   End FOLDANNOT.
@@ -89,84 +105,212 @@ Section S.
     | Some id => id :: l
     end.
 
-  Fixpoint ids_of_formula f :=
+  Fixpoint ids_of_formula (k: kind) (f:GFormula k) :=
     match f with
-    | I f id f' => cons_id id (ids_of_formula f')
+    | IMPL f id f' => cons_id id (ids_of_formula f')
     |  _           => nil
     end.
 
-  Fixpoint collect_annot (f : GFormula) : list AA :=
+  Fixpoint collect_annot (k: kind) (f : GFormula k) : list AA :=
     match f with
-    | TT | FF | X _ => nil
-    | A _ a => a ::nil
-    | Cj f1 f2
-    | D  f1 f2
-    | I f1 _ f2  => collect_annot f1 ++ collect_annot f2
-    | N  f       => collect_annot f
+    | TT _ | FF _ | X _ => nil
+    | A _ _ a => a ::nil
+    | AND f1 f2
+    | OR  f1 f2
+    | IFF f1 f2 | EQ f1 f2
+    | IMPL f1 _ f2  => collect_annot f1 ++ collect_annot f2
+    | NOT  f  => collect_annot f
     end.
 
-  Variable ex : TX -> Prop. (* [ex] will be the identity *)
+  Definition rtyp (k: kind) : Type := if k then Prop else bool.
 
-  Section EVAL.
+  Variable ex : forall (k: kind), TX k -> rtyp k. (* [ex] will be the identity *)
 
-  Variable ea : TA -> Prop.
+  Section EVAL.
 
-  Fixpoint eval_f (f:GFormula) {struct f}: Prop :=
-  match f with
-  | TT  => True
-  | FF  => False
-  | A a _ =>  ea a
-  | X  p => ex p
-  | Cj e1 e2 => (eval_f e1) /\ (eval_f e2)
-  | D e1 e2  => (eval_f e1) \/ (eval_f e2)
-  | N e     => ~ (eval_f e)
-  | I f1 _ f2 => (eval_f f1) -> (eval_f f2)
-  end.
+    Variable ea : forall (k: kind), TA -> rtyp k.
+
+    Definition eTT (k: kind) : rtyp k :=
+      if k as k' return  rtyp k' then True else true.
+
+    Definition eFF (k: kind) : rtyp k :=
+      if k as k' return  rtyp k' then False else false.
+
+    Definition eAND (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+      if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+      then and else andb.
+
+    Definition eOR (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+      if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+      then or else orb.
+
+    Definition eIMPL (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+      if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+      then (fun x y => x -> y) else implb.
+
+    Definition eIFF (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+      if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+      then iff else eqb.
+
+    Definition eNOT (k: kind) : rtyp k -> rtyp k :=
+      if k as k' return rtyp k' -> rtyp k'
+      then not else negb.
+
+    Fixpoint eval_f (k: kind) (f:GFormula k) {struct f}: rtyp k :=
+      match f in GFormula k' return rtyp k' with
+      | TT tk => eTT tk
+      | FF tk => eFF tk
+      | A k a _ =>  ea k a
+      | X p => ex  p
+      | @AND k e1 e2 => eAND k (eval_f  e1) (eval_f e2)
+      | @OR k e1 e2  => eOR k (eval_f e1) (eval_f e2)
+      | @NOT k e     => eNOT k (eval_f e)
+      | @IMPL k f1 _ f2 => eIMPL k (eval_f f1)  (eval_f f2)
+      | @IFF k f1 f2    => eIFF k (eval_f f1) (eval_f f2)
+      | EQ f1 f2    => (eval_f f1) = (eval_f f2)
+      end.
 
+    Lemma eval_f_rew : forall k (f:GFormula k),
+        eval_f f =
+        match f in GFormula k' return rtyp k' with
+        | TT tk => eTT tk
+        | FF tk => eFF tk
+        | A k a _ =>  ea k a
+        | X p => ex  p
+        | @AND k e1 e2 => eAND k (eval_f  e1) (eval_f e2)
+        | @OR k e1 e2  => eOR k (eval_f e1) (eval_f e2)
+        | @NOT k e     => eNOT k (eval_f e)
+        | @IMPL k f1 _ f2 => eIMPL k (eval_f f1)  (eval_f f2)
+        | @IFF k f1 f2    => eIFF k (eval_f f1) (eval_f f2)
+        | EQ f1 f2    => (eval_f f1) = (eval_f f2)
+        end.
+    Proof.
+      destruct f ; reflexivity.
+    Qed.
 
   End EVAL.
 
 
+  Definition hold (k: kind) : rtyp k ->  Prop :=
+    if k as k0 return (rtyp k0 -> Prop) then fun x  => x else is_true.
 
+  Definition eiff (k: kind) : rtyp k -> rtyp k -> Prop :=
+    if k as k' return rtyp k' -> rtyp k' -> Prop then iff else @eq bool.
 
+  Lemma eiff_refl : forall (k: kind) (x : rtyp k),
+      eiff k x x.
+  Proof.
+    destruct k ; simpl; tauto.
+  Qed.
 
-  Lemma eval_f_morph :
-    forall  (ev ev' : TA -> Prop) (f : GFormula),
-      (forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f).
+  Lemma eiff_sym : forall k (x y : rtyp k), eiff k x y -> eiff k y x.
+  Proof.
+    destruct k ; simpl; intros ; intuition.
+  Qed.
+
+  Lemma eiff_trans : forall k (x y z : rtyp k), eiff k x y -> eiff k y z -> eiff k x z.
+  Proof.
+    destruct k ; simpl; intros ; intuition congruence.
+  Qed.
+
+  Lemma hold_eiff : forall (k: kind) (x y : rtyp k),
+      (hold k x <-> hold k y) <-> eiff k x y.
+  Proof.
+    destruct k ; simpl.
+    - tauto.
+    - unfold is_true.
+      destruct x,y ; intuition congruence.
+  Qed.
+
+  Instance eiff_eq (k: kind) : Equivalence (eiff k).
+  Proof.
+    constructor.
+    - exact (eiff_refl k).
+    - exact (eiff_sym k).
+    - exact (eiff_trans k).
+  Qed.
+
+  Add Parametric Morphism (k: kind) : (@eAND k) with signature eiff k ==> eiff k ==> eiff k as eAnd_morph.
+  Proof.
+    intros.
+    destruct k ; simpl in *; intuition congruence.
+  Qed.
+
+  Add Parametric Morphism (k: kind) : (@eOR k) with signature eiff k ==> eiff k ==> eiff k as eOR_morph.
+  Proof.
+    intros.
+    destruct k ; simpl in *; intuition congruence.
+  Qed.
+
+  Add Parametric Morphism (k: kind) : (@eIMPL k) with signature eiff k ==> eiff k ==> eiff k as eIMPL_morph.
+  Proof.
+    intros.
+    destruct k ; simpl in *; intuition congruence.
+  Qed.
+
+  Add Parametric Morphism (k: kind) : (@eIFF k) with signature eiff k ==> eiff k ==> eiff k as eIFF_morph.
   Proof.
-    induction f ; simpl ; try tauto.
     intros.
-    apply H.
+    destruct k ; simpl in *; intuition congruence.
   Qed.
 
+  Add Parametric Morphism (k: kind) : (@eNOT k) with signature eiff k ==> eiff k as eNOT_morph.
+  Proof.
+    intros.
+    destruct k ; simpl in *; intuition congruence.
+  Qed.
+
+  Lemma eval_f_morph :
+    forall  (ev ev' : forall (k: kind), TA -> rtyp k),
+      (forall k a, eiff k (ev k a) (ev' k a)) ->
+      forall (k: kind)(f : GFormula k),
+        (eiff k (eval_f ev f) (eval_f ev' f)).
+  Proof.
+    induction f ; simpl.
+    - reflexivity.
+    - reflexivity.
+    - reflexivity.
+    - apply H.
+    - rewrite IHf1. rewrite IHf2. reflexivity.
+    - rewrite IHf1. rewrite IHf2. reflexivity.
+    - rewrite IHf. reflexivity.
+    - rewrite IHf1. rewrite IHf2. reflexivity.
+    - rewrite IHf1. rewrite IHf2. reflexivity.
+    - simpl in *. intuition congruence.
+  Qed.
 
 End S.
 
 
 
 (** Typical boolean formulae *)
-Definition BFormula (A : Type) := @GFormula A Prop unit unit.
+Definition eKind (k: kind) := if k then Prop else bool.
+Register eKind as micromega.eKind.
+
+Definition BFormula (A : Type) := @GFormula A eKind unit unit.
 
 Register BFormula as micromega.BFormula.type.
 
 Section MAPATOMS.
   Context {TA TA':Type}.
-  Context {TX  : Type}.
+  Context {TX  : kind -> Type}.
   Context {AA  : Type}.
   Context {AF  : Type}.
 
 
-Fixpoint map_bformula (fct : TA -> TA') (f : @GFormula TA TX AA AF ) : @GFormula TA' TX AA AF :=
-  match f with
-  | TT  => TT
-  | FF  => FF
-  | X p => X  p
-  | A a t => A (fct a) t
-  | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2)
-  | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2)
-  | N f     => N (map_bformula fct f)
-  | I f1 a f2 => I (map_bformula fct f1) a (map_bformula fct f2)
-  end.
+  Fixpoint map_bformula (k: kind)(fct : TA -> TA') (f : @GFormula TA TX AA AF k) : @GFormula TA' TX AA AF k:=
+    match f with
+    | TT k => TT k
+    | FF k => FF k
+    | X k p => X k p
+    | A k a t => A k (fct a) t
+    | AND f1 f2 => AND (map_bformula fct f1) (map_bformula fct f2)
+    | OR f1 f2 => OR (map_bformula fct f1) (map_bformula fct f2)
+    | NOT f     => NOT (map_bformula fct f)
+    | IMPL f1 a f2 => IMPL (map_bformula fct f1) a (map_bformula fct f2)
+    | IFF f1 f2 => IFF (map_bformula fct f1) (map_bformula fct f2)
+    | EQ f1 f2  => EQ (map_bformula fct f1) (map_bformula fct f2)
+    end.
 
 End MAPATOMS.
 
@@ -204,345 +348,458 @@ Section S.
   (** Our cnf is optimised and detects contradictions on the fly. *)
 
   Fixpoint add_term (t: Term' * Annot) (cl : clause) : option clause :=
-      match cl with
-      | nil =>
-        match deduce (fst t) (fst t) with
-        | None =>  Some (t ::nil)
-        | Some u => if unsat u then None else Some (t::nil)
+    match cl with
+    | nil =>
+      match deduce (fst t) (fst t) with
+      | None =>  Some (t ::nil)
+      | Some u => if unsat u then None else Some (t::nil)
+      end
+    | t'::cl =>
+      match deduce (fst t) (fst t') with
+      | None =>
+        match add_term t cl with
+        | None => None
+        | Some cl' => Some (t' :: cl')
         end
-      | t'::cl =>
-        match deduce (fst t) (fst t') with
-        | None =>
+      | Some u =>
+        if unsat u then None else
           match add_term t cl with
           | None => None
           | Some cl' => Some (t' :: cl')
           end
-        | Some u =>
-          if unsat u then None else
-            match add_term t cl with
-            | None => None
-            | Some cl' => Some (t' :: cl')
-            end
+      end
+    end.
+
+  Fixpoint or_clause (cl1 cl2 : clause) : option clause :=
+    match cl1 with
+    | nil => Some cl2
+    | t::cl => match add_term t cl2 with
+               | None => None
+               | Some cl' => or_clause cl cl'
+               end
+    end.
+
+  Definition xor_clause_cnf (t:clause) (f:cnf) : cnf :=
+    List.fold_left (fun acc e =>
+                      match or_clause t e with
+                      | None => acc
+                      | Some cl => cl :: acc
+                      end) f nil .
+
+  Definition or_clause_cnf (t: clause) (f:cnf) : cnf :=
+    match t with
+    | nil => f
+    | _   => xor_clause_cnf t f
+    end.
+
+
+  Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
+    match f with
+    | nil => cnf_tt
+    | e :: rst => (or_cnf rst f') +++ (or_clause_cnf e f')
+    end.
+
+
+  Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf :=
+    f1 +++ f2.
+
+  (** TX is Prop in Coq and EConstr.constr in Ocaml.
+      AF is unit in Coq and Names.Id.t in Ocaml
+   *)
+  Definition TFormula (TX: kind -> Type) (AF: Type) := @GFormula Term TX Annot AF.
+
+
+  Definition is_cnf_tt (c : cnf) : bool :=
+    match c with
+    | nil => true
+    | _  => false
+    end.
+
+  Definition is_cnf_ff (c : cnf) : bool :=
+    match c with
+    | nil::nil => true
+    | _        => false
+    end.
+
+  Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
+    if is_cnf_ff f1 || is_cnf_ff f2
+    then cnf_ff
+    else
+      if is_cnf_tt f2
+      then f1
+      else and_cnf f1 f2.
+
+
+  Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
+    if is_cnf_tt f1 || is_cnf_tt f2
+    then cnf_tt
+    else if is_cnf_ff f2
+         then f1 else or_cnf f1 f2.
+
+  Section REC.
+    Context {TX : kind -> Type}.
+    Context {AF : Type}.
+
+    Variable REC : forall (pol : bool) (k: kind) (f : TFormula TX AF k), cnf.
+
+    Definition mk_and (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):=
+      (if pol then and_cnf_opt else or_cnf_opt) (REC pol f1) (REC pol f2).
+
+    Definition mk_or (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):=
+      (if pol then or_cnf_opt else and_cnf_opt) (REC pol f1) (REC pol f2).
+
+    Definition mk_impl (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):=
+      (if pol then or_cnf_opt else and_cnf_opt) (REC (negb pol) f1) (REC pol f2).
+
+
+    Definition mk_iff (k: kind) (pol:bool) (f1 f2: TFormula TX AF k):=
+      or_cnf_opt (and_cnf_opt (REC (negb pol) f1) (REC false f2))
+                 (and_cnf_opt (REC pol f1) (REC true f2)).
+
+
+  End REC.
+
+  Definition is_bool {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula TX AF k) :=
+    match f with
+    | TT _ => Some true
+    | FF _ => Some false
+    | _    => None
+    end.
+
+  Lemma is_bool_inv : forall {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula  TX AF k) res,
+      is_bool f = Some res -> f = if res then TT _ else FF _.
+  Proof.
+    intros.
+    destruct f ; inversion H; reflexivity.
+  Qed.
+
+
+  Fixpoint xcnf {TX : kind -> Type} {AF: Type} (pol : bool) (k: kind) (f : TFormula TX AF k)  {struct f}: cnf :=
+    match f with
+    | TT _ => if pol then cnf_tt else cnf_ff
+    | FF _ => if pol then cnf_ff else cnf_tt
+    | X _ p => if pol then cnf_ff else cnf_ff (* This is not complete - cannot negate any proposition *)
+    | A _ x t => if pol then normalise x  t else negate x  t
+    | NOT e  => xcnf (negb pol) e
+    | AND e1 e2 => mk_and xcnf pol e1 e2
+    | OR e1 e2  => mk_or xcnf pol e1 e2
+    | IMPL e1 _ e2 => mk_impl xcnf pol e1 e2
+    | IFF e1 e2 => match is_bool e2 with
+                   | Some isb => xcnf (if isb then pol else negb pol) e1
+                   | None  => mk_iff xcnf pol e1 e2
+                   end
+    | EQ e1 e2 =>
+      match is_bool e2 with
+      | Some isb => xcnf (if isb then pol else negb pol) e1
+      | None  => mk_iff xcnf pol e1 e2
+      end
+    end.
+
+  Section CNFAnnot.
+
+    (** Records annotations used to optimise the cnf.
+          Those need to be kept when pruning the formula.
+          For efficiency, this is a separate function.
+     *)
+
+    Fixpoint radd_term (t : Term' * Annot) (cl : clause) : clause + list Annot :=
+      match cl with
+      | nil => (* if t is unsat, the clause is empty BUT t is needed. *)
+        match deduce (fst t) (fst t) with
+        | Some u => if unsat u then inr ((snd t)::nil) else inl (t::nil)
+        | None   => inl (t::nil)
+        end
+      | t'::cl => (* if t /\ t' is unsat, the clause is empty BUT t & t' are needed *)
+        match deduce (fst t) (fst t') with
+        | Some u => if unsat u then inr ((snd t)::(snd t')::nil)
+                    else match radd_term t cl with
+                         | inl cl' => inl (t'::cl')
+                         | inr l   => inr l
+                         end
+        | None  => match radd_term t cl  with
+                   | inl cl' => inl (t'::cl')
+                   | inr l   => inr l
+                   end
         end
       end.
 
-    Fixpoint or_clause (cl1 cl2 : clause) : option clause :=
+    Fixpoint ror_clause cl1 cl2 :=
       match cl1 with
-      | nil => Some cl2
-      | t::cl => match add_term t cl2 with
-               | None => None
-               | Some cl' => or_clause cl cl'
+      | nil => inl cl2
+      | t::cl => match radd_term t cl2 with
+                 | inl cl' => ror_clause cl cl'
+                 | inr l   => inr l
                  end
       end.
 
-    Definition xor_clause_cnf (t:clause) (f:cnf) : cnf :=
-      List.fold_left (fun acc e =>
-                         match or_clause t e with
-                         | None => acc
-                         | Some cl => cl :: acc
-                         end) f nil .
+    Definition xror_clause_cnf t f :=
+      List.fold_left (fun '(acc,tg) e  =>
+                        match ror_clause t e with
+                        | inl cl => (cl :: acc,tg)
+                        | inr l => (acc,tg+++l)
+                        end) f (nil,nil).
 
-    Definition or_clause_cnf (t: clause) (f:cnf) : cnf :=
+    Definition ror_clause_cnf t f :=
       match t with
-      | nil => f
-      | _   => xor_clause_cnf t f
+      | nil => (f,nil)
+      | _   => xror_clause_cnf t f
       end.
 
 
-    Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
+    Fixpoint ror_cnf (f f':list clause) :=
       match f with
-      | nil => cnf_tt
-      | e :: rst => (or_cnf rst f') +++ (or_clause_cnf e f')
+      | nil => (cnf_tt,nil)
+      | e :: rst =>
+        let (rst_f',t) := ror_cnf rst f' in
+        let (e_f', t') := ror_clause_cnf e f' in
+        (rst_f' +++ e_f', t +++ t')
       end.
 
+    Definition annot_of_clause (l : clause) : list Annot :=
+      List.map snd l.
 
-    Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf :=
-      f1 +++ f2.
+    Definition annot_of_cnf (f : cnf) : list Annot :=
+      List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil.
 
-    (** TX is Prop in Coq and EConstr.constr in Ocaml.
-      AF i s unit in Coq and Names.Id.t in Ocaml
-     *)
-    Definition TFormula (TX: Type) (AF: Type) := @GFormula Term TX Annot AF.
 
+    Definition ror_cnf_opt f1 f2 :=
+      if is_cnf_tt f1
+      then (cnf_tt ,  nil)
+      else if is_cnf_tt f2
+           then (cnf_tt, nil)
+           else if is_cnf_ff f2
+                then (f1,nil)
+                else ror_cnf f1 f2.
 
-    Definition is_cnf_tt (c : cnf) : bool :=
-      match c with
-      | nil => true
-      | _  => false
-      end.
 
-    Definition is_cnf_ff (c : cnf) : bool :=
-      match c with
-      | nil::nil => true
-      | _        => false
+    Definition ocons {A : Type} (o : option A) (l : list A) : list A :=
+      match o with
+      | None => l
+      | Some e => e ::l
       end.
 
-    Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
-      if is_cnf_ff f1 || is_cnf_ff f2
-      then cnf_ff
-      else and_cnf f1 f2.
-
-    Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
-      if is_cnf_tt f1 || is_cnf_tt f2
-      then cnf_tt
-      else if is_cnf_ff f2
-           then f1 else or_cnf f1 f2.
+    Definition ratom (c : cnf) (a : Annot) : cnf * list Annot :=
+      if is_cnf_ff c || is_cnf_tt c
+      then (c,a::nil)
+      else (c,nil). (* t is embedded in c *)
+
+    Section REC.
+      Context {TX : kind -> Type} {AF : Type}.
+
+      Variable RXCNF : forall (polarity: bool) (k: kind) (f: TFormula TX AF k) , cnf * list Annot.
+
+      Definition rxcnf_and (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+        let '(e1,t1) := RXCNF polarity e1 in
+        let '(e2,t2) := RXCNF polarity e2 in
+        if polarity
+        then  (and_cnf_opt e1  e2, t1 +++ t2)
+        else let (f',t') := ror_cnf_opt e1 e2 in
+             (f', t1 +++ t2 +++ t').
+
+      Definition rxcnf_or (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+        let '(e1,t1) := RXCNF polarity e1 in
+        let '(e2,t2) := RXCNF polarity e2 in
+        if polarity
+        then let (f',t') := ror_cnf_opt e1 e2 in
+             (f', t1 +++ t2 +++ t')
+        else (and_cnf_opt e1 e2, t1 +++ t2).
+
+      Definition rxcnf_impl (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+        let '(e1 , t1) := (RXCNF (negb polarity) e1) in
+        if polarity
+        then
+          if is_cnf_ff e1
+          then
+            RXCNF polarity e2
+          else (* compute disjunction *)
+            let '(e2 , t2) := (RXCNF polarity e2) in
+            let (f',t') := ror_cnf_opt e1 e2 in
+            (f', t1 +++ t2 +++ t') (* record the hypothesis *)
+        else
+          let '(e2 , t2) := (RXCNF polarity e2) in
+          (and_cnf_opt e1 e2, t1 +++ t2).
+
+      Definition rxcnf_iff (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+        let '(c1,t1) := RXCNF (negb polarity) e1 in
+        let '(c2,t2) := RXCNF false e2 in
+        let '(c3,t3) := RXCNF polarity e1 in
+        let '(c4,t4) := RXCNF true e2 in
+        let (f',t') := ror_cnf_opt (and_cnf_opt c1 c2) (and_cnf_opt c3 c4) in
+        (f', t1+++ t2+++t3 +++ t4 +++ t')
+      .
+
+    End REC.
+
+    Fixpoint rxcnf {TX : kind -> Type} {AF: Type}(polarity : bool) (k: kind) (f : TFormula TX AF k) : cnf * list Annot :=
 
-    Fixpoint xcnf {TX AF: Type} (pol : bool) (f : TFormula TX AF)  {struct f}: cnf :=
       match f with
-      | TT  => if pol then cnf_tt else cnf_ff
-      | FF  => if pol then cnf_ff else cnf_tt
-      | X  p => if pol then cnf_ff else cnf_ff (* This is not complete - cannot negate any proposition *)
-      | A x t => if pol then normalise x  t else negate x  t
-      | N e  => xcnf (negb pol) e
-      | Cj e1 e2 =>
-        (if pol then and_cnf_opt else or_cnf_opt) (xcnf pol e1) (xcnf pol e2)
-      | D e1 e2  => (if pol then or_cnf_opt else and_cnf_opt) (xcnf pol e1) (xcnf pol e2)
-      | I e1 _ e2
-        =>  (if pol then or_cnf_opt else and_cnf_opt) (xcnf (negb pol) e1) (xcnf pol e2)
+      | TT _ => if polarity then (cnf_tt,nil) else (cnf_ff,nil)
+      | FF _  => if polarity then (cnf_ff,nil) else (cnf_tt,nil)
+      | X b p => if polarity then (cnf_ff,nil) else (cnf_ff,nil)
+      | A _ x t  => ratom (if polarity then normalise x t else negate x t) t
+      | NOT e  => rxcnf (negb polarity) e
+      | AND e1 e2 => rxcnf_and rxcnf polarity e1 e2
+      | OR e1 e2  => rxcnf_or rxcnf polarity e1 e2
+      | IMPL e1 a e2 => rxcnf_impl rxcnf polarity e1 e2
+      | IFF e1 e2 => rxcnf_iff rxcnf polarity e1 e2
+      | EQ e1 e2  => rxcnf_iff rxcnf polarity e1 e2
       end.
 
-    Section CNFAnnot.
-
-      (** Records annotations used to optimise the cnf.
-          Those need to be kept when pruning the formula.
-          For efficiency, this is a separate function.
-       *)
-
-      Fixpoint radd_term (t : Term' * Annot) (cl : clause) : clause + list Annot :=
-        match cl with
-        | nil => (* if t is unsat, the clause is empty BUT t is needed. *)
-          match deduce (fst t) (fst t) with
-          | Some u => if unsat u then inr ((snd t)::nil) else inl (t::nil)
-          | None   => inl (t::nil)
-          end
-        | t'::cl => (* if t /\ t' is unsat, the clause is empty BUT t & t' are needed *)
-          match deduce (fst t) (fst t') with
-          | Some u => if unsat u then inr ((snd t)::(snd t')::nil)
-                      else match radd_term t cl with
-                           | inl cl' => inl (t'::cl')
-                           | inr l   => inr l
-                           end
-          | None  => match radd_term t cl  with
-                     | inl cl' => inl (t'::cl')
-                     | inr l   => inr l
-                     end
-          end
-        end.
+    Section Abstraction.
+      Variable TX : kind -> Type.
+      Variable AF : Type.
 
-      Fixpoint ror_clause cl1 cl2 :=
-        match cl1 with
-        | nil => inl cl2
-        | t::cl => match radd_term t cl2 with
-                   | inl cl' => ror_clause cl cl'
-                   | inr l   => inr l
-                   end
-        end.
+      Class to_constrT : Type :=
+        {
+          mkTT   : forall (k: kind), TX k;
+          mkFF   : forall (k: kind), TX k;
+          mkA    : forall (k: kind), Term -> Annot -> TX k;
+          mkAND  : forall (k: kind), TX k -> TX k -> TX k;
+          mkOR   : forall (k: kind), TX k -> TX k -> TX k;
+          mkIMPL : forall (k: kind), TX k -> TX k -> TX k;
+          mkIFF  : forall (k: kind), TX k -> TX k -> TX k;
+          mkNOT  : forall (k: kind), TX k -> TX k;
+          mkEQ   : TX isBool -> TX isBool -> TX isProp
 
-      Definition xror_clause_cnf t f :=
-        List.fold_left (fun '(acc,tg) e  =>
-                           match ror_clause t e with
-                           | inl cl => (cl :: acc,tg)
-                           | inr l => (acc,tg+++l)
-                           end) f (nil,nil).
-
-      Definition ror_clause_cnf t f :=
-        match t with
-        | nil => (f,nil)
-        | _   => xror_clause_cnf t f
-        end.
+        }.
 
+      Context {to_constr : to_constrT}.
 
-      Fixpoint ror_cnf (f f':list clause) :=
+      Fixpoint aformula (k: kind) (f : TFormula TX AF k) : TX k :=
         match f with
-        | nil => (cnf_tt,nil)
-        | e :: rst =>
-          let (rst_f',t) := ror_cnf rst f' in
-          let (e_f', t') := ror_clause_cnf e f' in
-          (rst_f' +++ e_f', t +++ t')
+        | TT b => mkTT b
+        | FF b => mkFF b
+        | X b p => p
+        | A b x t => mkA b x t
+        | AND f1 f2 => mkAND  (aformula f1) (aformula f2)
+        | OR  f1 f2 => mkOR (aformula f1) (aformula f2)
+        | IMPL f1 o f2 => mkIMPL  (aformula f1) (aformula f2)
+        | IFF f1 f2 => mkIFF  (aformula f1) (aformula f2)
+        | NOT f     => mkNOT  (aformula f)
+        | EQ f1 f2  => mkEQ (aformula f1) (aformula f2)
         end.
 
-      Definition annot_of_clause (l : clause) : list Annot :=
-        List.map snd l.
-
-      Definition annot_of_cnf (f : cnf) : list Annot :=
-        List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil.
 
+      Definition is_X (k: kind) (f : TFormula TX AF k) : option (TX k) :=
+        match f with
+        | X _ p => Some p
+        | _   => None
+        end.
 
-      Definition ror_cnf_opt f1 f2 :=
-        if is_cnf_tt f1
-        then (cnf_tt ,  nil)
-        else if is_cnf_tt f2
-             then (cnf_tt, nil)
-             else if is_cnf_ff f2
-                  then (f1,nil)
-                  else ror_cnf f1 f2.
+      Definition is_X_inv : forall (k: kind) (f: TFormula TX AF k) x,
+          is_X f = Some x -> f = X k x.
+      Proof.
+        destruct f ; simpl ; try congruence.
+      Qed.
 
+      Variable needA : Annot -> bool.
 
-      Definition ocons {A : Type} (o : option A) (l : list A) : list A :=
-        match o with
-        | None => l
-        | Some e => e ::l
+      Definition abs_and (k: kind) (f1 f2 : TFormula TX AF k)
+                 (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k -> TFormula TX AF k) :=
+        match is_X f1 , is_X f2 with
+        | Some _  , _ | _ , Some _ => X k (aformula  (c k f1  f2))
+        |   _     , _ => c k f1 f2
         end.
 
-      Definition ratom (c : cnf) (a : Annot) : cnf * list Annot :=
-        if is_cnf_ff c || is_cnf_tt c
-        then (c,a::nil)
-        else (c,nil). (* t is embedded in c *)
-
-      Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) : cnf * list Annot :=
-        match f with
-        | TT => if polarity then (cnf_tt,nil) else (cnf_ff,nil)
-        | FF  => if polarity then (cnf_ff,nil) else (cnf_tt,nil)
-        | X p => if polarity then (cnf_ff,nil) else (cnf_ff,nil)
-        | A x t  => ratom (if polarity then normalise x t else negate x t) t
-        | N e  => rxcnf (negb polarity) e
-        | Cj e1 e2 =>
-          let '(e1,t1) := rxcnf polarity e1 in
-          let '(e2,t2) := rxcnf polarity e2 in
-          if polarity
-          then  (and_cnf_opt e1  e2, t1 +++ t2)
-          else let (f',t') := ror_cnf_opt e1 e2 in
-            (f', t1 +++ t2 +++ t')
-        | D e1 e2  =>
-          let '(e1,t1) := rxcnf polarity e1 in
-          let '(e2,t2) := rxcnf polarity e2 in
-          if polarity
-       then let (f',t') := ror_cnf_opt e1 e2 in
-            (f', t1 +++ t2 +++ t')
-          else (and_cnf_opt e1 e2, t1 +++ t2)
-        | I e1 a e2 =>
-          let '(e1 , t1) := (rxcnf (negb polarity) e1) in
-          if polarity
-          then
-            if is_cnf_ff e1
-            then
-              rxcnf polarity e2
-            else (* compute disjunction *)
-              let '(e2 , t2) := (rxcnf polarity e2) in
-              let (f',t') := ror_cnf_opt e1 e2 in
-              (f', t1 +++ t2 +++ t') (* record the hypothesis *)
-          else
-            let '(e2 , t2) := (rxcnf polarity e2) in
-            (and_cnf_opt e1 e2, t1 +++ t2)
+      Definition abs_or (k: kind) (f1 f2 : TFormula TX AF k)
+                 (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k -> TFormula TX AF k) :=
+        match is_X f1 , is_X f2 with
+        | Some _  , Some _ => X k (aformula (c k f1  f2))
+        |   _     , _ => c k f1 f2
         end.
 
+      Definition abs_not (k: kind) (f1 : TFormula TX AF k)
+                 (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k) :=
+        match is_X f1 with
+        | Some _   => X k (aformula (c k f1 ))
+        |   _  => c k f1
+        end.
 
-      Section Abstraction.
-        Variable TX : Type.
-        Variable AF : Type.
-
-        Class to_constrT : Type :=
-          {
-            mkTT : TX;
-            mkFF : TX;
-            mkA  : Term -> Annot -> TX;
-            mkCj : TX -> TX -> TX;
-            mkD  : TX -> TX -> TX;
-            mkI  : TX -> TX -> TX;
-            mkN  : TX -> TX
-          }.
-
-        Context {to_constr : to_constrT}.
-
-        Fixpoint aformula (f : TFormula TX AF) : TX :=
-          match f with
-          | TT => mkTT
-          | FF => mkFF
-          | X p => p
-          | A x t => mkA x t
-          | Cj f1 f2 => mkCj (aformula f1) (aformula f2)
-          | D  f1 f2 => mkD (aformula f1) (aformula f2)
-          | I f1 o f2 => mkI (aformula f1) (aformula f2)
-          | N f       => mkN (aformula f)
-          end.
 
+      Definition mk_arrow (o : option AF) (k: kind) (f1 f2: TFormula TX AF k) :=
+        match o with
+        | None => IMPL f1 None f2
+        | Some _ => if is_X f1 then f2 else IMPL f1 o f2
+        end.
 
-        Definition is_X (f : TFormula TX AF) : option TX :=
-          match f with
-          | X p => Some p
-          | _   => None
-          end.
+      Fixpoint abst_simpl  (k: kind) (f : TFormula TX AF k) : TFormula TX AF k:=
+        match f  with
+        | TT k => TT k
+        | FF k =>  FF k
+        | X k p => X k p
+        | A k x t => if needA t then A k x t else X k (mkA k x t)
+        | AND f1 f2 => AND (abst_simpl f1) (abst_simpl f2)
+        | OR f1 f2 =>  OR (abst_simpl f1) (abst_simpl f2)
+        | IMPL f1 o f2 => IMPL (abst_simpl f1) o (abst_simpl f2)
+        | NOT f => NOT (abst_simpl f)
+        | IFF f1 f2 => IFF (abst_simpl f1) (abst_simpl f2)
+        | EQ f1 f2  => EQ (abst_simpl f1) (abst_simpl f2)
+        end.
 
-        Definition is_X_inv : forall f x,
-            is_X f = Some x -> f = X x.
-        Proof.
-          destruct f ; simpl ; congruence.
-        Qed.
+      Section REC.
+        Variable REC : forall (pol : bool) (k: kind) (f : TFormula TX AF k), TFormula TX AF k.
 
+        Definition abst_and (pol : bool) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:=
+          (if pol then abs_and else abs_or) k (REC pol f1) (REC pol f2) AND.
 
-        Variable needA : Annot -> bool.
+        Definition abst_or (pol : bool) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:=
+          (if pol then abs_or else abs_and) k (REC pol f1) (REC pol f2) OR.
 
-        Definition abs_and (f1 f2 : TFormula TX AF)
-                   (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) :=
-          match is_X f1 , is_X f2 with
-          | Some _  , _ | _ , Some _ => X (aformula (c f1  f2))
-          |   _     , _ => c f1 f2
-          end.
+        Definition abst_impl (pol : bool) (o :option AF) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:=
+          (if pol then abs_or else abs_and) k (REC (negb pol) f1) (REC pol f2) (mk_arrow o).
 
-        Definition abs_or (f1 f2 : TFormula TX AF)
-                   (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) :=
+        Definition or_is_X (k: kind) (f1 f2: TFormula TX AF k) : bool :=
           match is_X f1 , is_X f2 with
-          | Some _  , Some _ => X (aformula (c f1  f2))
-          |   _     , _ => c f1 f2
+          | Some _ , _
+          | _ , Some _ => true
+          |  _ , _     => false
           end.
 
-        Definition mk_arrow (o : option AF) (f1 f2: TFormula TX AF) :=
-          match o with
-          | None => I f1 None f2
-          | Some _ => if is_X f1 then f2 else I f1 o f2
-          end.
+        Definition abs_iff  (k: kind) (nf1  ff2 f1 tf2 : TFormula TX AF k) (r: kind) (def : TFormula TX AF r) : TFormula TX AF r :=
+          if andb (or_is_X nf1 ff2) (or_is_X f1 tf2)
+          then X r (aformula def)
+          else def.
 
 
-        Fixpoint abst_form  (pol : bool) (f : TFormula TX AF) :=
-          match f with
-          | TT => if pol then TT else X mkTT
-          | FF => if pol then X mkFF else FF
-          | X p => X p
-          | A x t => if needA t then A x t else X (mkA x t)
-          | Cj f1 f2 =>
-            let f1 := abst_form pol f1 in
-            let f2 := abst_form pol f2 in
-            if pol then abs_and f1 f2 Cj
-            else abs_or f1 f2 Cj
-          | D f1 f2 =>
-            let f1 := abst_form pol f1 in
-            let f2 := abst_form pol f2 in
-            if pol then abs_or f1 f2 D
-            else abs_and f1 f2 D
-          | I f1 o f2 =>
-            let f1 := abst_form (negb pol) f1 in
-            let f2 := abst_form pol f2 in
-            if pol
-            then abs_or f1 f2 (mk_arrow o)
-            else abs_and f1 f2 (mk_arrow o)
-          | N f => let f := abst_form (negb pol) f in
-                   match is_X f with
-                   | Some a => X (mkN a)
-                   |  _     => N f
-                   end
-          end.
+        Definition abst_iff (pol : bool) (k: kind) (f1 f2: TFormula TX AF k) : TFormula TX AF k :=
+          abs_iff   (REC (negb pol) f1) (REC false f2) (REC pol f1) (REC true f2) (IFF (abst_simpl f1) (abst_simpl f2)).
 
+        Definition abst_eq (pol : bool)  (f1 f2: TFormula TX AF isBool) : TFormula TX AF isProp :=
+          abs_iff   (REC (negb pol) f1) (REC false f2) (REC pol f1) (REC true f2) (EQ (abst_simpl f1) (abst_simpl f2)).
 
+      End REC.
 
+      Fixpoint abst_form  (pol : bool) (k: kind) (f : TFormula TX AF k) : TFormula TX AF k:=
+        match f  with
+        | TT k => if pol then TT k else X k (mkTT k)
+        | FF k => if pol then X k (mkFF k) else FF k
+        | X k p => X k p
+        | A k x t => if needA t then A k x t else X k (mkA k x t)
+        | AND f1 f2 => abst_and abst_form pol f1 f2
+        | OR f1 f2 =>  abst_or abst_form pol f1 f2
+        | IMPL f1 o f2 => abst_impl abst_form pol o f1 f2
+        | NOT f => abs_not  (abst_form (negb pol) f) NOT
+        | IFF f1 f2 => abst_iff abst_form  pol f1 f2
+        | EQ f1 f2  => abst_eq abst_form pol f1 f2
+        end.
 
-        Lemma if_same : forall {A: Type} (b:bool) (t:A),
-            (if b then t else t) = t.
-        Proof.
-          destruct b ; reflexivity.
-        Qed.
+      Lemma if_same : forall {A: Type} (b: bool) (t:A),
+          (if b then t else t) = t.
+      Proof.
+        destruct b ; reflexivity.
+      Qed.
 
-        Lemma is_cnf_tt_cnf_ff :
-          is_cnf_tt cnf_ff = false.
-        Proof.
-          reflexivity.
-        Qed.
+      Lemma is_cnf_tt_cnf_ff :
+        is_cnf_tt cnf_ff = false.
+      Proof.
+        reflexivity.
+      Qed.
 
-        Lemma is_cnf_ff_cnf_ff :
-          is_cnf_ff cnf_ff = true.
-        Proof.
-          reflexivity.
-        Qed.
+      Lemma is_cnf_ff_cnf_ff :
+        is_cnf_ff cnf_ff = true.
+      Proof.
+        reflexivity.
+      Qed.
 
 
       Lemma is_cnf_tt_inv : forall f1,
@@ -587,9 +844,9 @@ Section S.
         reflexivity.
       Qed.
 
-      Lemma abs_and_pol : forall f1 f2 pol,
+      Lemma abs_and_pol : forall (k: kind) (f1 f2: TFormula TX AF k) pol,
           and_cnf_opt (xcnf pol f1) (xcnf pol f2) =
-          xcnf pol (abs_and f1 f2 (if pol then Cj else D)).
+          xcnf pol (abs_and f1 f2 (if pol then AND else OR)).
       Proof.
         unfold abs_and; intros.
         destruct (is_X f1) eqn:EQ1.
@@ -607,9 +864,9 @@ Section S.
         destruct pol ; simpl; auto.
       Qed.
 
-      Lemma abs_or_pol : forall f1 f2 pol,
+      Lemma abs_or_pol : forall (k: kind) (f1 f2:TFormula TX AF k) pol,
           or_cnf_opt (xcnf pol f1) (xcnf pol f2) =
-          xcnf pol (abs_or f1 f2 (if pol then D else Cj)).
+          xcnf pol (abs_or f1 f2 (if pol then OR else AND)).
       Proof.
         unfold abs_or; intros.
         destruct (is_X f1) eqn:EQ1.
@@ -629,8 +886,8 @@ Section S.
 
       Variable needA_all : forall a, needA a = true.
 
-      Lemma xcnf_true_mk_arrow_l : forall o t f,
-        xcnf true (mk_arrow o (X t) f) = xcnf true f.
+      Lemma xcnf_true_mk_arrow_l : forall b o t (f:TFormula TX AF b),
+          xcnf true (mk_arrow o (X b t) f) = xcnf true f.
       Proof.
         destruct o ; simpl; auto.
         intros. rewrite or_cnf_opt_cnf_ff. reflexivity.
@@ -647,8 +904,8 @@ Section S.
         apply if_cnf_tt.
       Qed.
 
-      Lemma xcnf_true_mk_arrow_r : forall o t f,
-          xcnf true (mk_arrow o  f (X t)) = xcnf false f.
+      Lemma xcnf_true_mk_arrow_r : forall b o t (f:TFormula TX AF b),
+          xcnf true (mk_arrow o  f (X b t)) = xcnf false f.
       Proof.
         destruct o ; simpl; auto.
         - intros.
@@ -660,9 +917,167 @@ Section S.
           apply or_cnf_opt_cnf_ff_r.
       Qed.
 
+      Lemma and_cnf_opt_cnf_ff_r : forall f,
+          and_cnf_opt f cnf_ff = cnf_ff.
+      Proof.
+        intros.
+        unfold and_cnf_opt.
+        rewrite is_cnf_ff_cnf_ff.
+        rewrite orb_comm. reflexivity.
+      Qed.
+
+      Lemma and_cnf_opt_cnf_ff : forall f,
+          and_cnf_opt cnf_ff f  = cnf_ff.
+      Proof.
+        intros.
+        unfold and_cnf_opt.
+        rewrite is_cnf_ff_cnf_ff.
+        reflexivity.
+      Qed.
+
+
+      Lemma and_cnf_opt_cnf_tt : forall f,
+          and_cnf_opt f cnf_tt   = f.
+      Proof.
+        intros.
+        unfold and_cnf_opt.
+        simpl. rewrite orb_comm.
+        simpl.
+        destruct (is_cnf_ff f) eqn:EQ ; auto.
+        apply is_cnf_ff_inv in EQ.
+        auto.
+      Qed.
+
+      Lemma is_bool_abst_simpl : forall b (f:TFormula TX AF b),
+          is_bool (abst_simpl f) = is_bool f.
+      Proof.
+        induction f ; simpl ; auto.
+        rewrite needA_all.
+        reflexivity.
+      Qed.
+
+      Lemma abst_simpl_correct : forall b (f:TFormula TX AF b) pol,
+          xcnf pol f = xcnf pol (abst_simpl f).
+      Proof.
+        induction f; simpl;intros;
+          unfold mk_and,mk_or,mk_impl, mk_iff;
+          rewrite <- ?IHf;
+          try (rewrite <- !IHf1; rewrite <- !IHf2);
+          try reflexivity.
+        - rewrite needA_all.
+          reflexivity.
+        - rewrite is_bool_abst_simpl.
+          destruct (is_bool f2); auto.
+        - rewrite is_bool_abst_simpl.
+          destruct (is_bool f2); auto.
+      Qed.
+
+      Ltac is_X :=
+        match goal with
+        | |-context[is_X ?X] =>
+          let f := fresh "EQ" in
+          destruct (is_X X) eqn:f ;
+          [apply is_X_inv in f|]
+        end.
+
+      Ltac cnf_simpl :=
+        repeat match goal with
+               | |- context[and_cnf_opt cnf_ff _ ] => rewrite and_cnf_opt_cnf_ff
+               | |- context[and_cnf_opt _ cnf_ff] => rewrite and_cnf_opt_cnf_ff_r
+               | |- context[and_cnf_opt _ cnf_tt] => rewrite and_cnf_opt_cnf_tt
+               | |- context[or_cnf_opt cnf_ff _] => rewrite or_cnf_opt_cnf_ff
+               | |- context[or_cnf_opt _ cnf_ff] => rewrite or_cnf_opt_cnf_ff_r
+               end.
+
+      Lemma or_is_X_inv : forall (k: kind) (f1 f2 : TFormula TX AF k),
+          or_is_X f1 f2 = true ->
+          exists k1, is_X f1 = Some k1 \/ is_X f2 = Some k1.
+      Proof.
+        unfold or_is_X.
+        intros k f1 f2.
+        repeat is_X.
+        exists t ; intuition.
+        exists t ; intuition.
+        exists t ; intuition.
+        congruence.
+      Qed.
+
+      Lemma mk_iff_is_bool : forall (k: kind) (f1 f2:TFormula TX AF k) pol,
+          match is_bool f2 with
+          | Some isb => xcnf (if isb then pol else negb pol) f1
+          | None => mk_iff xcnf pol f1 f2
+          end = mk_iff xcnf pol f1 f2.
+      Proof.
+        intros.
+        destruct (is_bool f2) eqn:EQ; auto.
+        apply is_bool_inv in EQ.
+        subst.
+        unfold mk_iff.
+        destruct b ; simpl; cnf_simpl; reflexivity.
+      Qed.
+
+      Lemma abst_iff_correct : forall
+          (k: kind)
+          (f1 f2 : GFormula k)
+          (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1))
+          (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2))
+          (pol : bool),
+          xcnf pol (IFF f1 f2) = xcnf pol (abst_iff abst_form pol f1 f2).
+      Proof.
+        intros; simpl.
+        assert (D1 :mk_iff xcnf pol f1 f2 = mk_iff xcnf pol (abst_simpl f1) (abst_simpl f2)).
+        {
+          simpl.
+          unfold mk_iff.
+          rewrite <- !abst_simpl_correct.
+          reflexivity.
+        }
+        rewrite mk_iff_is_bool.
+        unfold abst_iff,abs_iff.
+        destruct (      or_is_X (abst_form (negb pol) f1) (abst_form false f2) &&
+                                or_is_X (abst_form pol f1) (abst_form true f2)
+                 ) eqn:EQ1.
+        + simpl.
+          rewrite andb_true_iff in EQ1.
+          destruct EQ1 as (EQ1 & EQ2).
+          apply or_is_X_inv in EQ1.
+          apply or_is_X_inv in EQ2.
+          destruct EQ1 as (b1 & EQ1).
+          destruct EQ2 as (b2 & EQ2).
+          rewrite if_same.
+          unfold mk_iff.
+          rewrite !IHf1.
+          rewrite !IHf2.
+          destruct EQ1 as [EQ1 | EQ1] ; apply is_X_inv in EQ1;
+            destruct EQ2 as [EQ2 | EQ2] ; apply is_X_inv in EQ2;
+              rewrite EQ1; rewrite EQ2; simpl;
+                repeat rewrite if_same ; cnf_simpl; auto.
+        + simpl.
+          rewrite mk_iff_is_bool.
+          unfold mk_iff.
+          rewrite <- ! abst_simpl_correct.
+          reflexivity.
+      Qed.
+
+      Lemma abst_eq_correct : forall
+          (f1 f2 : GFormula isBool)
+          (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1))
+          (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2))
+          (pol : bool),
+          xcnf pol (EQ f1 f2) = xcnf pol (abst_form pol (EQ f1 f2)).
+      Proof.
+        intros.
+        change (xcnf pol (IFF f1 f2) = xcnf pol (abst_form pol (EQ f1 f2))).
+        rewrite abst_iff_correct by assumption.
+        simpl. unfold abst_iff, abst_eq.
+        unfold abs_iff.
+        destruct (or_is_X (abst_form (negb pol) f1) (abst_form false f2) &&
+                          or_is_X (abst_form pol f1) (abst_form true f2)
+                 ) ; auto.
+      Qed.
 
 
-      Lemma abst_form_correct : forall f pol,
+      Lemma abst_form_correct : forall b (f:TFormula TX AF b) pol,
           xcnf pol f = xcnf pol (abst_form pol f).
       Proof.
         induction f;intros.
@@ -671,27 +1086,24 @@ Section S.
         - simpl. reflexivity.
         - simpl. rewrite needA_all.
           reflexivity.
-        - simpl.
+        - simpl. unfold mk_and.
           specialize (IHf1 pol).
           specialize (IHf2 pol).
           rewrite IHf1.
           rewrite IHf2.
           destruct pol.
-          +
-            apply abs_and_pol; auto.
-          +
-            apply abs_or_pol; auto.
-        - simpl.
+          + apply abs_and_pol; auto.
+          + apply abs_or_pol.
+        - simpl. unfold mk_or.
           specialize (IHf1 pol).
           specialize (IHf2 pol).
           rewrite IHf1.
           rewrite IHf2.
           destruct pol.
-          +
-            apply abs_or_pol; auto.
-          +
-            apply abs_and_pol; auto.
+          + apply abs_or_pol; auto.
+          + apply abs_and_pol; auto.
         -  simpl.
+           unfold abs_not.
            specialize (IHf (negb pol)).
            destruct (is_X (abst_form (negb pol) f)) eqn:EQ1.
            + apply is_X_inv in EQ1.
@@ -699,381 +1111,438 @@ Section S.
              simpl in *.
              destruct pol ; auto.
            + simpl. congruence.
-        - simpl.
+        - simpl. unfold mk_impl.
           specialize (IHf1 (negb pol)).
           specialize (IHf2 pol).
           destruct pol.
-            +
-              simpl in *.
-              unfold abs_or.
-              destruct (is_X (abst_form false f1)) eqn:EQ1;
-                destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl.
-              * apply is_X_inv in EQ1.
-               apply is_X_inv in EQ2.
-               rewrite EQ1 in *.
-               rewrite EQ2 in *.
-               rewrite IHf1. rewrite IHf2.
-               simpl. reflexivity.
-              * apply is_X_inv in EQ1.
-               rewrite EQ1 in *.
-               rewrite IHf1.
-               simpl.
-               rewrite xcnf_true_mk_arrow_l.
-               rewrite or_cnf_opt_cnf_ff.
-               congruence.
-              * apply is_X_inv in EQ2.
-               rewrite EQ2 in *.
-               rewrite IHf2.
-               simpl.
-               rewrite xcnf_true_mk_arrow_r.
-               rewrite or_cnf_opt_cnf_ff_r.
-               congruence.
-              * destruct o ; simpl ; try congruence.
-                rewrite EQ1.
-                simpl. congruence.
-            +  simpl in *.
-               unfold abs_and.
-               destruct (is_X (abst_form true f1)) eqn:EQ1;
-                destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl.
-              * apply is_X_inv in EQ1.
+          +
+            simpl in *.
+            unfold abs_or.
+            destruct (is_X (abst_form false f1)) eqn:EQ1;
+              destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl.
+            * apply is_X_inv in EQ1.
+              apply is_X_inv in EQ2.
+              rewrite EQ1 in *.
+              rewrite EQ2 in *.
+              rewrite IHf1. rewrite IHf2.
+              simpl. reflexivity.
+            * apply is_X_inv in EQ1.
+              rewrite EQ1 in *.
+              rewrite IHf1.
+              simpl.
+              rewrite xcnf_true_mk_arrow_l.
+              rewrite or_cnf_opt_cnf_ff.
+              congruence.
+            * apply is_X_inv in EQ2.
+              rewrite EQ2 in *.
+              rewrite IHf2.
+              simpl.
+              rewrite xcnf_true_mk_arrow_r.
+              rewrite or_cnf_opt_cnf_ff_r.
+              congruence.
+            * destruct o ; simpl ; try congruence.
+              rewrite EQ1.
+              simpl. congruence.
+          +  simpl in *.
+             unfold abs_and.
+             destruct (is_X (abst_form true f1)) eqn:EQ1;
+               destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl.
+             * apply is_X_inv in EQ1.
                apply is_X_inv in EQ2.
                rewrite EQ1 in *.
                rewrite EQ2 in *.
                rewrite IHf1. rewrite IHf2.
                simpl. reflexivity.
-              * apply is_X_inv in EQ1.
+             * apply is_X_inv in EQ1.
                rewrite EQ1 in *.
                rewrite IHf1.
                simpl. reflexivity.
-              * apply is_X_inv in EQ2.
+             * apply is_X_inv in EQ2.
                rewrite EQ2 in *.
                rewrite IHf2.
                simpl. unfold and_cnf_opt.
                rewrite orb_comm. reflexivity.
-              * destruct o; simpl.
-                rewrite EQ1. simpl.
-                congruence.
-                congruence.
-        Qed.
-
-      End Abstraction.
-
-
-      End CNFAnnot.
-
-
-      Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl.
-      Proof.
-        induction a' ; simpl.
-        - intros.
-          destruct (deduce (fst a) (fst a)).
-          destruct (unsat t). congruence.
-          inversion H. reflexivity.
-          inversion H ;reflexivity.
-        - intros.
-          destruct (deduce (fst a0) (fst a)).
-          destruct (unsat t). congruence.
-          destruct (radd_term a0 a') eqn:RADD; try congruence.
-          inversion H. subst.
-          apply IHa' in RADD.
-          rewrite RADD.
-          reflexivity.
-          destruct (radd_term a0 a') eqn:RADD; try congruence.
-          inversion H. subst.
-          apply IHa' in RADD.
-          rewrite RADD.
-          reflexivity.
-      Qed.
-
-      Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl.
-      Proof.
-        induction a' ; simpl.
-        - intros.
-          destruct (deduce (fst a) (fst a)).
-          destruct (unsat t). congruence.
-          inversion H. reflexivity.
-          inversion H ;reflexivity.
-        - intros.
-          destruct (deduce (fst a0) (fst a)).
-          destruct (unsat t). congruence.
-          destruct (add_term a0 a') eqn:RADD; try congruence.
-          inversion H. subst.
-          apply IHa' in RADD.
-          rewrite RADD.
-          reflexivity.
-          destruct (add_term a0 a') eqn:RADD; try congruence.
-          inversion H. subst.
-          apply IHa' in RADD.
-          rewrite RADD.
-          reflexivity.
+             * destruct o; simpl.
+               rewrite EQ1. simpl.
+               congruence.
+               congruence.
+        -  apply abst_iff_correct; auto.
+        -  apply abst_eq_correct; auto.
       Qed.
 
-      Lemma xror_clause_clause : forall a f,
-          fst (xror_clause_cnf a f) = xor_clause_cnf a f.
-      Proof.
-        unfold xror_clause_cnf.
-        unfold xor_clause_cnf.
-        assert (ACC: fst (@nil clause,@nil Annot) = nil).
-        reflexivity.
-        intros.
-        set (F1:= (fun '(acc, tg) (e : clause) =>
-        match ror_clause a e with
-        | inl cl => (cl :: acc, tg)
-        | inr l => (acc, tg +++ l)
-        end)).
-        set (F2:= (fun (acc : list clause) (e : clause) =>
-     match or_clause a e with
-     | Some cl => cl :: acc
-     | None => acc
-     end)).
-        revert ACC.
-        generalize (@nil clause,@nil Annot).
-        generalize (@nil clause).
-        induction f ; simpl ; auto.
-        intros.
-        apply IHf.
-        unfold F1 , F2.
-        destruct p ; simpl in * ; subst.
-        clear.
-        revert a0.
-        induction a; simpl; auto.
-        intros.
-        destruct (radd_term a a1) eqn:RADD.
-        apply radd_term_term in RADD.
-        rewrite RADD.
-        auto.
-        destruct (add_term a a1) eqn:RADD'.
-        apply radd_term_term' in RADD'.
-        congruence.
-        reflexivity.
-      Qed.
+    End Abstraction.
 
-      Lemma ror_clause_clause : forall a f,
-          fst (ror_clause_cnf a f) = or_clause_cnf a f.
-      Proof.
-        unfold ror_clause_cnf,or_clause_cnf.
-        destruct a ; auto.
-        apply xror_clause_clause.
-      Qed.
 
-      Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2.
-      Proof.
-        induction f1 ; simpl ; auto.
-        intros.
-        specialize (IHf1  f2).
-        destruct(ror_cnf f1 f2).
-        rewrite <- ror_clause_clause.
-        destruct(ror_clause_cnf a f2).
-        simpl.
-        rewrite <- IHf1.
-        reflexivity.
-      Qed.
+  End CNFAnnot.
 
-      Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2.
-      Proof.
-        unfold ror_cnf_opt, or_cnf_opt.
-        intros.
-        destruct (is_cnf_tt f1).
-        - simpl ; auto.
-        - simpl. destruct (is_cnf_tt f2) ; simpl ; auto.
-          destruct (is_cnf_ff f2) eqn:EQ.
-          reflexivity.
-          apply ror_cnf_cnf.
-      Qed.
 
-      Lemma ratom_cnf : forall  f a,
-          fst (ratom f a) = f.
-      Proof.
-        unfold ratom.
-        intros.
-        destruct (is_cnf_ff f || is_cnf_tt f); auto.
-      Qed.
-
-
-
-      Lemma rxcnf_xcnf : forall {TX AF:Type} (f:TFormula TX AF) b,
-        fst (rxcnf  b f) = xcnf b f.
-      Proof.
-        induction f ; simpl ; auto.
-        - destruct b; simpl ; auto.
-        - destruct b; simpl ; auto.
-        - destruct b ; simpl ; auto.
-        - intros. rewrite ratom_cnf. reflexivity.
-        - intros.
-          specialize (IHf1 b).
-          specialize (IHf2 b).
-          destruct (rxcnf b f1).
-          destruct (rxcnf b f2).
-          simpl in *.
-          subst. destruct b ; auto.
-          rewrite <- ror_opt_cnf_cnf.
-          destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)).
-          reflexivity.
-        - intros.
-          specialize (IHf1 b).
-          specialize (IHf2 b).
-          rewrite <- IHf1.
-          rewrite <- IHf2.
-          destruct (rxcnf b f1).
-          destruct (rxcnf b f2).
-          simpl in *.
-          subst. destruct b ; auto.
-          rewrite <- ror_opt_cnf_cnf.
-          destruct (ror_cnf_opt (xcnf true f1) (xcnf true f2)).
-          reflexivity.
-        - intros.
-          specialize (IHf1 (negb b)).
-          specialize (IHf2 b).
-          rewrite <- IHf1.
-          rewrite <- IHf2.
-          destruct (rxcnf (negb b) f1).
-          destruct (rxcnf b f2).
-          simpl in *.
-          subst.
-          destruct b;auto.
-          generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
-          destruct (is_cnf_ff (xcnf (negb true) f1)).
-          + intros.
-            rewrite H by auto.
-            unfold or_cnf_opt.
-            simpl.
-            destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto.
-            apply is_cnf_tt_inv in EQ; auto.
-            destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1.
-            apply is_cnf_ff_inv in EQ1. congruence.
-            reflexivity.
-          +
-            rewrite <- ror_opt_cnf_cnf.
-            destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)).
-            intros.
-            reflexivity.
-      Qed.
+  Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl.
+  Proof.
+    induction a' ; simpl.
+    - intros.
+      destruct (deduce (fst a) (fst a)).
+      destruct (unsat t). congruence.
+      inversion H. reflexivity.
+      inversion H ;reflexivity.
+    - intros.
+      destruct (deduce (fst a0) (fst a)).
+      destruct (unsat t). congruence.
+      destruct (radd_term a0 a') eqn:RADD; try congruence.
+      inversion H. subst.
+      apply IHa' in RADD.
+      rewrite RADD.
+      reflexivity.
+      destruct (radd_term a0 a') eqn:RADD; try congruence.
+      inversion H. subst.
+      apply IHa' in RADD.
+      rewrite RADD.
+      reflexivity.
+  Qed.
 
+  Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl.
+  Proof.
+    induction a' ; simpl.
+    - intros.
+      destruct (deduce (fst a) (fst a)).
+      destruct (unsat t). congruence.
+      inversion H. reflexivity.
+      inversion H ;reflexivity.
+    - intros.
+      destruct (deduce (fst a0) (fst a)).
+      destruct (unsat t). congruence.
+      destruct (add_term a0 a') eqn:RADD; try congruence.
+      inversion H. subst.
+      apply IHa' in RADD.
+      rewrite RADD.
+      reflexivity.
+      destruct (add_term a0 a') eqn:RADD; try congruence.
+      inversion H. subst.
+      apply IHa' in RADD.
+      rewrite RADD.
+      reflexivity.
+  Qed.
 
-    Variable eval'  : Env -> Term' -> Prop.
+  Lemma xror_clause_clause : forall a f,
+      fst (xror_clause_cnf a f) = xor_clause_cnf a f.
+  Proof.
+    unfold xror_clause_cnf.
+    unfold xor_clause_cnf.
+    assert (ACC: fst (@nil clause,@nil Annot) = nil).
+    reflexivity.
+    intros.
+    set (F1:= (fun '(acc, tg) (e : clause) =>
+                 match ror_clause a e with
+                 | inl cl => (cl :: acc, tg)
+                 | inr l => (acc, tg +++ l)
+                 end)).
+    set (F2:= (fun (acc : list clause) (e : clause) =>
+                 match or_clause a e with
+                 | Some cl => cl :: acc
+                 | None => acc
+                 end)).
+    revert ACC.
+    generalize (@nil clause,@nil Annot).
+    generalize (@nil clause).
+    induction f ; simpl ; auto.
+    intros.
+    apply IHf.
+    unfold F1 , F2.
+    destruct p ; simpl in * ; subst.
+    clear.
+    revert a0.
+    induction a; simpl; auto.
+    intros.
+    destruct (radd_term a a1) eqn:RADD.
+    apply radd_term_term in RADD.
+    rewrite RADD.
+    auto.
+    destruct (add_term a a1) eqn:RADD'.
+    apply radd_term_term' in RADD'.
+    congruence.
+    reflexivity.
+  Qed.
 
-    Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
+  Lemma ror_clause_clause : forall a f,
+      fst (ror_clause_cnf a f) = or_clause_cnf a f.
+  Proof.
+    unfold ror_clause_cnf,or_clause_cnf.
+    destruct a ; auto.
+    apply xror_clause_clause.
+  Qed.
 
+  Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2.
+  Proof.
+    induction f1 ; simpl ; auto.
+    intros.
+    specialize (IHf1  f2).
+    destruct(ror_cnf f1 f2).
+    rewrite <- ror_clause_clause.
+    destruct(ror_clause_cnf a f2).
+    simpl.
+    rewrite <- IHf1.
+    reflexivity.
+  Qed.
 
-    Variable unsat_prop : forall t, unsat t  = true ->
-                                    forall env, eval' env t -> False.
+  Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2.
+  Proof.
+    unfold ror_cnf_opt, or_cnf_opt.
+    intros.
+    destruct (is_cnf_tt f1).
+    - simpl ; auto.
+    - simpl. destruct (is_cnf_tt f2) ; simpl ; auto.
+      destruct (is_cnf_ff f2) eqn:EQ.
+      reflexivity.
+      apply ror_cnf_cnf.
+  Qed.
 
+  Lemma ratom_cnf : forall  f a,
+      fst (ratom f a) = f.
+  Proof.
+    unfold ratom.
+    intros.
+    destruct (is_cnf_ff f || is_cnf_tt f); auto.
+  Qed.
 
+  Lemma rxcnf_and_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+                                (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+                                (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+      forall pol : bool, fst (rxcnf_and rxcnf pol f1 f2) = mk_and xcnf pol f1 f2.
+  Proof.
+    intros.
+    unfold mk_and, rxcnf_and.
+    specialize (IHf1 pol).
+    specialize (IHf2 pol).
+    destruct (rxcnf pol f1).
+    destruct (rxcnf pol f2).
+    simpl in *.
+    subst. destruct pol ; auto.
+    rewrite <- ror_opt_cnf_cnf.
+    destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)).
+    reflexivity.
+  Qed.
 
-    Variable deduce_prop : forall t t' u,
-        deduce t t' = Some u -> forall env,
-        eval' env t -> eval' env t' -> eval' env u.
+  Lemma rxcnf_or_xcnf :
+    forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+           (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+           (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+    forall pol : bool, fst (rxcnf_or rxcnf pol f1 f2) = mk_or xcnf pol f1 f2.
+  Proof.
+    intros.
+    unfold rxcnf_or, mk_or.
+    specialize (IHf1 pol).
+    specialize (IHf2 pol).
+    destruct (rxcnf pol f1).
+    destruct (rxcnf pol f2).
+    simpl in *.
+    subst. destruct pol ; auto.
+    rewrite <- ror_opt_cnf_cnf.
+    destruct (ror_cnf_opt (xcnf true f1) (xcnf true f2)).
+    reflexivity.
+  Qed.
 
+  Lemma rxcnf_impl_xcnf :
+    forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+           (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+           (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+    forall pol : bool, fst (rxcnf_impl rxcnf pol f1 f2) = mk_impl xcnf pol f1 f2.
+  Proof.
+    intros.
+    unfold rxcnf_impl, mk_impl, mk_or.
+    specialize (IHf1 (negb pol)).
+    specialize (IHf2 pol).
+    rewrite <- IHf1.
+    rewrite <- IHf2.
+    destruct (rxcnf (negb pol) f1).
+    destruct (rxcnf pol f2).
+    simpl in *.
+    subst.
+    destruct pol;auto.
+    generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
+    destruct (is_cnf_ff (xcnf (negb true) f1)).
+    + intros.
+      rewrite H by auto.
+      unfold or_cnf_opt.
+      simpl.
+      destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto.
+      apply is_cnf_tt_inv in EQ; auto.
+      destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1.
+      apply is_cnf_ff_inv in EQ1. congruence.
+      reflexivity.
+    +
+      rewrite <- ror_opt_cnf_cnf.
+      destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)).
+      intros.
+      reflexivity.
+  Qed.
 
 
-    Definition eval_tt (env : Env) (tt : Term' * Annot) := eval' env (fst tt).
 
 
-    Definition eval_clause (env : Env) (cl : clause) := ~ make_conj  (eval_tt env) cl.
+  Lemma rxcnf_iff_xcnf :
+    forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+           (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+           (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+    forall pol : bool, fst (rxcnf_iff rxcnf pol f1 f2) = mk_iff xcnf pol f1 f2.
+  Proof.
+    intros.
+    unfold rxcnf_iff.
+    unfold mk_iff.
+    rewrite <- (IHf1 (negb pol)).
+    rewrite <- (IHf1 pol).
+    rewrite <- (IHf2 false).
+    rewrite <- (IHf2 true).
+    destruct (rxcnf (negb pol) f1).
+    destruct (rxcnf false f2).
+    destruct (rxcnf pol f1).
+    destruct (rxcnf true f2).
+    destruct (ror_cnf_opt (and_cnf_opt c c0) (and_cnf_opt c1 c2)) eqn:EQ.
+    simpl.
+    change c3 with (fst (c3,l3)).
+    rewrite <- EQ. rewrite ror_opt_cnf_cnf.
+    reflexivity.
+  Qed.
 
-    Definition eval_cnf (env : Env) (f:cnf) := make_conj  (eval_clause  env) f.
+  Lemma rxcnf_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f:TFormula TX AF k) pol,
+      fst (rxcnf  pol f) = xcnf pol f.
+  Proof.
+    induction f ; simpl ; auto.
+    - destruct pol; simpl ; auto.
+    - destruct pol; simpl ; auto.
+    - destruct pol ; simpl ; auto.
+    - intros. rewrite ratom_cnf. reflexivity.
+    - apply rxcnf_and_xcnf; auto.
+    - apply rxcnf_or_xcnf; auto.
+    - apply rxcnf_impl_xcnf; auto.
+    - intros.
+      rewrite mk_iff_is_bool.
+      apply rxcnf_iff_xcnf; auto.
+    - intros.
+      rewrite mk_iff_is_bool.
+      apply rxcnf_iff_xcnf; auto.
+  Qed.
 
 
-    Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y.
-    Proof.
-      unfold eval_cnf.
-      intros.
-      rewrite make_conj_rapp.
-      rewrite make_conj_app ; auto.
-      tauto.
-    Qed.
+  Variable eval'  : Env -> Term' -> Prop.
 
+  Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
 
-    Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False.
-    Proof.
-      unfold cnf_ff, eval_cnf,eval_clause.
-      simpl. tauto.
-    Qed.
+  Variable unsat_prop : forall t, unsat t  = true ->
+                                  forall env, eval' env t -> False.
 
-    Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True.
-    Proof.
-      unfold cnf_tt, eval_cnf,eval_clause.
-      simpl. tauto.
-    Qed.
+  Variable deduce_prop : forall t t' u,
+      deduce t t' = Some u -> forall env,
+        eval' env t -> eval' env t' -> eval' env u.
 
+  Definition eval_tt (env : Env) (tt : Term' * Annot) := eval' env (fst tt).
 
-    Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y).
-    Proof.
-      unfold and_cnf_opt.
-      intros.
-      destruct (is_cnf_ff x) eqn:F1.
-      { apply is_cnf_ff_inv in F1.
-        simpl. subst.
-        unfold and_cnf.
-        rewrite eval_cnf_app.
-        rewrite eval_cnf_ff.
-        tauto.
-      }
-      simpl.
-      destruct (is_cnf_ff y) eqn:F2.
-      { apply is_cnf_ff_inv in F2.
-        simpl. subst.
-        unfold and_cnf.
-        rewrite eval_cnf_app.
-        rewrite eval_cnf_ff.
-        tauto.
-      }
-      tauto.
-    Qed.
+  Definition eval_clause (env : Env) (cl : clause) := ~ make_conj  (eval_tt env) cl.
 
+  Definition eval_cnf (env : Env) (f:cnf) := make_conj  (eval_clause  env) f.
 
+  Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y.
+  Proof.
+    unfold eval_cnf.
+    intros.
+    rewrite make_conj_rapp.
+    rewrite make_conj_app ; auto.
+    tauto.
+  Qed.
 
-    Definition eval_opt_clause (env : Env) (cl: option clause) :=
-      match cl with
-      | None => True
-      | Some cl => eval_clause env cl
-      end.
+  Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False.
+  Proof.
+    unfold cnf_ff, eval_cnf,eval_clause.
+    simpl. tauto.
+  Qed.
 
+  Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True.
+  Proof.
+    unfold cnf_tt, eval_cnf,eval_clause.
+    simpl. tauto.
+  Qed.
 
-  Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl).
+  Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y).
   Proof.
-    induction cl.
-    - (* BC *)
-    simpl.
-    case_eq (deduce (fst t) (fst t)) ; try tauto.
+    unfold and_cnf_opt.
     intros.
-    generalize (@deduce_prop _ _ _ H env).
-    case_eq (unsat t0) ; try tauto.
-    { intros.
-      generalize (@unsat_prop _ H0 env).
-      unfold eval_clause.
-      rewrite make_conj_cons.
-      simpl; intros.
+    destruct (is_cnf_ff x) eqn:F1.
+    { apply is_cnf_ff_inv in F1.
+      simpl. subst.
+      unfold and_cnf.
+      rewrite eval_cnf_app.
+      rewrite eval_cnf_ff.
       tauto.
     }
-    - (* IC *)
     simpl.
-    case_eq (deduce (fst t) (fst a));
-    intros.
-    generalize (@deduce_prop _ _ _ H env).
-    case_eq (unsat t0); intros.
-    {
-      generalize (@unsat_prop _ H0 env).
-      simpl.
-      unfold eval_clause.
-      repeat rewrite make_conj_cons.
-      tauto.
-    }
-    destruct (add_term t cl) ; simpl in * ; try tauto.
-    {
-      intros.
-      unfold eval_clause in *.
-      repeat rewrite make_conj_cons in *.
+    destruct (is_cnf_ff y) eqn:F2.
+    { apply is_cnf_ff_inv in F2.
+      simpl. subst.
+      unfold and_cnf.
+      rewrite eval_cnf_app.
+      rewrite eval_cnf_ff.
       tauto.
     }
+    destruct (is_cnf_tt y) eqn:F3.
     {
-      unfold eval_clause in *.
-      repeat rewrite make_conj_cons in *.
+      apply is_cnf_tt_inv in F3.
+      subst.
+      unfold and_cnf.
+      rewrite eval_cnf_app.
+      rewrite eval_cnf_tt.
       tauto.
     }
-    destruct (add_term t cl) ; simpl in *;
-      unfold eval_clause in * ;
-      repeat rewrite make_conj_cons in *; tauto.
+    tauto.
+  Qed.
+
+  Definition eval_opt_clause (env : Env) (cl: option clause) :=
+    match cl with
+    | None => True
+    | Some cl => eval_clause env cl
+    end.
+
+  Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl).
+  Proof.
+    induction cl.
+    - (* BC *)
+      simpl.
+      case_eq (deduce (fst t) (fst t)) ; try tauto.
+      intros.
+      generalize (@deduce_prop _ _ _ H env).
+      case_eq (unsat t0) ; try tauto.
+      { intros.
+        generalize (@unsat_prop _ H0 env).
+        unfold eval_clause.
+        rewrite make_conj_cons.
+        simpl; intros.
+        tauto.
+      }
+    - (* IC *)
+      simpl.
+      case_eq (deduce (fst t) (fst a));
+        intros.
+      generalize (@deduce_prop _ _ _ H env).
+      case_eq (unsat t0); intros.
+      {
+        generalize (@unsat_prop _ H0 env).
+        simpl.
+        unfold eval_clause.
+        repeat rewrite make_conj_cons.
+        tauto.
+      }
+      destruct (add_term t cl) ; simpl in * ; try tauto.
+      {
+        intros.
+        unfold eval_clause in *.
+        repeat rewrite make_conj_cons in *.
+        tauto.
+      }
+      {
+        unfold eval_clause in *.
+        repeat rewrite make_conj_cons in *.
+        tauto.
+      }
+      destruct (add_term t cl) ; simpl in *;
+        unfold eval_clause in * ;
+        repeat rewrite make_conj_cons in *; tauto.
   Qed.
 
 
@@ -1096,10 +1565,10 @@ Section S.
       assert (eval_tt env a \/ ~ eval_tt env a) by (apply no_middle_eval').
       destruct (add_term a cl'); simpl in *.
       +
-      rewrite IHcl.
-      unfold eval_clause in *.
-      rewrite !make_conj_cons in *.
-      tauto.
+        rewrite IHcl.
+        unfold eval_clause in *.
+        rewrite !make_conj_cons in *.
+        tauto.
       + unfold eval_clause in *.
         repeat rewrite make_conj_cons in *.
         tauto.
@@ -1131,8 +1600,8 @@ Section S.
         generalize (or_clause_correct t a env).
         destruct (or_clause t a).
         +
-        rewrite make_conj_cons.
-        simpl. tauto.
+          rewrite make_conj_cons.
+          simpl. tauto.
         + simpl. tauto.
     }
     destruct t ; auto.
@@ -1211,113 +1680,108 @@ Section S.
     }
   Qed.
 
+  Variable eval  : Env -> forall (k: kind), Term -> rtyp k.
 
-  Variable eval  : Env -> Term -> Prop.
+  Variable normalise_correct : forall env b t tg, eval_cnf  env (normalise t tg) ->  hold b (eval env b t).
 
-  Variable normalise_correct : forall env t tg, eval_cnf  env (normalise t tg) -> eval env t.
+  Variable negate_correct : forall env b t tg, eval_cnf env (negate t tg) -> hold b (eNOT b (eval env b t)).
 
-  Variable negate_correct : forall env t tg, eval_cnf env (negate t tg) -> ~ eval env t.
+  Definition e_rtyp (k: kind) (x : rtyp k) : rtyp k := x.
 
-  Lemma xcnf_correct : forall (f : @GFormula Term Prop Annot unit)  pol env, eval_cnf env (xcnf pol f) -> eval_f (fun x => x) (eval env) (if pol then f else N f).
+  Lemma hold_eTT : forall k, hold k (eTT k).
   Proof.
-    induction f.
-    - (* TT *)
-    unfold eval_cnf.
-    simpl.
-    destruct pol ; simpl ; auto.
-    - (* FF *)
-    unfold eval_cnf.
-    destruct pol; simpl ; auto.
-    unfold eval_clause ; simpl.
-    tauto.
-    - (* P *)
-    simpl.
-    destruct pol ; intros ;simpl.
-    unfold eval_cnf in H.
-    (* Here I have to drop the proposition *)
-    simpl in H.
-    unfold eval_clause in H ; simpl in H.
-    tauto.
-    (* Here, I could store P in the clause *)
-    unfold eval_cnf in H;simpl in H.
-    unfold eval_clause in H ; simpl in H.
-    tauto.
-    - (* A *)
-    simpl.
-    destruct pol ; simpl.
-    intros.
-    eapply normalise_correct  ; eauto.
-    (* A 2 *)
-    intros.
-    eapply  negate_correct ; eauto.
-    - (* Cj *)
-    destruct pol ; simpl.
-    + (* pol = true *)
-    intros.
-    rewrite eval_cnf_and_opt in H.
-    unfold and_cnf in H.
-    rewrite eval_cnf_app  in H.
-    destruct H.
-    split.
-    apply (IHf1 _ _ H).
-    apply (IHf2 _ _ H0).
-    +  (* pol = false *)
-    intros.
-    rewrite or_cnf_opt_correct in H.
-    rewrite or_cnf_correct in H.
-    destruct H as [H | H].
-    generalize (IHf1 false  env H).
-    simpl.
-    tauto.
-    generalize (IHf2 false  env H).
-    simpl.
-    tauto.
-    - (* D *)
-    simpl.
-    destruct pol.
-    + (* pol = true *)
-    intros.
-    rewrite or_cnf_opt_correct in H.
-    rewrite or_cnf_correct in H.
-    destruct H as [H | H].
-    generalize (IHf1 _  env H).
-    simpl.
-    tauto.
-    generalize (IHf2 _  env H).
-    simpl.
-    tauto.
-    + (* pol = true *)
-    intros.
-    rewrite eval_cnf_and_opt in H.
-    unfold and_cnf.
-    rewrite eval_cnf_app in H.
-    destruct H as [H0 H1].
-    simpl.
-    generalize (IHf1 _ _ H0).
-    generalize (IHf2 _ _ H1).
-    simpl.
-    tauto.
-    - (**)
-    simpl.
-    destruct pol ; simpl.
-    intros.
-    apply (IHf false) ; auto.
-    intros.
-    generalize (IHf _ _ H).
-    tauto.
-    - (* I *)
-    simpl; intros.
+    destruct k ; simpl; auto.
+  Qed.
+
+  Hint Resolve hold_eTT : tauto.
+
+  Lemma hold_eFF : forall k,
+      hold k (eNOT k (eFF k)).
+  Proof.
+    destruct k ; simpl;auto.
+  Qed.
+
+  Hint Resolve hold_eFF : tauto.
+
+  Lemma hold_eAND : forall k r1 r2,
+      hold k (eAND k r1 r2) <-> (hold k r1 /\ hold k r2).
+  Proof.
+    destruct k ; simpl.
+    - intros. apply iff_refl.
+    - apply andb_true_iff.
+  Qed.
+
+  Lemma hold_eOR : forall k r1 r2,
+      hold k (eOR k r1 r2) <-> (hold k r1 \/ hold k r2).
+  Proof.
+    destruct k ; simpl.
+    - intros. apply iff_refl.
+    - apply orb_true_iff.
+  Qed.
+
+  Lemma hold_eNOT : forall k e,
+      hold k (eNOT k e) <-> not (hold k e).
+  Proof.
+    destruct k ; simpl.
+    - intros. apply iff_refl.
+    - intros. unfold is_true.
+      rewrite negb_true_iff.
+      destruct e ; intuition congruence.
+  Qed.
+
+  Lemma hold_eIMPL : forall k e1 e2,
+      hold k (eIMPL k e1 e2) <-> (hold k e1 -> hold k e2).
+  Proof.
+    destruct k ; simpl.
+    - intros. apply iff_refl.
+    - intros.
+      unfold is_true.
+      destruct e1,e2 ; simpl ; intuition congruence.
+  Qed.
+
+  Lemma hold_eIFF : forall k e1 e2,
+      hold k (eIFF k e1 e2) <-> (hold k e1 <-> hold k e2).
+  Proof.
+    destruct k ; simpl.
+    - intros. apply iff_refl.
+    - intros.
+      unfold is_true.
+      rewrite eqb_true_iff.
+      destruct e1,e2 ; simpl ; intuition congruence.
+  Qed.
+
+
+
+  Lemma xcnf_impl :
+    forall
+      (k: kind)
+      (f1 : GFormula k)
+      (o : option unit)
+      (f2 : GFormula k)
+      (IHf1 : forall (pol : bool) (env : Env),
+          eval_cnf env (xcnf pol f1) ->
+          hold k (eval_f e_rtyp (eval env) (if pol then f1 else NOT f1)))
+      (IHf2 : forall (pol : bool) (env : Env),
+          eval_cnf env (xcnf pol f2) ->
+          hold k (eval_f e_rtyp (eval env) (if pol then f2 else NOT f2))),
+    forall (pol : bool) (env : Env),
+      eval_cnf env (xcnf pol (IMPL f1 o f2)) ->
+      hold k (eval_f e_rtyp (eval env) (if pol then IMPL f1 o f2 else NOT (IMPL f1 o f2))).
+  Proof.
+    simpl; intros. unfold mk_impl in H.
     destruct pol.
     + simpl.
-    intro.
-    rewrite or_cnf_opt_correct in H.
-    rewrite or_cnf_correct in H.
-    destruct H as [H | H].
-    generalize (IHf1 _ _ H).
-    simpl in *.
-    tauto.
-    generalize (IHf2 _ _ H).
-    auto.
+      rewrite hold_eIMPL.
+      intro.
+      rewrite or_cnf_opt_correct in H.
+      rewrite or_cnf_correct in H.
+      destruct H as [H | H].
+      generalize (IHf1 _ _ H).
+      simpl in *.
+      rewrite hold_eNOT.
+      tauto.
+      generalize (IHf2 _ _ H).
+      auto.
     + (* pol = false *)
       rewrite eval_cnf_and_opt in H.
       unfold and_cnf in H.
@@ -1327,9 +1791,190 @@ Section S.
       generalize (IHf1 _ _ H0).
       generalize (IHf2 _ _ H1).
       simpl.
+      rewrite ! hold_eNOT.
+      rewrite ! hold_eIMPL.
       tauto.
   Qed.
 
+  Lemma hold_eIFF_IMPL : forall k e1 e2,
+      hold k (eIFF k e1 e2) <-> (hold k (eAND k (eIMPL k e1 e2) (eIMPL k e2 e1))).
+  Proof.
+    intros.
+    rewrite hold_eIFF.
+    rewrite hold_eAND.
+    rewrite! hold_eIMPL.
+    tauto.
+  Qed.
+
+  Lemma hold_eEQ : forall e1 e2,
+      hold isBool (eIFF isBool e1 e2) <-> e1 = e2.
+  Proof.
+    simpl.
+    destruct e1,e2 ; simpl ; intuition congruence.
+  Qed.
+
+
+  Lemma xcnf_iff : forall
+      (k : kind)
+      (f1 f2 : @GFormula Term rtyp Annot unit k)
+      (IHf1 : forall (pol : bool) (env : Env),
+          eval_cnf env (xcnf pol f1) ->
+          hold k (eval_f e_rtyp (eval env) (if pol then f1 else NOT f1)))
+      (IHf2 : forall (pol : bool) (env : Env),
+          eval_cnf env (xcnf pol f2) ->
+          hold k (eval_f e_rtyp (eval env) (if pol then f2 else NOT f2))),
+      forall (pol : bool) (env : Env),
+        eval_cnf env (xcnf pol (IFF f1 f2)) ->
+        hold k (eval_f e_rtyp (eval env) (if pol then IFF f1 f2 else NOT (IFF f1 f2))).
+  Proof.
+    simpl.
+    intros.
+    rewrite mk_iff_is_bool in H.
+    unfold mk_iff in H.
+    destruct pol;
+      rewrite or_cnf_opt_correct in H;
+      rewrite or_cnf_correct in H;
+      rewrite! eval_cnf_and_opt in H;
+      unfold and_cnf in H;
+      rewrite! eval_cnf_app in H;
+      generalize (IHf1 false env);
+      generalize (IHf1 true env);
+      generalize (IHf2 false env);
+      generalize (IHf2 true env);
+      simpl.
+    -
+      rewrite hold_eIFF_IMPL.
+      rewrite hold_eAND.
+      rewrite! hold_eIMPL.
+      rewrite! hold_eNOT.
+      tauto.
+    -  rewrite! hold_eNOT.
+       rewrite hold_eIFF_IMPL.
+       rewrite hold_eAND.
+       rewrite! hold_eIMPL.
+       tauto.
+  Qed.
+
+  Lemma xcnf_correct : forall (k: kind) (f : @GFormula Term rtyp Annot unit k)  pol env,
+      eval_cnf env (xcnf pol f) -> hold k (eval_f e_rtyp (eval env) (if pol then f else NOT f)).
+  Proof.
+    induction f.
+    - (* TT *)
+      unfold eval_cnf.
+      simpl.
+      destruct pol ; intros; simpl; auto with tauto.
+      rewrite eval_cnf_ff in H. tauto.
+    - (* FF *)
+      destruct pol ; simpl in *; intros; auto with tauto.
+      + rewrite eval_cnf_ff in H. tauto.
+    - (* P *)
+      simpl.
+      destruct pol ; intros ;simpl.
+      + rewrite eval_cnf_ff in H. tauto.
+      + rewrite eval_cnf_ff in H. tauto.
+    - (* A *)
+      simpl.
+      destruct pol ; simpl.
+      intros.
+      eapply normalise_correct  ; eauto.
+      (* A 2 *)
+      intros.
+      eapply  negate_correct ; eauto.
+    - (* AND *)
+      destruct pol ; simpl.
+      + (* pol = true *)
+        intros.
+        rewrite eval_cnf_and_opt in H.
+        unfold and_cnf in H.
+        rewrite eval_cnf_app  in H.
+        destruct H.
+        apply hold_eAND; split.
+        apply (IHf1 _ _ H).
+        apply (IHf2 _ _ H0).
+      +  (* pol = false *)
+        intros.
+        apply hold_eNOT.
+        rewrite hold_eAND.
+        rewrite or_cnf_opt_correct in H.
+        rewrite or_cnf_correct in H.
+        destruct H as [H | H].
+        generalize (IHf1 false  env H).
+        simpl.
+        rewrite hold_eNOT.
+        tauto.
+        generalize (IHf2 false  env H).
+        simpl.
+        rewrite hold_eNOT.
+        tauto.
+    - (* OR *)
+      simpl.
+      destruct pol.
+      + (* pol = true *)
+        intros. unfold mk_or in H.
+        rewrite or_cnf_opt_correct in H.
+        rewrite or_cnf_correct in H.
+        destruct H as [H | H].
+        generalize (IHf1 _  env H).
+        simpl.
+        rewrite hold_eOR.
+        tauto.
+        generalize (IHf2 _  env H).
+        simpl.
+        rewrite hold_eOR.
+        tauto.
+      + (* pol = true *)
+        intros. unfold mk_or in H.
+        rewrite eval_cnf_and_opt in H.
+        unfold and_cnf.
+        rewrite eval_cnf_app in H.
+        destruct H as [H0 H1].
+        simpl.
+        generalize (IHf1 _ _ H0).
+        generalize (IHf2 _ _ H1).
+        simpl.
+        rewrite ! hold_eNOT.
+        rewrite ! hold_eOR.
+        tauto.
+    - (**)
+      simpl.
+      destruct pol ; simpl.
+      intros.
+      apply (IHf false) ; auto.
+      intros.
+      generalize (IHf _ _ H).
+      rewrite ! hold_eNOT.
+      tauto.
+    - (* IMPL *)
+      apply xcnf_impl; auto.
+    - apply xcnf_iff ; auto.
+    - simpl.
+      destruct (is_bool f2) eqn:EQ.
+      + apply is_bool_inv in EQ.
+        destruct b; subst; intros;
+          apply IHf1 in H;
+          destruct pol ; simpl in * ; auto.
+        * unfold is_true in H.
+          rewrite negb_true_iff in H.
+          congruence.
+        *
+          unfold is_true in H.
+          rewrite negb_true_iff in H.
+          congruence.
+        * unfold is_true in H.
+          congruence.
+      + intros.
+        rewrite <- mk_iff_is_bool in H.
+        apply xcnf_iff in H; auto.
+        simpl in H.
+        destruct pol ; simpl in *.
+        rewrite <- hold_eEQ.
+        simpl; auto.
+        rewrite <- hold_eEQ.
+        simpl; auto.
+        unfold is_true in *.
+        rewrite negb_true_iff in H.
+        congruence.
+  Qed.
 
   Variable Witness : Type.
   Variable checker : list (Term'*Annot) -> Witness -> bool.
@@ -1370,28 +2015,26 @@ Section S.
     tauto.
   Qed.
 
-
-  Definition tauto_checker (f:@GFormula Term Prop Annot unit) (w:list Witness) : bool :=
+  Definition tauto_checker (f:@GFormula Term rtyp Annot unit isProp) (w:list Witness) : bool :=
     cnf_checker (xcnf true f) w.
 
-  Lemma tauto_checker_sound : forall t  w, tauto_checker t w = true -> forall env, eval_f (fun x => x) (eval env)  t.
+  Lemma tauto_checker_sound : forall t  w, tauto_checker t w = true -> forall env, eval_f e_rtyp (eval env)  t.
   Proof.
     unfold tauto_checker.
     intros.
-    change (eval_f (fun x => x) (eval env) t) with (eval_f (fun x => x) (eval env) (if true then t else TT)).
+    change (eval_f e_rtyp (eval env) t) with (eval_f e_rtyp (eval env) (if true then t else TT isProp)).
     apply (xcnf_correct t true).
     eapply cnf_checker_sound ; eauto.
   Qed.
 
-  Definition eval_bf {A : Type} (ea : A -> Prop) (f: BFormula A) := eval_f (fun x => x) ea f.
-
+  Definition eval_bf {A : Type} (ea : forall (k: kind), A -> rtyp k) (k: kind) (f: BFormula A k) := eval_f e_rtyp ea f.
 
-  Lemma eval_bf_map : forall T U (fct: T-> U) env f ,
-    eval_bf env  (map_bformula fct f)  = eval_bf (fun x => env (fct x)) f.
-Proof.
-  induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto.
-  rewrite <- IHf.  auto.
-Qed.
+  Lemma eval_bf_map : forall T U (fct: T-> U) env (k: kind) (f:BFormula T k) ,
+      eval_bf env  (map_bformula fct f)  = eval_bf (fun b x => env b (fct x)) f.
+  Proof.
+    induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto.
+    rewrite <- IHf.  auto.
+  Qed.
 
 
 End S.
diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v
index bff9671fee..935757f30a 100644
--- a/theories/micromega/ZMicromega.v
+++ b/theories/micromega/ZMicromega.v
@@ -176,7 +176,7 @@ Proof.
   rewrite ZNpower. congruence.
 Qed.
 
-Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop :=
+Definition Zeval_pop2 (o : Op2) : Z -> Z -> Prop :=
 match o with
 | OpEq =>  @eq Z
 | OpNEq => fun x y  => ~ x = y
@@ -187,14 +187,62 @@ match o with
 end.
 
 
-Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=
+Definition Zeval_bop2 (o : Op2) : Z -> Z -> bool :=
+match o with
+| OpEq =>  Z.eqb
+| OpNEq => fun x y => negb (Z.eqb x y)
+| OpLe => Z.leb
+| OpGe => Z.geb
+| OpLt => Z.ltb
+| OpGt => Z.gtb
+end.
+
+Lemma pop2_bop2 :
+  forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2.
+Proof.
+  unfold is_true.
+  destruct op ; simpl; intros.
+  - apply Z.eqb_eq.
+  - rewrite <- Z.eqb_eq.
+    rewrite negb_true_iff.
+    destruct (q1 =? q2) ; intuition congruence.
+  - apply Z.leb_le.
+  - rewrite Z.geb_le. rewrite Z.ge_le_iff. tauto.
+  - apply Z.ltb_lt.
+  - rewrite <- Zgt_is_gt_bool; tauto.
+Qed.
+
+Definition Zeval_op2 (k: Tauto.kind) :  Op2 ->  Z -> Z -> Tauto.rtyp k:=
+  if k as k0 return (Op2 -> Z -> Z -> Tauto.rtyp k0)
+  then Zeval_pop2 else Zeval_bop2.
+
+
+Lemma Zeval_op2_hold : forall k op q1 q2,
+    Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2.
+Proof.
+  destruct k.
+  simpl ; tauto.
+  simpl. apply pop2_bop2.
+Qed.
+
+
+Definition Zeval_formula (env : PolEnv Z) (k: Tauto.kind) (f : Formula Z):=
   let (lhs, op, rhs) := f in
-    (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs).
+    (Zeval_op2 k op) (Zeval_expr env lhs) (Zeval_expr env rhs).
 
 Definition Zeval_formula' :=
   eval_formula  Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul).
 
-Lemma Zeval_formula_compat' : forall env f,  Zeval_formula env  f <-> Zeval_formula' env f.
+Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f.
+Proof.
+  destruct k ; simpl.
+  - tauto.
+  - destruct f ; simpl.
+    rewrite <- Zeval_op2_hold with (k:=Tauto.isBool).
+    simpl. tauto.
+Qed.
+
+Lemma Zeval_formula_compat' : forall env f,  Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f.
 Proof.
   intros.
   unfold Zeval_formula.
@@ -312,7 +360,7 @@ Definition xnnormalise (t : Formula Z) : NFormula Z :=
 
 Lemma xnnormalise_correct :
   forall env f,
-    eval_nformula env (xnnormalise f) <-> Zeval_formula env  f.
+    eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f.
 Proof.
   intros.
   rewrite Zeval_formula_compat'.
@@ -393,6 +441,7 @@ Proof.
 Qed.
 
 
+
 Require Import Coq.micromega.Tauto BinNums.
 
 Definition cnf_of_list {T: Type} (tg : T) (l : list (NFormula Z)) :=
@@ -435,7 +484,7 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
   if Zunsat f then cnf_ff _ _
   else cnf_of_list tg (xnormalise f).
 
-Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env t.
+Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t.
 Proof.
   intros.
   rewrite <- xnnormalise_correct.
@@ -449,6 +498,7 @@ Proof.
     apply xnormalise_correct.
 Qed.
 
+
 Definition xnegate (f:NFormula Z) : list (NFormula Z)  :=
   let (e,o) := f in
     match o with
@@ -478,7 +528,7 @@ Proof.
   - tauto.
 Qed.
 
-Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env  t.
+Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t.
 Proof.
   intros.
   rewrite <- xnnormalise_correct.
@@ -492,10 +542,10 @@ Proof.
     apply xnegate_correct.
 Qed.
 
-Definition cnfZ (Annot: Type) (TX : Type)  (AF : Type)  (f : TFormula (Formula Z) Annot TX AF) :=
+Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type)  (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) :=
   rxcnf Zunsat Zdeduce normalise negate true f.
 
-Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool :=
+Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z) Tauto.isProp) : bool :=
   @tauto_checker (Formula Z)  (NFormula Z) unit Zunsat Zdeduce normalise negate  ZWitness (fun cl => ZWeakChecker (List.map fst cl)) f w.
 
 (* To get a complete checker, the proof format has to be enriched *)
@@ -1672,9 +1722,7 @@ Proof.
     apply Nat.lt_succ_diag_r.
 Qed.
 
-
-
-Definition ZTautoChecker  (f : BFormula (Formula Z)) (w: list ZArithProof): bool :=
+Definition ZTautoChecker  (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool :=
   @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate  ZArithProof (fun cl => ZChecker (List.map fst cl)) f w.
 
 Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf  (Zeval_formula env)  f.
@@ -1692,10 +1740,12 @@ Proof.
   -
     intros.
     rewrite normalise_correct  in H.
-    auto.
+    rewrite Zeval_formula_compat; auto.
   -
     intros.
     rewrite negate_correct in H ; auto.
+    rewrite Tauto.hold_eNOT.
+    rewrite Zeval_formula_compat; auto.
   - intros t w0.
     unfold eval_tt.
     intros.
@@ -1703,8 +1753,6 @@ Proof.
     eapply ZChecker_sound; eauto.
     tauto.
 Qed.
-
-
 Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof)  : list nat :=
   match pt with
     | DoneProof => acc
diff --git a/theories/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v
index c693824f89..d41ac6cf2f 100644
--- a/theories/micromega/ZifyBool.v
+++ b/theories/micromega/ZifyBool.v
@@ -9,177 +9,88 @@
 (************************************************************************)
 Require Import Bool ZArith.
 Require Import Zify ZifyClasses.
+Require Import ZifyInst.
 Local Open Scope Z_scope.
-(* Instances of [ZifyClasses] for dealing with boolean operators.
-   Various encodings of boolean are possible.  One objective is to
-   have an encoding that is terse but also lia friendly.
- *)
+(* Instances of [ZifyClasses] for dealing with boolean operators. *)
 
-(** [Z_of_bool] is the injection function for boolean *)
-Definition Z_of_bool (b : bool) : Z := if b then 1 else 0.
-
-(** [bool_of_Z] is a compatible reverse operation *)
-Definition bool_of_Z (z : Z) : bool := negb (Z.eqb z 0).
-
-Lemma Z_of_bool_bound : forall x,   0 <= Z_of_bool x <= 1.
-Proof.
-  destruct x ; simpl; compute; intuition congruence.
-Qed.
-
-Instance Inj_bool_Z : InjTyp bool Z :=
-  { inj := Z_of_bool ; pred :=(fun x => 0 <= x <= 1) ; cstr := Z_of_bool_bound}.
-Add InjTyp Inj_bool_Z.
+Instance Inj_bool_bool : InjTyp bool bool :=
+  { inj := (fun x => x) ; pred := (fun x => True) ; cstr := (fun _ => I)}.
+Add InjTyp Inj_bool_bool.
 
 (** Boolean operators *)
 
 Instance Op_andb : BinOp andb :=
-  { TBOp := Z.min ;
-    TBOpInj := ltac: (destruct n,m; reflexivity)}.
+  { TBOp := andb ;
+    TBOpInj := ltac: (reflexivity)}.
 Add BinOp Op_andb.
 
 Instance Op_orb : BinOp orb :=
-  { TBOp := Z.max ;
-    TBOpInj := ltac:(destruct n,m; reflexivity)}.
+  { TBOp := orb ;
+    TBOpInj := ltac:(reflexivity)}.
 Add BinOp Op_orb.
 
 Instance Op_implb : BinOp implb :=
-  { TBOp := fun x y => Z.max (1 - x) y;
-    TBOpInj := ltac:(destruct n,m; reflexivity) }.
+  { TBOp := implb;
+    TBOpInj := ltac:(reflexivity) }.
 Add BinOp Op_implb.
 
+Definition xorb_eq : forall b1 b2,
+    xorb b1 b2 = andb (orb b1 b2) (negb (eqb b1 b2)).
+Proof.
+  destruct b1,b2 ; reflexivity.
+Qed.
+
 Instance Op_xorb : BinOp xorb :=
-  { TBOp := fun x y => Z.max (x - y) (y - x);
-    TBOpInj := ltac:(destruct n,m; reflexivity) }.
+  { TBOp := fun x y => andb (orb x y) (negb (eqb x y));
+    TBOpInj := xorb_eq }.
 Add BinOp Op_xorb.
 
 Instance Op_negb : UnOp negb :=
-  { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}.
+  { TUOp := negb ; TUOpInj := ltac:(reflexivity)}.
 Add UnOp Op_negb.
 
 Instance Op_eq_bool : BinRel (@eq bool) :=
-  {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }.
+  {TR := @eq bool ; TRInj := ltac:(reflexivity) }.
 Add BinRel Op_eq_bool.
 
 Instance Op_true : CstOp true :=
-  { TCst := 1 ; TCstInj := eq_refl }.
+  { TCst := true ; TCstInj := eq_refl }.
 Add CstOp Op_true.
 
 Instance Op_false : CstOp false :=
-  { TCst := 0 ; TCstInj := eq_refl }.
+  { TCst := false ; TCstInj := eq_refl }.
 Add CstOp Op_false.
 
-(** Comparisons are encoded using the predicates [isZero] and [isLeZero].*)
-
-Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0).
-
-Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0).
-
-Instance Op_isZero : UnOp isZero :=
-  { TUOp := isZero; TUOpInj := ltac: (reflexivity) }.
-Add UnOp Op_isZero.
-
-Instance Op_isLeZero : UnOp isLeZero :=
-  { TUOp := isLeZero; TUOpInj := ltac: (reflexivity) }.
-Add UnOp Op_isLeZero.
-
-(* Some intermediate lemma *)
-
-Lemma Z_eqb_isZero : forall n m,
-    Z_of_bool (n =? m) = isZero (n - m).
-Proof.
-  intros ; unfold isZero.
-  destruct ( n =? m) eqn:EQ.
-  - simpl. rewrite Z.eqb_eq in EQ.
-    rewrite EQ. rewrite Z.sub_diag.
-    reflexivity.
-  -
-    destruct (n - m =? 0) eqn:EQ'.
-    rewrite Z.eqb_neq in EQ.
-    rewrite Z.eqb_eq in EQ'.
-    apply Zminus_eq in EQ'.
-    congruence.
-    reflexivity.
-Qed.
-
-Lemma Z_leb_sub : forall x y, x <=? y  = ((x - y) <=? 0).
-Proof.
-  intros.
-  destruct (x <=?y) eqn:B1 ;
-    destruct (x - y <=?0) eqn:B2 ; auto.
-  - rewrite Z.leb_le in B1.
-    rewrite Z.leb_nle in B2.
-    rewrite Z.le_sub_0 in B2. tauto.
-  - rewrite Z.leb_nle in B1.
-    rewrite Z.leb_le in B2.
-    rewrite Z.le_sub_0 in B2. tauto.
-Qed.
-
-Lemma Z_ltb_leb : forall x y, x <? y  = (x +1 <=? y).
-Proof.
-  intros.
-  destruct (x <?y) eqn:B1 ;
-    destruct (x + 1 <=?y) eqn:B2 ; auto.
-  - rewrite Z.ltb_lt in B1.
-    rewrite Z.leb_nle in B2.
-    apply Zorder.Zlt_le_succ in B1.
-    unfold Z.succ in B1.
-    tauto.
-  - rewrite Z.ltb_nlt in B1.
-    rewrite Z.leb_le in B2.
-    apply Zorder.Zle_lt_succ in B2.
-    unfold Z.succ in B2.
-    apply Zorder.Zplus_lt_reg_r in B2.
-    tauto.
-Qed.
-
-
 (** Comparison over Z *)
 
 Instance Op_Zeqb : BinOp Z.eqb :=
-  { TBOp := fun x y => isZero (Z.sub x y) ; TBOpInj := Z_eqb_isZero}.
+  { TBOp := Z.eqb ; TBOpInj := ltac:(reflexivity)}.
 
 Instance Op_Zleb : BinOp Z.leb :=
-  { TBOp := fun x y => isLeZero (x-y) ;
-    TBOpInj :=
-      ltac: (intros;unfold isLeZero;
-               rewrite Z_leb_sub;
-               auto) }.
+  { TBOp := Z.leb;
+    TBOpInj :=  ltac: (reflexivity);
+  }.
 Add BinOp Op_Zleb.
 
 Instance Op_Zgeb : BinOp Z.geb :=
-  { TBOp := fun x y => isLeZero (y-x) ;
-    TBOpInj := ltac:(
-                 intros;
-                   unfold isLeZero;
-                   rewrite Z.geb_leb;
-                   rewrite Z_leb_sub;
-                   auto) }.
+  { TBOp := Z.geb;
+    TBOpInj := ltac:(reflexivity)
+  }.
 Add BinOp Op_Zgeb.
 
 Instance Op_Zltb : BinOp Z.ltb :=
-  { TBOp := fun x y => isLeZero (x+1-y) ;
-    TBOpInj := ltac:(
-                 intros;
-                   unfold isLeZero;
-                   rewrite Z_ltb_leb;
-                   rewrite <- Z_leb_sub;
-                   reflexivity) }.
+  { TBOp := Z.ltb ;
+    TBOpInj := ltac:(reflexivity)
+  }.
 
 Instance Op_Zgtb : BinOp Z.gtb :=
-  { TBOp := fun x y => isLeZero (y-x+1) ;
-    TBOpInj := ltac:(
-                 intros;
-                   unfold isLeZero;
-                   rewrite Z.gtb_ltb;
-                   rewrite Z_ltb_leb;
-                   rewrite Z_leb_sub;
-                   rewrite Z.add_sub_swap;
-                   reflexivity) }.
+  { TBOp := Z.gtb;
+    TBOpInj := ltac:(reflexivity)
+  }.
 Add BinOp Op_Zgtb.
 
 (** Comparison over nat *)
 
-
 Lemma Z_of_nat_eqb_iff : forall n m,
     (n =? m)%nat = (Z.of_nat n =? Z.of_nat m).
 Proof.
@@ -211,68 +122,18 @@ Proof.
 Qed.
 
 Instance Op_nat_eqb : BinOp Nat.eqb :=
-   { TBOp := fun x y => isZero (Z.sub x y) ;
-     TBOpInj := ltac:(
-                  intros; simpl;
-                    rewrite  <- Z_eqb_isZero;
-                  f_equal; apply Z_of_nat_eqb_iff) }.
+   { TBOp := Z.eqb;
+     TBOpInj := Z_of_nat_eqb_iff }.
 Add BinOp Op_nat_eqb.
 
 Instance Op_nat_leb : BinOp Nat.leb :=
-  { TBOp := fun x y => isLeZero (x-y) ;
-    TBOpInj := ltac:(
-                 intros;
-                 rewrite Z_of_nat_leb_iff;
-                 unfold isLeZero;
-                 rewrite Z_leb_sub;
-                 auto) }.
+  { TBOp := Z.leb ;
+    TBOpInj := Z_of_nat_leb_iff
+  }.
 Add BinOp Op_nat_leb.
 
 Instance Op_nat_ltb : BinOp Nat.ltb :=
-  { TBOp := fun x y => isLeZero (x+1-y) ;
-     TBOpInj := ltac:(
-                  intros;
-                  rewrite Z_of_nat_ltb_iff;
-                    unfold isLeZero;
-                    rewrite Z_ltb_leb;
-                    rewrite <- Z_leb_sub;
-                    reflexivity) }.
+  { TBOp := Z.ltb;
+    TBOpInj := Z_of_nat_ltb_iff
+  }.
 Add BinOp Op_nat_ltb.
-
-(** Injected boolean operators *)
-
-Lemma Z_eqb_ZSpec_ok : forall x,  0 <= isZero x <= 1 /\
-                                  (x = 0 <-> isZero x = 1).
-Proof.
-  intros.
-  unfold isZero.
-  destruct (x =? 0) eqn:EQ.
-  -  apply Z.eqb_eq in EQ.
-     simpl. intuition try congruence;
-     compute ; congruence.
-  - apply Z.eqb_neq in EQ.
-    simpl. intuition try congruence;
-             compute ; congruence.
-Qed.
-
-
-Instance Z_eqb_ZSpec : UnOpSpec isZero :=
-  {| UPred := fun n r => 0 <= r <= 1 /\ (n = 0 <-> isZero n = 1) ; USpec := Z_eqb_ZSpec_ok |}.
-Add Spec Z_eqb_ZSpec.
-
-Lemma leZeroSpec_ok : forall x,  x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0.
-Proof.
-  intros.
-  unfold isLeZero.
-  destruct (x <=? 0) eqn:EQ.
-  -  apply Z.leb_le in EQ.
-     simpl. intuition congruence.
-  -  simpl.
-     apply Z.leb_nle in EQ.
-     apply Zorder.Znot_le_gt in EQ.
-     tauto.
-Qed.
-
-Instance leZeroSpec : UnOpSpec isLeZero :=
-  {| UPred := fun n r => (n<=0 /\ r = 1) \/ (n > 0 /\ r = 0) ; USpec := leZeroSpec_ok|}.
-Add Spec leZeroSpec.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index 3eb4c924ae..65083791ca 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -34,19 +34,19 @@ Class InjTyp (S : Type) (T : Type) :=
 
 (** [BinOp Op] declares a source operator [Op: S1 -> S2 -> S3].
  *)
-Class BinOp {S1 S2 S3:Type} {T:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} :=
+Class BinOp {S1 S2 S3 T1 T2 T3:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T1} {I2 : InjTyp S2 T2} {I3 : InjTyp S3 T3} :=
   mkbop {
       (* [TBOp] is the target operator after injection of operands. *)
-      TBOp : T -> T -> T;
+      TBOp : T1 -> T2 -> T3;
       (* [TBOpInj] states the correctness of the injection. *)
       TBOpInj : forall (n:S1) (m:S2), inj (Op n m) = TBOp (inj n) (inj m)
     }.
 
 (** [Unop Op] declares a source operator [Op : S1 -> S2]. *)
-Class UnOp {S1 S2 T:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T}  :=
+Class UnOp {S1 S2 T1 T2:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T1} {I2 : InjTyp S2 T2}  :=
   mkuop {
       (* [TUOp] is the target operator after injection of operands. *)
-      TUOp : T -> T;
+      TUOp : T1 -> T2;
       (* [TUOpInj] states the correctness of the injection. *)
       TUOpInj : forall (x:S1), inj (Op x) = TUOp (inj x)
     }.
@@ -141,9 +141,6 @@ Record injprop  :=
       injprop_ok : source_prop <-> target_prop}.
 
 
-
-
-
 (** Lemmas for building rewrite rules. *)
 
 Definition PropOp_iff (Op : Prop -> Prop -> Prop) :=
@@ -152,22 +149,22 @@ Definition PropOp_iff (Op : Prop -> Prop -> Prop) :=
 Definition PropUOp_iff (Op : Prop -> Prop) :=
   forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1).
 
-Lemma mkapp2 (S1 S2 S3 T : Type) (Op : S1 -> S2 -> S3)
-      (I1 : S1 -> T) (I2 : S2 -> T) (I3 : S3 -> T)
-      (TBOP : T -> T -> T)
+Lemma mkapp2 (S1 S2 S3 T1 T2 T3 : Type) (Op : S1 -> S2 -> S3)
+      (I1 : S1 -> T1) (I2 : S2 -> T2) (I3 : S3 -> T3)
+      (TBOP : T1 -> T2 -> T3)
       (TBOPINJ : forall n m, I3 (Op n m) = TBOP (I1 n) (I2 m))
-      (s1 : S1) (t1 : T) (P1: I1 s1 = t1)
-      (s2 : S2) (t2 : T) (P2: I2 s2 = t2):  I3 (Op s1 s2) = TBOP t1 t2.
+      (s1 : S1) (t1 : T1) (P1: I1 s1 = t1)
+      (s2 : S2) (t2 : T2) (P2: I2 s2 = t2):  I3 (Op s1 s2) = TBOP t1 t2.
 Proof.
   subst. apply TBOPINJ.
 Qed.
 
-Lemma mkapp (S1 S2 T : Type) (OP : S1 -> S2)
-      (I1 : S1 -> T)
-      (I2 : S2 -> T)
-      (TUOP : T -> T)
+Lemma mkapp (S1 S2 T1 T2 : Type) (OP : S1 -> S2)
+      (I1 : S1 -> T1)
+      (I2 : S2 -> T2)
+      (TUOP : T1 -> T2)
       (TUOPINJ : forall n, I2 (OP n) = TUOP (I1 n))
-      (s1: S1) (t1: T) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1.
+      (s1: S1) (t1: T1) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1.
 Proof.
   subst. apply TUOPINJ.
 Qed.