Merge PR #11906: [micromega] native support for boolean operators

Reviewed-by: maximedenes
Reviewed-by: pi8027
Reviewed-by: vbgl

12 files changed, 1882 insertions, 1203 deletions

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..1bb016da9a 100644
--- a/theories/micromega/QMicromega.v
+++ b/theories/micromega/QMicromega.v
@@ -10,7 +10,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria)                                       *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -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..7e2694a519 100644
--- a/theories/micromega/RMicromega.v
+++ b/theories/micromega/RMicromega.v
@@ -10,19 +10,18 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria)                                       *)
 (*                                                                      *)
 (************************************************************************)
 
 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..fa3f123b18 100644
--- a/theories/micromega/ZifyBool.v
+++ b/theories/micromega/ZifyBool.v
@@ -9,177 +9,83 @@
 (************************************************************************)
 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 b => b = true \/ b = false) ;
+    cstr := (ltac:(intro b; destruct b; tauto))}.
+Add Zify InjTyp Inj_bool_bool.
 
 (** Boolean operators *)
 
 Instance Op_andb : BinOp andb :=
-  { TBOp := Z.min ;
-    TBOpInj := ltac: (destruct n,m; reflexivity)}.
-Add BinOp Op_andb.
+  { TBOp := andb ; TBOpInj := fun _ _  => eq_refl}.
+Add Zify BinOp Op_andb.
 
 Instance Op_orb : BinOp orb :=
-  { TBOp := Z.max ;
-    TBOpInj := ltac:(destruct n,m; reflexivity)}.
-Add BinOp Op_orb.
+  { TBOp := orb ; TBOpInj := fun _ _ => eq_refl}.
+Add Zify BinOp Op_orb.
 
 Instance Op_implb : BinOp implb :=
-  { TBOp := fun x y => Z.max (1 - x) y;
-    TBOpInj := ltac:(destruct n,m; reflexivity) }.
-Add BinOp Op_implb.
+  { TBOp := implb; TBOpInj := fun _ _ => eq_refl }.
+Add Zify 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) }.
-Add BinOp Op_xorb.
+  { TBOp := fun x y => andb (orb x y) (negb (eqb x y)); TBOpInj := xorb_eq }.
+Add Zify BinOp Op_xorb.
+
+Instance Op_eqb : BinOp eqb :=
+  { TBOp := eqb; TBOpInj := fun _ _ => eq_refl }.
+Add Zify BinOp Op_eqb.
 
 Instance Op_negb : UnOp negb :=
-  { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}.
-Add UnOp Op_negb.
+  { TUOp := negb ; TUOpInj := fun _ => eq_refl}.
+Add Zify UnOp Op_negb.
 
 Instance Op_eq_bool : BinRel (@eq bool) :=
-  {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }.
-Add BinRel Op_eq_bool.
+  {TR := @eq bool ; TRInj := ltac:(reflexivity) }.
+Add Zify BinRel Op_eq_bool.
 
 Instance Op_true : CstOp true :=
-  { TCst := 1 ; TCstInj := eq_refl }.
-Add CstOp Op_true.
+  { TCst := true ; TCstInj := eq_refl }.
+Add Zify CstOp Op_true.
 
 Instance Op_false : CstOp false :=
-  { TCst := 0 ; 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.
-
+  { TCst := false ; TCstInj := eq_refl }.
+Add Zify CstOp Op_false.
 
 (** 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 := fun _ _ => eq_refl }.
+Add Zify BinOp Op_Zeqb.
 
 Instance Op_Zleb : BinOp Z.leb :=
-  { TBOp := fun x y => isLeZero (x-y) ;
-    TBOpInj :=
-      ltac: (intros;unfold isLeZero;
-               rewrite Z_leb_sub;
-               auto) }.
-Add BinOp Op_Zleb.
+  { TBOp := Z.leb; TBOpInj :=  fun _ _ => eq_refl }.
+Add Zify 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) }.
-Add BinOp Op_Zgeb.
+  { TBOp := Z.geb; TBOpInj := fun _ _ => eq_refl }.
+Add Zify 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 := fun _ _ => eq_refl }.
+Add Zify BinOp Op_Zltb.
 
 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) }.
-Add BinOp Op_Zgtb.
+  { TBOp := Z.gtb; TBOpInj := fun _ _  => eq_refl }.
+Add Zify 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 +117,45 @@ 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) }.
-Add BinOp Op_nat_eqb.
+  { TBOp := Z.eqb; TBOpInj := Z_of_nat_eqb_iff }.
+Add Zify 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) }.
-Add BinOp Op_nat_leb.
+  { TBOp := Z.leb; TBOpInj := Z_of_nat_leb_iff }.
+Add Zify 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) }.
-Add BinOp Op_nat_ltb.
-
-(** Injected boolean operators *)
-
-Lemma Z_eqb_ZSpec_ok : forall x,  0 <= isZero x <= 1 /\
-                                  (x = 0 <-> isZero x = 1).
+  { TBOp := Z.ltb; TBOpInj := Z_of_nat_ltb_iff }.
+Add Zify BinOp Op_nat_ltb.
+
+Lemma b2n_b2z :  forall x,  Z.of_nat (Nat.b2n x) = Z.b2z x.
 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.
+  intro. destruct x ; reflexivity.
 Qed.
 
+Instance Op_b2n : UnOp Nat.b2n :=
+  { TUOp := Z.b2z; TUOpInj := b2n_b2z }.
+Add Zify UnOp Op_b2n.
 
-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.
+Instance Op_b2z : UnOp Z.b2z :=
+  { TUOp := Z.b2z; TUOpInj := fun _ => eq_refl }.
+Add Zify UnOp Op_b2z.
 
-Lemma leZeroSpec_ok : forall x,  x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0.
+Lemma b2z_spec : forall b, (b = true /\ Z.b2z b = 1) \/ (b = false /\ Z.b2z b = 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.
+  destruct b ; simpl; intuition congruence.
 Qed.
 
-Instance leZeroSpec : UnOpSpec isLeZero :=
-  {| UPred := fun n r => (n<=0 /\ r = 1) \/ (n > 0 /\ r = 0) ; USpec := leZeroSpec_ok|}.
-Add Spec leZeroSpec.
+Instance b2zSpec : UnOpSpec Z.b2z :=
+  { UPred := fun b r => (b = true /\ r = 1) \/ (b = false /\ r = 0);
+    USpec := b2z_spec
+  }.
+Add Zify UnOpSpec b2zSpec.
+
+Ltac elim_bool_cstr :=
+  repeat match goal with
+         | C : ?B = true \/ ?B = false |- _ =>
+           destruct C as [C|C]; rewrite C in *
+         end.
+
+Ltac Zify.zify_post_hook ::= elim_bool_cstr.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index 3eb4c924ae..37eef12381 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)
     }.
@@ -90,15 +90,15 @@ Class PropUOp (Op : Prop -> Prop) :=
     NB1: The Ltac code is currently limited to (Op: Z -> Z -> Z)
     NB2: This is not sufficient to cope with [Z.div] or [Z.mod]
  *)
-Class BinOpSpec {S T: Type} (Op : T -> T -> T) {I : InjTyp S T} :=
+Class BinOpSpec {T1 T2 T3: Type} (Op : T1 -> T2 -> T3)  :=
   mkbspec {
-      BPred : T -> T -> T -> Prop;
+      BPred : T1 -> T2 -> T3 -> Prop;
       BSpec : forall x y, BPred x y (Op x y)
     }.
 
-Class UnOpSpec {S T: Type} (Op : T -> T) {I : InjTyp S T} :=
+Class UnOpSpec {T1 T2: Type} (Op : T1 -> T2)  :=
   mkuspec {
-      UPred : T -> T -> Prop;
+      UPred : T1 -> T2 -> Prop;
       USpec : forall x, UPred x (Op 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.
@@ -223,8 +220,6 @@ Proof.
   exact (fun H => proj1 IFF H).
 Qed.
 
-Definition identity (A : Type) : A -> A := fun x => x.
-
 (** Registering constants for use by the plugin *)
 Register eq_iff      as ZifyClasses.eq_iff.
 Register target_prop as ZifyClasses.target_prop.
@@ -268,6 +263,4 @@ Register iff_morph as ZifyClasses.iff_morph.
 Register impl_morph as ZifyClasses.impl_morph.
 Register not as ZifyClasses.not.
 Register not_morph as ZifyClasses.not_morph.
-
-(** Identify function *)
-Register identity as ZifyClasses.identity.
+Register True as ZifyClasses.True.
diff --git a/theories/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v
index 9b37f10841..a4ada571f1 100644
--- a/theories/micromega/ZifyComparison.v
+++ b/theories/micromega/ZifyComparison.v
@@ -28,30 +28,30 @@ Qed.
 
 Instance Inj_comparison_Z : InjTyp comparison Z :=
   { inj := Z_of_comparison ; pred :=(fun x => -1 <= x <= 1) ; cstr := Z_of_comparison_bound}.
-Add InjTyp Inj_comparison_Z.
+Add Zify InjTyp Inj_comparison_Z.
 
 Definition ZcompareZ (x y : Z) :=
   Z_of_comparison (Z.compare x y).
 
 Program Instance BinOp_Zcompare : BinOp Z.compare :=
   { TBOp := ZcompareZ }.
-Add BinOp BinOp_Zcompare.
+Add Zify BinOp BinOp_Zcompare.
 
 Instance Op_eq_comparison : BinRel (@eq comparison) :=
   {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }.
-Add BinRel Op_eq_comparison.
+Add Zify BinRel Op_eq_comparison.
 
 Instance Op_Eq : CstOp Eq :=
   { TCst := 0 ; TCstInj := eq_refl }.
-Add CstOp Op_Eq.
+Add Zify CstOp Op_Eq.
 
 Instance Op_Lt : CstOp Lt :=
   { TCst := -1 ; TCstInj := eq_refl }.
-Add CstOp Op_Lt.
+Add Zify CstOp Op_Lt.
 
 Instance Op_Gt : CstOp Gt :=
   { TCst := 1 ; TCstInj := eq_refl }.
-Add CstOp Op_Gt.
+Add Zify CstOp Op_Gt.
 
 
 Lemma Zcompare_spec : forall x y,
@@ -79,4 +79,4 @@ Instance ZcompareSpec : BinOpSpec ZcompareZ :=
                            /\
                            (x < y  -> r = -1)
               ; BSpec := Zcompare_spec|}.
-Add Spec ZcompareSpec.
+Add Zify BinOpSpec ZcompareSpec.
diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
index 5b15dc072a..0e135ba793 100644
--- a/theories/micromega/ZifyInst.v
+++ b/theories/micromega/ZifyInst.v
@@ -25,117 +25,117 @@ Ltac refl :=
 
 Instance Inj_Z_Z : InjTyp Z Z :=
   mkinj _ _ (fun x => x) (fun x =>  True ) (fun _ => I).
-Add InjTyp Inj_Z_Z.
+Add Zify InjTyp Inj_Z_Z.
 
 (** Support for nat *)
 
 Instance Inj_nat_Z : InjTyp nat Z :=
   mkinj _ _ Z.of_nat (fun x =>  0 <= x ) Nat2Z.is_nonneg.
-Add InjTyp Inj_nat_Z.
+Add Zify InjTyp Inj_nat_Z.
 
 (* zify_nat_rel *)
 Instance Op_ge : BinRel ge :=
   {| TR := Z.ge; TRInj := Nat2Z.inj_ge |}.
-Add BinRel Op_ge.
+Add Zify BinRel Op_ge.
 
 Instance Op_lt : BinRel lt :=
   {| TR := Z.lt; TRInj := Nat2Z.inj_lt |}.
-Add BinRel Op_lt.
+Add Zify BinRel Op_lt.
 
 Instance Op_Nat_lt : BinRel Nat.lt := Op_lt.
-Add BinRel Op_Nat_lt.
+Add Zify BinRel Op_Nat_lt.
 
 Instance Op_gt : BinRel gt :=
   {| TR := Z.gt; TRInj := Nat2Z.inj_gt |}.
-Add BinRel Op_gt.
+Add Zify BinRel Op_gt.
 
 Instance Op_le : BinRel le :=
   {| TR := Z.le; TRInj := Nat2Z.inj_le |}.
-Add BinRel Op_le.
+Add Zify BinRel Op_le.
 
 Instance Op_Nat_le : BinRel Nat.le := Op_le.
-Add BinRel Op_Nat_le.
+Add Zify BinRel Op_Nat_le.
 
 Instance Op_eq_nat : BinRel (@eq nat) :=
   {| TR := @eq Z ; TRInj := fun x y : nat => iff_sym (Nat2Z.inj_iff x y) |}.
-Add BinRel Op_eq_nat.
+Add Zify BinRel Op_eq_nat.
 
 Instance Op_Nat_eq : BinRel (Nat.eq) := Op_eq_nat.
-Add BinRel Op_Nat_eq.
+Add Zify BinRel Op_Nat_eq.
 
 (* zify_nat_op *)
 Instance Op_plus : BinOp Nat.add :=
   {| TBOp := Z.add; TBOpInj := Nat2Z.inj_add |}.
-Add BinOp Op_plus.
+Add Zify BinOp Op_plus.
 
 Instance Op_sub : BinOp Nat.sub :=
   {| TBOp := fun n m => Z.max 0 (n - m) ; TBOpInj := Nat2Z.inj_sub_max |}.
-Add BinOp Op_sub.
+Add Zify BinOp Op_sub.
 
 Instance Op_mul : BinOp Nat.mul :=
   {| TBOp := Z.mul ; TBOpInj := Nat2Z.inj_mul |}.
-Add BinOp Op_mul.
+Add Zify BinOp Op_mul.
 
 Instance Op_min : BinOp Nat.min :=
   {| TBOp := Z.min ; TBOpInj := Nat2Z.inj_min |}.
-Add BinOp Op_min.
+Add Zify BinOp Op_min.
 
 Instance Op_max : BinOp Nat.max :=
   {| TBOp := Z.max ; TBOpInj := Nat2Z.inj_max |}.
-Add BinOp Op_max.
+Add Zify BinOp Op_max.
 
 Instance Op_pred : UnOp Nat.pred :=
   {| TUOp := fun n => Z.max 0 (n - 1) ; TUOpInj := Nat2Z.inj_pred_max |}.
-Add UnOp Op_pred.
+Add Zify UnOp Op_pred.
 
 Instance Op_S : UnOp S :=
   {| TUOp := fun x => Z.add x 1 ; TUOpInj := Nat2Z.inj_succ |}.
-Add UnOp Op_S.
+Add Zify UnOp Op_S.
 
 Instance Op_O : CstOp O :=
   {| TCst := Z0 ; TCstInj := eq_refl (Z.of_nat 0) |}.
-Add CstOp Op_O.
+Add Zify CstOp Op_O.
 
 Instance Op_Z_abs_nat : UnOp  Z.abs_nat :=
   { TUOp := Z.abs ; TUOpInj := Zabs2Nat.id_abs }.
-Add UnOp Op_Z_abs_nat.
+Add Zify UnOp Op_Z_abs_nat.
 
 (** Support for positive *)
 
 Instance Inj_pos_Z : InjTyp positive Z :=
   {| inj := Zpos ; pred := (fun x =>  0 < x ) ; cstr := Pos2Z.pos_is_pos |}.
-Add InjTyp Inj_pos_Z.
+Add Zify InjTyp Inj_pos_Z.
 
 Instance Op_pos_to_nat : UnOp  Pos.to_nat :=
   {TUOp := (fun x => x); TUOpInj := positive_nat_Z}.
-Add UnOp Op_pos_to_nat.
+Add Zify UnOp Op_pos_to_nat.
 
 Instance Inj_N_Z : InjTyp N Z :=
   mkinj _ _ Z.of_N (fun x =>  0 <= x ) N2Z.is_nonneg.
-Add InjTyp Inj_N_Z.
+Add Zify InjTyp Inj_N_Z.
 
 
 Instance Op_N_to_nat : UnOp  N.to_nat :=
   { TUOp := fun x => x ; TUOpInj := N_nat_Z }.
-Add UnOp Op_N_to_nat.
+Add Zify UnOp Op_N_to_nat.
 
 (* zify_positive_rel *)
 
 Instance Op_pos_ge : BinRel Pos.ge :=
   {| TR := Z.ge; TRInj := fun x y => iff_refl (Z.pos x >= Z.pos y) |}.
-Add BinRel Op_pos_ge.
+Add Zify BinRel Op_pos_ge.
 
 Instance Op_pos_lt : BinRel Pos.lt :=
   {| TR := Z.lt; TRInj := fun x y => iff_refl (Z.pos x < Z.pos y) |}.
-Add BinRel Op_pos_lt.
+Add Zify BinRel Op_pos_lt.
 
 Instance Op_pos_gt : BinRel Pos.gt :=
   {| TR := Z.gt; TRInj := fun x y => iff_refl (Z.pos x > Z.pos y)  |}.
-Add BinRel Op_pos_gt.
+Add Zify BinRel Op_pos_gt.
 
 Instance Op_pos_le : BinRel Pos.le :=
   {| TR := Z.le; TRInj := fun x y => iff_refl (Z.pos x <= Z.pos y) |}.
-Add BinRel Op_pos_le.
+Add Zify BinRel Op_pos_le.
 
 Lemma eq_pos_inj : forall (x y:positive), x = y <-> Z.pos x = Z.pos y.
 Proof.
@@ -145,36 +145,36 @@ Qed.
 
 Instance Op_eq_pos : BinRel (@eq positive) :=
   { TR := @eq Z ; TRInj := eq_pos_inj }.
-Add BinRel Op_eq_pos.
+Add Zify BinRel Op_eq_pos.
 
 (* zify_positive_op *)
 
 Instance Op_Z_of_N : UnOp Z.of_N :=
   { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }.
-Add UnOp Op_Z_of_N.
+Add Zify UnOp Op_Z_of_N.
 
 Instance Op_Z_to_N : UnOp Z.to_N :=
   { TUOp := fun x => Z.max 0 x ; TUOpInj := ltac:(now intro x; destruct x) }.
-Add UnOp Op_Z_to_N.
+Add Zify UnOp Op_Z_to_N.
 
 Instance Op_Z_neg : UnOp Z.neg :=
   { TUOp :=  Z.opp ; TUOpInj := (fun x => eq_refl (Zneg x))}.
-Add UnOp Op_Z_neg.
+Add Zify UnOp Op_Z_neg.
 
 Instance Op_Z_pos : UnOp Z.pos :=
   { TUOp := (fun x =>  x) ; TUOpInj := (fun x => eq_refl (Z.pos x))}.
-Add UnOp Op_Z_pos.
+Add Zify UnOp Op_Z_pos.
 
 Instance Op_pos_succ : UnOp Pos.succ :=
   { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ  }.
-Add UnOp Op_pos_succ.
+Add Zify UnOp Op_pos_succ.
 
 
 
 
 Instance Op_pos_pred_double : UnOp Pos.pred_double :=
 { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(refl) }.
-Add UnOp Op_pos_pred_double.
+Add Zify UnOp Op_pos_pred_double.
 
 Instance Op_pos_pred : UnOp Pos.pred :=
   { TUOp := fun x => Z.max 1 (x - 1) ;
@@ -182,266 +182,266 @@ Instance Op_pos_pred : UnOp Pos.pred :=
                  (intros;
                     rewrite <- Pos.sub_1_r;
                     apply Pos2Z.inj_sub_max) }.
-Add UnOp Op_pos_pred.
+Add Zify UnOp Op_pos_pred.
 
 Instance Op_pos_predN : UnOp Pos.pred_N :=
   { TUOp := fun x => x - 1 ;
     TUOpInj := ltac: (now destruct x; rewrite N.pos_pred_spec) }.
-Add UnOp Op_pos_predN.
+Add Zify UnOp Op_pos_predN.
 
 Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat :=
   { TUOp := fun x => x + 1 ; TUOpInj := Zpos_P_of_succ_nat }.
-Add UnOp Op_pos_of_succ_nat.
+Add Zify UnOp Op_pos_of_succ_nat.
 
 Instance Op_pos_of_nat : UnOp Pos.of_nat :=
   { TUOp := fun x => Z.max 1 x ;
     TUOpInj := ltac: (now destruct x;
                         [|rewrite <- Pos.of_nat_succ, <- (Nat2Z.inj_max 1)]) }.
-Add UnOp Op_pos_of_nat.
+Add Zify UnOp Op_pos_of_nat.
 
 Instance Op_pos_add : BinOp Pos.add :=
   { TBOp := Z.add ; TBOpInj := ltac: (refl) }.
-Add BinOp Op_pos_add.
+Add Zify BinOp Op_pos_add.
 
 Instance Op_pos_add_carry : BinOp Pos.add_carry :=
   { TBOp := fun x y => x + y + 1 ;
     TBOpInj := ltac:(now intros; rewrite Pos.add_carry_spec, Pos2Z.inj_succ) }.
-Add BinOp Op_pos_add_carry.
+Add Zify BinOp Op_pos_add_carry.
 
 Instance Op_pos_sub : BinOp Pos.sub :=
   { TBOp := fun n m => Z.max 1 (n - m) ;TBOpInj := Pos2Z.inj_sub_max }.
-Add BinOp Op_pos_sub.
+Add Zify BinOp Op_pos_sub.
 
 Instance Op_pos_mul : BinOp Pos.mul :=
   { TBOp :=  Z.mul ; TBOpInj := ltac: (refl) }.
-Add BinOp Op_pos_mul.
+Add Zify BinOp Op_pos_mul.
 
 Instance Op_pos_min : BinOp Pos.min :=
   { TBOp := Z.min ; TBOpInj := Pos2Z.inj_min }.
-Add BinOp Op_pos_min.
+Add Zify BinOp Op_pos_min.
 
 Instance Op_pos_max : BinOp Pos.max :=
   { TBOp := Z.max ; TBOpInj := Pos2Z.inj_max }.
-Add BinOp Op_pos_max.
+Add Zify BinOp Op_pos_max.
 
 Instance Op_pos_pow : BinOp Pos.pow :=
   { TBOp := Z.pow ; TBOpInj := Pos2Z.inj_pow }.
-Add BinOp Op_pos_pow.
+Add Zify BinOp Op_pos_pow.
 
 Instance Op_pos_square : UnOp Pos.square :=
   { TUOp := Z.square ; TUOpInj := Pos2Z.inj_square }.
-Add UnOp Op_pos_square.
+Add Zify UnOp Op_pos_square.
 
 Instance Op_xO : UnOp xO :=
   { TUOp := fun x => 2 * x ; TUOpInj := ltac: (refl) }.
-Add UnOp Op_xO.
+Add Zify UnOp Op_xO.
 
 Instance Op_xI : UnOp xI :=
   { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (refl) }.
-Add UnOp Op_xI.
+Add Zify UnOp Op_xI.
 
 Instance Op_xH : CstOp xH :=
   { TCst := 1%Z ; TCstInj := ltac:(refl)}.
-Add CstOp Op_xH.
+Add Zify CstOp Op_xH.
 
 Instance Op_Z_of_nat : UnOp Z.of_nat:=
   { TUOp := fun x => x ; TUOpInj := (fun x : nat => @eq_refl Z (Z.of_nat x)) }.
-Add UnOp Op_Z_of_nat.
+Add Zify UnOp Op_Z_of_nat.
 
 (* zify_N_rel *)
 Instance Op_N_ge : BinRel N.ge :=
   {| TR := Z.ge ; TRInj := N2Z.inj_ge |}.
-Add BinRel Op_N_ge.
+Add Zify BinRel Op_N_ge.
 
 Instance Op_N_lt : BinRel N.lt :=
   {| TR := Z.lt ; TRInj := N2Z.inj_lt |}.
-Add BinRel Op_N_lt.
+Add Zify BinRel Op_N_lt.
 
 Instance Op_N_gt : BinRel N.gt :=
   {| TR := Z.gt ; TRInj := N2Z.inj_gt |}.
-Add BinRel Op_N_gt.
+Add Zify BinRel Op_N_gt.
 
 Instance Op_N_le : BinRel N.le :=
   {| TR := Z.le ; TRInj := N2Z.inj_le |}.
-Add BinRel Op_N_le.
+Add Zify BinRel Op_N_le.
 
 Instance Op_eq_N : BinRel (@eq N) :=
   {| TR := @eq Z ; TRInj := fun x y : N => iff_sym (N2Z.inj_iff x y) |}.
-Add BinRel Op_eq_N.
+Add Zify BinRel Op_eq_N.
 
 (* zify_N_op *)
 Instance Op_N_N0 : CstOp  N0 :=
   { TCst := Z0 ; TCstInj := eq_refl }.
-Add CstOp Op_N_N0.
+Add Zify CstOp Op_N_N0.
 
 Instance Op_N_Npos : UnOp  Npos :=
   { TUOp := (fun x => x) ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_N_Npos.
+Add Zify UnOp Op_N_Npos.
 
 Instance Op_N_of_nat : UnOp  N.of_nat :=
   { TUOp := fun x => x ; TUOpInj := nat_N_Z }.
-Add UnOp Op_N_of_nat.
+Add Zify UnOp Op_N_of_nat.
 
 Instance Op_Z_abs_N : UnOp Z.abs_N :=
   { TUOp := Z.abs ; TUOpInj := N2Z.inj_abs_N }.
-Add UnOp Op_Z_abs_N.
+Add Zify UnOp Op_Z_abs_N.
 
 Instance Op_N_pos : UnOp N.pos :=
   { TUOp := fun x => x ; TUOpInj := ltac:(refl)}.
-Add UnOp Op_N_pos.
+Add Zify UnOp Op_N_pos.
 
 Instance Op_N_add : BinOp N.add :=
   {| TBOp := Z.add ; TBOpInj := N2Z.inj_add |}.
-Add BinOp Op_N_add.
+Add Zify BinOp Op_N_add.
 
 Instance Op_N_min : BinOp N.min :=
   {| TBOp := Z.min ; TBOpInj := N2Z.inj_min |}.
-Add BinOp Op_N_min.
+Add Zify BinOp Op_N_min.
 
 Instance Op_N_max : BinOp N.max :=
   {| TBOp := Z.max ; TBOpInj := N2Z.inj_max |}.
-Add BinOp Op_N_max.
+Add Zify BinOp Op_N_max.
 
 Instance Op_N_mul : BinOp N.mul :=
   {| TBOp := Z.mul ; TBOpInj := N2Z.inj_mul |}.
-Add BinOp Op_N_mul.
+Add Zify BinOp Op_N_mul.
 
 Instance Op_N_sub : BinOp N.sub :=
   {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}.
-Add BinOp Op_N_sub.
+Add Zify BinOp Op_N_sub.
 
 Instance Op_N_div : BinOp N.div :=
   {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}.
-Add BinOp Op_N_div.
+Add Zify BinOp Op_N_div.
 
 Instance Op_N_mod : BinOp N.modulo :=
   {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}.
-Add BinOp Op_N_mod.
+Add Zify BinOp Op_N_mod.
 
 Instance Op_N_pred : UnOp N.pred :=
   { TUOp := fun x  => Z.max 0 (x - 1) ;
     TUOpInj :=
       ltac:(intros; rewrite N.pred_sub; apply N2Z.inj_sub_max) }.
-Add UnOp Op_N_pred.
+Add Zify UnOp Op_N_pred.
 
 Instance Op_N_succ : UnOp N.succ :=
   {| TUOp := fun x => x + 1 ; TUOpInj := N2Z.inj_succ |}.
-Add UnOp Op_N_succ.
+Add Zify UnOp Op_N_succ.
 
 (** Support for Z - injected to itself *)
 
 (* zify_Z_rel *)
 Instance Op_Z_ge : BinRel Z.ge :=
   {| TR := Z.ge ; TRInj := fun x y  => iff_refl (x>= y)|}.
-Add BinRel Op_Z_ge.
+Add Zify BinRel Op_Z_ge.
 
 Instance Op_Z_lt : BinRel Z.lt :=
   {| TR := Z.lt ;  TRInj := fun x y  => iff_refl (x < y)|}.
-Add BinRel Op_Z_lt.
+Add Zify BinRel Op_Z_lt.
 
 Instance Op_Z_gt : BinRel Z.gt :=
   {| TR := Z.gt ;TRInj := fun x y  => iff_refl (x > y)|}.
-Add BinRel Op_Z_gt.
+Add Zify BinRel Op_Z_gt.
 
 Instance Op_Z_le : BinRel Z.le :=
   {| TR := Z.le ;TRInj := fun x y  => iff_refl (x <= y)|}.
-Add BinRel Op_Z_le.
+Add Zify BinRel Op_Z_le.
 
 Instance Op_eqZ : BinRel (@eq Z) :=
   { TR := @eq Z ; TRInj := fun x y  => iff_refl (x = y) }.
-Add BinRel Op_eqZ.
+Add Zify BinRel Op_eqZ.
 
 Instance Op_Z_Z0 : CstOp Z0 :=
   { TCst := Z0  ; TCstInj := eq_refl }.
-Add CstOp Op_Z_Z0.
+Add Zify CstOp Op_Z_Z0.
 
 Instance Op_Z_add : BinOp Z.add :=
   { TBOp := Z.add  ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_add.
+Add Zify BinOp Op_Z_add.
 
 Instance Op_Z_min : BinOp Z.min :=
   { TBOp := Z.min ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_min.
+Add Zify BinOp Op_Z_min.
 
 Instance Op_Z_max : BinOp Z.max :=
   { TBOp := Z.max ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_max.
+Add Zify BinOp Op_Z_max.
 
 Instance Op_Z_mul : BinOp Z.mul :=
   { TBOp := Z.mul ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_mul.
+Add Zify BinOp Op_Z_mul.
 
 Instance Op_Z_sub : BinOp Z.sub :=
   { TBOp := Z.sub ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_sub.
+Add Zify BinOp Op_Z_sub.
 
 Instance Op_Z_div : BinOp Z.div :=
   { TBOp := Z.div ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_div.
+Add Zify BinOp Op_Z_div.
 
 Instance Op_Z_mod : BinOp Z.modulo :=
   { TBOp := Z.modulo ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_mod.
+Add Zify BinOp Op_Z_mod.
 
 Instance Op_Z_rem : BinOp Z.rem :=
   { TBOp := Z.rem ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_rem.
+Add Zify BinOp Op_Z_rem.
 
 Instance Op_Z_quot : BinOp Z.quot :=
   { TBOp := Z.quot ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_quot.
+Add Zify BinOp Op_Z_quot.
 
 Instance Op_Z_succ : UnOp Z.succ :=
   { TUOp := fun x => x + 1 ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_succ.
+Add Zify UnOp Op_Z_succ.
 
 Instance Op_Z_pred : UnOp Z.pred :=
   { TUOp := fun x => x - 1 ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_pred.
+Add Zify UnOp Op_Z_pred.
 
 Instance Op_Z_opp : UnOp Z.opp :=
   { TUOp := Z.opp ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_opp.
+Add Zify UnOp Op_Z_opp.
 
 Instance Op_Z_abs : UnOp Z.abs :=
   { TUOp := Z.abs ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_abs.
+Add Zify UnOp Op_Z_abs.
 
 Instance Op_Z_sgn : UnOp Z.sgn :=
   { TUOp := Z.sgn ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_sgn.
+Add Zify UnOp Op_Z_sgn.
 
 Instance Op_Z_pow : BinOp Z.pow :=
   { TBOp := Z.pow ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_pow.
+Add Zify BinOp Op_Z_pow.
 
 Instance Op_Z_pow_pos : BinOp Z.pow_pos :=
   { TBOp := Z.pow ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_pow_pos.
+Add Zify BinOp Op_Z_pow_pos.
 
 Instance Op_Z_double : UnOp Z.double :=
   { TUOp := Z.mul 2 ; TUOpInj := Z.double_spec }.
-Add UnOp Op_Z_double.
+Add Zify UnOp Op_Z_double.
 
 Instance Op_Z_pred_double : UnOp Z.pred_double :=
   { TUOp := fun x => 2 * x - 1 ; TUOpInj := Z.pred_double_spec }.
-Add UnOp Op_Z_pred_double.
+Add Zify UnOp Op_Z_pred_double.
 
 Instance Op_Z_succ_double : UnOp Z.succ_double :=
   { TUOp := fun x => 2 * x + 1 ; TUOpInj := Z.succ_double_spec }.
-Add UnOp Op_Z_succ_double.
+Add Zify UnOp Op_Z_succ_double.
 
 Instance Op_Z_square : UnOp Z.square :=
   { TUOp := fun x => x * x ; TUOpInj := Z.square_spec }.
-Add UnOp Op_Z_square.
+Add Zify UnOp Op_Z_square.
 
 Instance Op_Z_div2 : UnOp Z.div2 :=
   { TUOp := fun x => x / 2 ; TUOpInj := Z.div2_div }.
-Add UnOp Op_Z_div2.
+Add Zify UnOp Op_Z_div2.
 
 Instance Op_Z_quot2 : UnOp Z.quot2 :=
   { TUOp := fun x => Z.quot x 2 ; TUOpInj := Zeven.Zquot2_quot }.
-Add UnOp Op_Z_quot2.
+Add Zify UnOp Op_Z_quot2.
 
 Lemma of_nat_to_nat_eq : forall x,  Z.of_nat (Z.to_nat x) = Z.max 0 x.
 Proof.
@@ -455,49 +455,28 @@ Qed.
 
 Instance Op_Z_to_nat : UnOp Z.to_nat :=
   { TUOp := fun x => Z.max 0 x ; TUOpInj := of_nat_to_nat_eq }.
-Add UnOp Op_Z_to_nat.
+Add Zify UnOp Op_Z_to_nat.
 
 (** Specification of derived operators over Z *)
 
-Lemma z_max_spec : forall n m,
-    n <= Z.max n m /\ m <= Z.max n m /\ (Z.max n m = n \/ Z.max n m = m).
-Proof.
-  intros.
-  generalize (Z.le_max_l n m).
-  generalize (Z.le_max_r n m).
-  generalize (Z.max_spec_le n m).
-  intuition idtac.
-Qed.
-
 Instance ZmaxSpec : BinOpSpec Z.max :=
   {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}.
-Add Spec ZmaxSpec.
-
-Lemma z_min_spec : forall n m,
-    Z.min n m <= n /\ Z.min n m <= m /\ (Z.min n m = n \/ Z.min n m = m).
-Proof.
-  intros.
-  generalize (Z.le_min_l n m).
-  generalize (Z.le_min_r n m).
-  generalize (Z.min_spec_le n m).
-  intuition idtac.
-Qed.
-
+Add Zify BinOpSpec ZmaxSpec.
 
 Instance ZminSpec : BinOpSpec Z.min :=
   {| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ;
      BSpec := Z.min_spec |}.
-Add Spec ZminSpec.
+Add Zify BinOpSpec ZminSpec.
 
 Instance ZsgnSpec : UnOpSpec Z.sgn :=
   {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ;
      USpec := Z.sgn_spec|}.
-Add Spec ZsgnSpec.
+Add Zify UnOpSpec ZsgnSpec.
 
 Instance ZabsSpec : UnOpSpec Z.abs :=
   {| UPred := fun n r: Z =>  0 <= n /\ r = n \/ n < 0 /\ r = - n ;
      USpec := Z.abs_spec|}.
-Add Spec ZabsSpec.
+Add Zify UnOpSpec ZabsSpec.
 
 (** Saturate positivity constraints *)
 
@@ -508,7 +487,7 @@ Instance SatProd : Saturate Z.mul :=
     PRes  := fun r => 0 <= r;
     SatOk := Z.mul_nonneg_nonneg
   |}.
-Add Saturate SatProd.
+Add Zify Saturate SatProd.
 
 Instance SatProdPos : Saturate Z.mul :=
   {|
@@ -517,7 +496,7 @@ Instance SatProdPos : Saturate Z.mul :=
     PRes  := fun r => 0 < r;
     SatOk := Z.mul_pos_pos
   |}.
-Add Saturate SatProdPos.
+Add Zify Saturate SatProdPos.
 
 Lemma pow_pos_strict :
   forall a b,
@@ -536,4 +515,4 @@ Instance SatPowPos : Saturate Z.pow :=
     PRes  := fun r => 0 < r;
     SatOk := pow_pos_strict
   |}.
-Add Saturate SatPowPos.
+Add Zify Saturate SatPowPos.