Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10

7 files changed, 648 insertions, 715 deletions

diff --git a/src/QInst.v b/src/QInst.v
index 8971380..2306c40 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -88,14 +88,7 @@ Qed.
 (* An auxiliary lemma to rewrite an eqb_of_compdec into its the symmetrical version *)
 Lemma eqb_of_compdec_sym (A:Type) (HA:CompDec A) (a b:A) :
   eqb_of_compdec HA b a = eqb_of_compdec HA a b.
-Proof.
-  destruct (@eq_dec _ (@Decidable _ HA) a b) as [H|H].
-  - now rewrite H.
-  - case_eq (eqb_of_compdec HA a b).
-    + now rewrite <- !(@compdec_eq_eqb _ HA).
-    + intros _. case_eq (eqb_of_compdec HA b a); auto.
-      intro H1. elim H. symmetry. now rewrite compdec_eq_eqb.
-Qed.
+Proof. apply eqb_sym2. Qed.
 
 (* First strategy: change the order of all equalities in the goal or the
    hypotheses
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 148d6d7..aa49904 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -274,13 +274,13 @@ Module Typ.
       match t with
       | TFArray ti te =>
         existT (fun ty : Type => CompDec ty)
-               (@farray (type_compdec (projT2 (interp_compdec_aux ti)))
-                        (type_compdec (projT2 (interp_compdec_aux te)))
+               (@farray (projT1 (interp_compdec_aux ti))
+                        (projT1 (interp_compdec_aux te))
                         (@ord_of_compdec _ (projT2 (interp_compdec_aux ti)))
                         (@inh_of_compdec _ (projT2 (interp_compdec_aux te))))
                (FArray_compdec
-                  (type_compdec (projT2 (interp_compdec_aux ti)))
-                  (type_compdec (projT2 (interp_compdec_aux te))))
+                  (projT1 (interp_compdec_aux ti))
+                  (projT1 (interp_compdec_aux te)))
       | Tindex i =>
         existT (fun ty : Type => CompDec ty)
                (te_carrier (t_i .[ i])) (te_compdec (t_i .[ i]))
@@ -293,7 +293,7 @@ Module Typ.
     Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) :=
       projT2 (interp_compdec_aux t).
 
-    Definition interp (t:type) : Type := type_compdec (interp_compdec t).
+    Definition interp (t:type) : Type := projT1 (interp_compdec_aux t).
 
 
     Definition interp_ftype (t:ftype) :=
@@ -302,23 +302,26 @@ Module Typ.
 
 
     Definition dec_interp (t:type) : DecType (interp t).
-      destruct (interp_compdec t).
-      subst ty.
-      apply Decidable.
-    Defined.
-
-    Instance comp_interp (t:type) : Comparable (interp t).
-      destruct (interp_compdec t).
-      subst ty.
-      apply Comp.
+    Proof.
+      unfold interp.
+      destruct (interp_compdec_aux t) as [x c]. simpl.
+      apply EqbToDecType.
     Defined.
 
     Instance ord_interp (t:type) : OrdType (interp t).
-      destruct (interp_compdec t).
-      subst ty.
+    Proof.
+      unfold interp.
+      destruct (interp_compdec_aux t) as [x c]. simpl.
       apply Ordered.
     Defined.
 
+    Instance comp_interp (t:type) : Comparable (interp t).
+    Proof.
+      unfold interp, ord_interp.
+      destruct (interp_compdec_aux t) as [x c]. simpl.
+      apply Comp.
+    Defined.
+
 
     Definition inh_interp (t:type) : Inhabited (interp t).
       unfold interp.
@@ -326,7 +329,7 @@ Module Typ.
       apply Inh.
     Defined.
 
-    Definition inhabitant_interp (t:type) : interp t := default_value.
+    Definition inhabitant_interp (t:type) : interp t := @default_value _ (inh_interp _).
 
 
     Hint Resolve
@@ -344,28 +347,18 @@ Module Typ.
 
       Lemma eqb_compdec_spec {t} (c : CompDec t) : forall x y,
           eqb_of_compdec c x y = true <-> x = y.
-        intros.
-        destruct c.
-        destruct Eqb.
-        simpl.
-        auto.
+      Proof.
+        intros x y.
+        destruct c as [[E HE] O C I].
+        unfold eqb_of_compdec.
+        simpl. now rewrite HE.
       Qed.
 
       Lemma eqb_compdec_spec_false {t} (c : CompDec t) : forall x y,
           eqb_of_compdec c x y = false <-> x <> y.
-        intros.
-        destruct c.
-        destruct Eqb.
-        simpl.
-        split. intros.
-        unfold not. intros.
-        apply eqb_spec in H0.
-        rewrite H in H0. now contradict H0.
-        intros. unfold not in H.
-        rewrite <- not_true_iff_false.
-        unfold not. intros.
-        apply eqb_spec in H0.
-        apply H in H0. now contradict H0.
+      Proof.
+        intros x y.
+        apply eqb_spec_false.
       Qed.
 
       Lemma i_eqb_spec : forall t x y, i_eqb t x y <-> x = y.
@@ -384,12 +377,9 @@ Module Typ.
 
       Lemma reflect_eqb_compdec {t} (c : CompDec t) : forall x y,
           reflect (x = y) (eqb_of_compdec c x y).
-        intros.
-        destruct c.
-        destruct Eqb.
-        simpl in *.
-        apply iff_reflect.
-        symmetry; auto.
+      Proof.
+        intros x y.
+        apply reflect_eqb.
       Qed.
 
 
@@ -401,15 +391,8 @@ Module Typ.
       Qed.
 
      Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x.
-     Proof.
-       intros t x y; case_eq (i_eqb t x y); intro H1; symmetry;
-          [ | rewrite neg_eq_true_eq_false in *; intro H2; apply H1];
-          rewrite is_true_iff in *; now rewrite i_eqb_spec in *.
-      Qed.
-
+     Proof. intros. apply eqb_sym2. Qed.
 
-      (* Lemma i_eqb_compdec_tbv (c: CompDec): forall x y,  TBV x y = BITVECTOR_LIST_FIXED.bv_eq x y.  *)
-      (* Proof. *)
 
       Definition i_eqb_eqb (t:type) : interp t -> interp t -> bool :=
         match t with
@@ -424,11 +407,9 @@ Module Typ.
 
       Lemma eqb_compdec_refl {t} (c : CompDec t) : forall x,
           eqb_of_compdec c x x = true.
-        intros.
-        destruct c.
-        destruct Eqb.
-        simpl.
-        apply eqb_spec. auto.
+      Proof.
+        intro x.
+        apply eqb_refl.
       Qed.
 
       Lemma i_eqb_refl : forall t x, i_eqb t x x.
@@ -442,15 +423,10 @@ Module Typ.
       Lemma eqb_compdec_trans {t} (c : CompDec t) : forall x y z,
           eqb_of_compdec c x y = true ->
           eqb_of_compdec c y z = true ->
-          eqb_of_compdec c x z = true .
-        intros.
-        destruct c.
-        destruct Eqb.
-        simpl in *.
-        apply eqb_spec.
-        apply eqb_spec in H.
-        apply eqb_spec in H0.
-        subst; auto.
+          eqb_of_compdec c x z = true.
+      Proof.
+        intros x y z.
+        apply eqb_trans.
       Qed.
 
       Lemma i_eqb_trans : forall t x y z, i_eqb t x y -> i_eqb t y z -> i_eqb t x z.
@@ -1547,13 +1523,13 @@ Qed.
            apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_shr s)
          | BO_select ti te => apply_binop (Typ.TFArray ti te) ti te FArray.select
          | BO_diffarray ti te =>
-           apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti FArray.diff
+           apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te))
          end.
 
       Definition interp_top o :=
          match o with
          | TO_store ti te =>
-           apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) FArray.store
+           apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i te))
          end.
 
       Fixpoint compute_interp ty acc l :=
@@ -1987,7 +1963,11 @@ Qed.
         rewrite H2, H3, H1.
         rewrite !Typ.cast_refl.
         intros.
-        exists (FArray.diff x1 x2); auto.
+        exists ((@FArray.diff (Typ.interp t_i t') (Typ.interp t_i te)
+             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t')))
+             (ord_of_compdec _)
+             (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
+             (Typ.comp_interp t_i te) (Typ.inh_interp t_i t') (Typ.inh_interp t_i te) x1 x2)); auto.
 
         (* Ternary operatores *)
         destruct op as [ti te]; intros [ ti' te' | | | | | ];
@@ -2008,7 +1988,11 @@ Qed.
         intros.
         rewrite !Typ.cast_refl.
         intros.
-        exists (FArray.store x1 x2 x3); auto.
+        exists ((@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te')
+             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti')))
+             (ord_of_compdec _)
+             (comp_of_compdec _) (Typ.ord_interp t_i te') (Typ.comp_interp t_i te')
+             (Typ.inh_interp t_i te') x1 x2 x3)); auto.
 
         (* N-ary operators *)
         destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha).
@@ -2483,7 +2467,12 @@ Qed.
           simpl; try (exists true; auto); intro k1;
             case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TFArray ti te)) as [k2| ];
             simpl; try (exists true; reflexivity).
-        exists (FArray.diff (k1 interp_t x) (k2 interp_t y)); auto.
+        exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te)
+             (@EqbToDecType _ (@eqbtype_of_compdec _(Typ.interp_compdec t_i ti)))
+             (ord_of_compdec _)
+             (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
+             (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te)
+             (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto.
 
         (* Ternary operators *)
         intros [ti te] h1 h2 h3; simpl; rewrite !andb_true_iff; intros [[H1 H2] H3];
@@ -2496,7 +2485,12 @@ Qed.
           simpl; try (exists true; auto); intro k2;
             case (Typ.cast (v_type Typ.type interp_t (a .[ h3])) te) as [k3| ];
             simpl; try (exists true; reflexivity).
-         exists (FArray.store (k1 interp_t x) (k2 interp_t y) (k3 interp_t z)); auto.
+         exists (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te)
+             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti)))
+             (ord_of_compdec _)
+             (comp_of_compdec _) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te)
+             (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y)
+             (k3 (Typ.interp t_i) z)); auto.
 
         (* N-ary operators *)
         intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 < h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl.
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index da0f6f2..5bf0eaa 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -380,8 +380,11 @@ Section certif.
 
         rewrite H6d1, H6d2, H14.
         intros.
-        specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) 
-        (store v_val2 v_val3 v_val4) (v_val0)).
+        specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t)
+          (@store _ _
+                  (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0)))
+               _ _ _ (Typ.comp_interp t_i t) _
+               v_val2 v_val3 v_val4) v_val0).
         intros. specialize (H18 H6).
         rewrite <- H18.
 
@@ -397,7 +400,8 @@ Section certif.
         intros. specialize (H20 Htia2).
         rewrite <- H20.
         apply Typ.i_eqb_spec.
-        apply (read_over_write (elt_dec:=(EqbToDecType _ (@Eqb _ _)))).
+        apply (read_over_write (elt_dec:=(@EqbToDecType _ (@Eqb _
+                   (projT2 (Typ.interp_compdec_aux t_i _)))))).
     Qed.
 
 
@@ -677,9 +681,12 @@ Section certif.
 
           rewrite H25a, H25b, H10. intros.
           specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2)
-                                     (store v_vale1 v_vale2 v_vale3) (v_vald1')).
+            (@store _ _
+                    (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1)))
+                   _ _ _ (Typ.comp_interp t_i t2) _
+                   v_vale1 v_vale2 v_vale3) (v_vald1')).
           intro H25. specialize (H25 Htid1').
-          
+
           unfold Atom.interp_form_hatom, interp_hatom.
           rewrite !Atom.t_interp_wf; trivial.
           rewrite Heq6. simpl.
@@ -725,7 +732,7 @@ Section certif.
             subst; intros;
 
               rewrite Htid2 in Htic2;
-              rewrite <- (Atom.Bval_inj2 _ _  (v_vald2) (v_valc2) Htic2) in *. 
+              rewrite <- (Atom.Bval_inj2 _ _  (v_vald2) (v_valc2) Htic2) in *.
           
           + rewrite Htie2 in Htia1.
             rewrite Htia2 in Htic2''.
@@ -831,7 +838,10 @@ Section certif.
 
           rewrite H25a, H25b, H10. intros.
           specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2)
-                                     (store v_vale1 v_vale2 v_vale3) (v_valc1')).
+            (@store _ _
+                   (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1)))
+                   _ _ _ (Typ.comp_interp t_i t2) _
+                   v_vale1 v_vale2 v_vale3) (v_valc1')).
           intro H25. specialize (H25 Htic1').
           
           unfold Atom.interp_form_hatom, interp_hatom.
@@ -878,7 +888,7 @@ Section certif.
             subst; intros;
 
               rewrite Htid2 in Htic2;
-              rewrite <- (Atom.Bval_inj2 _ _  (v_vald2) (v_valc2) Htic2) in *. 
+              rewrite <- (Atom.Bval_inj2 _ _  (v_vald2) (v_valc2) Htic2) in *.
           
           + rewrite Htie2 in Htia1.
             rewrite Htia2 in Htic2''.
@@ -1169,7 +1179,10 @@ Section certif.
     unfold Bval. rewrite <- H25.
     rewrite !Typ.cast_refl. intros.
 
-    specialize (Atom.Bval_inj2 t_i t0 (diff v_valf1 v_valf2) (v_vald2')).
+    specialize (Atom.Bval_inj2 t_i t0 (@diff _ _
+       (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0)))
+       _ _ (Typ.dec_interp t_i v_typec2') _ (Typ.comp_interp t_i v_typec2') (Typ.inh_interp t_i t0) _
+       v_valf1 v_valf2) (v_vald2')).
     intros. specialize (H29 Htid2').
 
     (* semantics *)
@@ -1212,7 +1225,57 @@ Section certif.
     apply negb_true_iff.
     apply Typ.i_eqb_spec_false.
     subst.
-    specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (diff v_valf1 v_valf2)).
+    specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (@diff (Typ.interp t_i v_typed2') (Typ.interp t_i v_typec1')
+             (@EqbToDecType
+                _
+                (@eqbtype_of_compdec
+                   _
+                   (Typ.interp_compdec t_i v_typed2')))
+             _
+             (@comp_of_compdec (Typ.interp t_i v_typed2')
+                (projT2
+                   ((fix interp_compdec_aux (t : Typ.type) :
+                       @sigT Type (fun ty : Type => CompDec ty) :=
+                       match t return (@sigT Type (fun ty : Type => CompDec ty)) with
+                       | Typ.TFArray ti te =>
+                           @existT Type (fun ty : Type => CompDec ty)
+                             (@farray
+                                (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti))
+                                (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te))
+                                (@ord_of_compdec
+                                   (@projT1 Type (fun ty : Type => CompDec ty)
+                                      (interp_compdec_aux ti))
+                                   (@projT2 Type (fun ty : Type => CompDec ty)
+                                      (interp_compdec_aux ti)))
+                                (@inh_of_compdec
+                                   (@projT1 Type (fun ty : Type => CompDec ty)
+                                      (interp_compdec_aux te))
+                                   (@projT2 Type (fun ty : Type => CompDec ty)
+                                      (interp_compdec_aux te))))
+                             (@SMT_classes_instances.FArray_compdec
+                                (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti))
+                                (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te))
+                                (@projT2 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti))
+                                (@projT2 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te)))
+                       | Typ.Tindex i =>
+                           @existT Type (fun ty : Type => CompDec ty)
+                             (te_carrier (@get typ_compdec t_i i))
+                             (te_compdec (@get typ_compdec t_i i))
+                       | Typ.TZ =>
+                           @existT Type (fun ty : Type => CompDec ty) BinNums.Z
+                             SMT_classes_instances.Z_compdec
+                       | Typ.Tbool =>
+                           @existT Type (fun ty : Type => CompDec ty) bool
+                             SMT_classes_instances.bool_compdec
+                       | Typ.Tpositive =>
+                           @existT Type (fun ty : Type => CompDec ty) BinNums.positive
+                             SMT_classes_instances.Positive_compdec
+                       | Typ.TBV n =>
+                           @existT Type (fun ty : Type => CompDec ty)
+                             (BVList.BITVECTOR_LIST.bitvector n) (SMT_classes_instances.BV_compdec n)
+                       end) v_typed2'))) (Typ.dec_interp t_i v_typec1')
+             _ (Typ.comp_interp t_i v_typec1')
+             (Typ.inh_interp t_i v_typed2') (Typ.inh_interp t_i v_typec1') v_valf1 v_valf2)).
     intros. specialize (H5 Htid2''').
     rewrite <- H5.
     specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)).
diff --git a/src/array/FArray.v b/src/array/FArray.v
index bc079d7..6eec859 100644
--- a/src/array/FArray.v
+++ b/src/array/FArray.v
@@ -54,10 +54,7 @@ Module Raw.
 
   Definition ltk (a b : (key * elt)) := lt (fst a) (fst b).
 
-  (* Definition ltke (a b : (key * elt)) := *)
-  (*   lt (fst a) (fst b) \/ ( (fst a) = (fst b) /\ lt (snd a) (snd b)). *)
-
-  Hint Unfold ltk (* ltke *) eqk eqke : smtcoq_array.
+  Hint Unfold ltk eqk eqke : smtcoq_array.
   Hint Extern 2 (eqke ?a ?b) => split : smtcoq_array.
 
   Global Instance lt_key_strorder : StrictOrder (lt : key -> key -> Prop).
@@ -69,8 +66,6 @@ Module Raw.
   Global Instance ke_dec : DecType (key * elt).
   Proof.
     split; auto.
-    intros; destruct x, y, z.
-    inversion H. inversion H0. trivial.
     intros; destruct x, y.
     destruct (eq_dec k k0).
     destruct (eq_dec e e0).
@@ -107,45 +102,6 @@ Module Raw.
 
   Hint Unfold MapsTo In : smtcoq_array.
 
-  (* Instance ke_ord: OrdType (key * elt). *)
-  (* Proof. *)
-  (*   exists ltke. *)
-  (*   unfold ltke. intros. *)
-  (*   destruct H, H0. *)
-  (*   left; apply (lt_trans _ (fst y)); auto. *)
-  (*   destruct H0. left. rewrite <- H0. assumption. *)
-  (*   destruct H. left. rewrite H. assumption. *)
-  (*   destruct H, H0. *)
-  (*   right. split. *)
-  (*   apply (eq_trans _ (fst y)); trivial. *)
-  (*   apply (lt_trans _ (snd y)); trivial. *)
-  (*   unfold ltke. intros. *)
-  (*   destruct x, y. simpl in H. *)
-  (*   destruct H. *)
-  (*   apply lt_not_eq in H. *)
-  (*   unfold not in *. intro. inversion H0. apply H. trivial. *)
-  (*   destruct H. apply lt_not_eq in H0. unfold not in *. intro.  *)
-  (*   inversion H1. apply H0; trivial. *)
-  (*   intros. *)
-  (*   unfold ltke. *)
-  (*   destruct (compare (fst x) (fst y)). *)
-  (*   apply LT. left; assumption. *)
-  (*   destruct (compare (snd x) (snd y)). *)
-  (*   apply LT. right; split; assumption. *)
-  (*   apply EQ. destruct x, y. simpl in *. rewrite e, e0; trivial. *)
-  (*   apply GT. right; symmetry in e; split; assumption. *)
-  (*   apply GT. left; assumption. *)
-  (* Qed. *)
-
-  (* Hint Immediate ke_ord. *)
-  (* Let ke_ord := ke_ord. *)
-
-  (* Instance keyelt_ord: OrdType (key * elt). *)
-
-
-  (* Variable keyelt_ord : OrdType (key * elt). *)
-   (* eqke is stricter than eqk *)
-
    Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
    Proof.
      unfold eqk, eqke; intuition.
@@ -166,15 +122,15 @@ Module Raw.
   Proof. unfold eqke; intuition. Qed.
 
   Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
-  Proof. eauto with smtcoq_array. Qed.
+  Proof. unfold eqk; now intros e1 e2 e3 ->. Qed.
 
   Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
   Proof.
-    unfold eqke; intuition; [ eauto with smtcoq_array | congruence ].
+    unfold eqke; intros [k1 e1] [k2 e2] [k3 e3]; simpl; now intros [-> ->].
   Qed.
 
   Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''.
-  Proof. eauto with smtcoq_array. Qed.
+  Proof. unfold ltk; eauto. Qed.
 
   Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
   Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto with smtcoq_array. Qed.
@@ -203,25 +159,12 @@ Module Raw.
     unfold Transitive. intros x y z. apply lt_trans.
   Qed.
 
-  (* Instance ltke_strorder : StrictOrder ltke. *)
-  (* Proof. *)
-  (*   split. *)
-  (*   unfold Irreflexive, Reflexive, complement. *)
-  (*   intros. apply lt_not_eq in H; auto with smtcoq_array. *)
-  (*   unfold Transitive. apply lt_trans. *)
-  (* Qed. *)
-
   Global Instance eq_equiv : @Equivalence (key * elt) eq.
   Proof.
     split; auto with smtcoq_array.
     unfold Transitive. apply eq_trans.
   Qed.
 
-  (* Instance ltke_compat : Proper (eq ==> eq ==> iff) ltke. *)
-  (* Proof. *)
-  (*   split; rewrite H, H0; trivial. *)
-  (* Qed. *)
-
   Global Instance ltk_compat : Proper (eq ==> eq ==> iff) ltk.
   Proof.
     split; rewrite H, H0; trivial.
@@ -276,27 +219,6 @@ Module Raw.
 
   Hint Resolve InA_eqke_eqk : smtcoq_array.
 
-  (* Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. *)
-  (* Proof. *)
-  (*  intros; apply InA_eqA with p; auto with smtcoq_array with *. *)
-  (* Qed. *)
-
-  (* Lemma In_eq : forall l x y, eq x y -> InA eqke x l -> InA eqke y l. *)
-  (* Proof. intros. rewrite <- H; auto with smtcoq_array. Qed. *)
-
-  (* Lemma ListIn_In : forall l x, List.In x l -> InA eqk x l. *)
-  (* Proof. apply In_InA. split; auto with smtcoq_array. unfold Transitive. *)
-  (*   unfold eqk; intros. rewrite H, <- H0. auto with smtcoq_array. *)
-  (* Qed. *)
-  
-  (* Lemma Inf_lt : forall l x y, ltk x y -> Inf y l -> Inf x l. *)
-  (* Proof. exact (InfA_ltA ltk_strorder). Qed. *)
-
-  (* Lemma Inf_eq : forall l x y, x = y -> Inf y l -> Inf x l. *)
-  (* Proof. exact (InfA_eqA eq_equiv ltk_compat). Qed. *)
-
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
-
   Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
   Proof.
   firstorder.
@@ -666,10 +588,6 @@ Module Raw.
     clear e0. inversion Hm. subst.
     apply Sort_Inf_NotIn with x0; auto with smtcoq_array.
 
-    (* clear e0;inversion_clear Hm. *)
-    (* apply Sort_Inf_NotIn with x0; auto with smtcoq_array. *)
-    (* apply Inf_eq with (k',x0);auto with smtcoq_array; compute; apply eq_trans with x; auto with smtcoq_array. *)
-
     clear e0;inversion_clear Hm.
     assert (notin:~ In y (remove y l)) by auto with smtcoq_array.
     intros (x1,abs).
@@ -755,7 +673,6 @@ Module Raw.
       | _ => idtac
       end.
     intros.
-    (* rewrite In_alt in *. *)
     destruct H0 as (e, H0).
     exists e.
     apply InA_cons_tl. auto with smtcoq_array.
@@ -764,7 +681,6 @@ Module Raw.
     inversion_clear Hm.
     apply In_inv in H0.
     destruct H0.
-    (* destruct (eq_dec k' y). *)
     exists _x.
     apply InA_cons_hd. split; simpl; auto with smtcoq_array.
     specialize (IHb H1 H H0).
@@ -1030,16 +946,11 @@ Section FArray.
   Qed.
 
   (** Boolean comparison over elements *)
-  Definition cmp (e e':elt) :=
-    match compare e e' with EQ _ => true | _ => false end.
-
+  Definition cmp := @compare2eqb _ _ elt_comp.
 
   Lemma cmp_refl : forall e, cmp e e = true.
-    unfold cmp.
-    intros.
-    destruct (compare e e); auto;
-      apply lt_not_eq in l; now contradict l.
-  Qed.
+  Proof. intro e. unfold cmp. now rewrite compare2eqb_spec. Qed.
+
 
   Lemma remove_nodefault : forall l (Hd:NoDefault l) (Hs:Sorted (Raw.ltk key_ord) l) x ,
       NoDefault (Raw.remove key_comp x l).
@@ -1072,29 +983,26 @@ Section FArray.
   Lemma add_nodefault : forall l (Hd:NoDefault l) (Hs:Sorted (Raw.ltk key_ord) l) x e,
       NoDefault (raw_add_nodefault x e l).
   Proof.
-    intros.
+    intros l Hd Hs x e.
     unfold raw_add_nodefault.
-    case_eq (cmp e default_value); intro; auto.
-    case_eq (Raw.mem key_comp x l); intro; auto.
-    apply remove_nodefault; auto.
-    unfold NoDefault; intros.
-    assert (e <> default_value).
-      unfold cmp in H.
-      case (compare e default_value) in H; try now contradict H.
-      apply lt_not_eq in l0; auto.
-      apply lt_not_eq in l0; now auto.
-    destruct (eq_dec k x).
-    - symmetry in e0.
-      apply (Raw.add_1 key_dec key_comp l e) in e0.
-      unfold not; intro.
-      specialize (Raw.add_sorted key_dec key_comp Hs x e).
-      intro Hsadd.
-      specialize (Raw.MapsTo_inj key_dec Hsadd e0 H1).
-      intro. contradiction.
-    - unfold not; intro.
-      assert (x <> k). unfold not in *. intro. apply n. symmetry; auto.
-      specialize (Raw.add_3 key_dec key_comp l e H2 H1).
-      intro. now apply Hd in H3.
+    case_eq (cmp e default_value); intro H; auto.
+    - case_eq (Raw.mem key_comp x l); intro H0; auto.
+      apply remove_nodefault; auto.
+    - unfold NoDefault; intros k.
+      assert (H0: e <> default_value).
+      { intro H1. subst e. rewrite cmp_refl in H. discriminate. }
+      destruct (eq_dec k x) as [e0|n].
+      + symmetry in e0.
+        apply (Raw.add_1 key_comp l e) in e0.
+        unfold not; intro.
+        specialize (Raw.add_sorted key_comp Hs x e).
+        intro Hsadd.
+        specialize (Raw.MapsTo_inj Hsadd e0 H1).
+        intro. contradiction.
+      + unfold not; intro.
+        assert (x <> k). unfold not in *. intro. apply n. symmetry; auto.
+        specialize (Raw.add_3 key_comp l e H2 H1).
+        intro. now apply Hd in H3.
   Qed.
 
   Definition empty : farray :=
@@ -1133,8 +1041,7 @@ Section FArray.
   Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.ltk key elt key_ord.
 
   Lemma MapsTo_1 : forall m x y e, eq x y -> MapsTo x e m -> MapsTo y e m.
-  Proof. intros m.
-    apply (Raw.MapsTo_eq key_dec elt_dec). Qed.
+  Proof. intros m. apply Raw.MapsTo_eq. Qed.
 
   Lemma mem_1 : forall m x, In x m -> mem x m = true.
   Proof. intros m; apply (Raw.mem_1); auto. apply m.(sorted). Qed.
@@ -1150,12 +1057,13 @@ Section FArray.
   Proof. intros m; apply Raw.is_empty_2. Qed.
 
   Lemma add_1 : forall m x y e, e <> default_value -> eq x y -> MapsTo y e (add x e m).
-  Proof. intros.
+  Proof.
+    intros m x y e H H0.
     unfold add, raw_add_nodefault.
     unfold MapsTo. simpl.
-    case_eq (cmp e default_value); intro; auto.
-    unfold cmp in H1. destruct (compare e default_value); try now contradict H1.
-    apply Raw.add_1; auto.
+    case_eq (cmp e default_value); intro H1; auto.
+    - elim H. unfold cmp in H1. now rewrite compare2eqb_spec in H1.
+    - apply Raw.add_1; auto.
   Qed.
 
   Lemma add_2 : forall m x y e e', ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
@@ -1203,7 +1111,7 @@ Section FArray.
   Proof. intros m; apply Raw.elements_3; auto. apply m.(sorted). Qed.
 
   Lemma elements_3w : forall m, NoDupA eq_key (elements m).
-  Proof. intros m; apply (Raw.elements_3w key_dec m.(sorted)). Qed.
+  Proof. intros m; apply (Raw.elements_3w m.(sorted)). Qed.
 
   Lemma cardinal_1 : forall m, cardinal m = length (elements m).
   Proof. intros; reflexivity. Qed.
@@ -1236,62 +1144,64 @@ Section FArray.
     apply (H k). unfold Raw.MapsTo. apply InA_cons_tl. apply H0.
   Qed.
 
-  Lemma raw_equal_eq : forall a (Ha: Sorted (Raw.ltk key_ord) a) b (Hb: Sorted (Raw.ltk key_ord) b),
+  Lemma raw_equal_eq :
+    forall a (Ha: Sorted (Raw.ltk key_ord) a) b (Hb: Sorted (Raw.ltk key_ord) b),
       Raw.equal key_comp cmp a b = true -> a = b.
   Proof.
-    induction a; intros.
-    simpl in H.
-    case b in *; auto.
-    now contradict H.
-    destruct a as (xa, ea).
-    simpl in H.
-    case b in *.
-    now contradict H.
-    destruct p as (xb, eb).
-    destruct (compare xa xb); auto; try (now contradict H).
-    rewrite andb_true_iff in H. destruct H.
-    unfold cmp in H.
-    destruct (compare ea eb); auto; try (now contradict H).
-    subst. apply f_equal.
-    apply IHa; auto.
-    now inversion Ha.
-    now inversion Hb.
+    induction a as [ |a a0 IHa]; intros Ha b Hb H.
+    - simpl in H.
+      case b in *; auto.
+      now contradict H.
+    - destruct a as (xa, ea).
+      simpl in H.
+      case b in *.
+      + now contradict H.
+      + destruct p as (xb, eb).
+        destruct (compare xa xb); auto; try (now contradict H).
+        rewrite andb_true_iff in H. destruct H as [H H0].
+        unfold cmp in H. rewrite compare2eqb_spec in H.
+        subst. apply f_equal.
+        apply IHa; auto.
+        * now inversion Ha.
+        * now inversion Hb.
   Qed.
 
   Lemma eq_equal : forall m m', eq m m' <-> equal m m' = true.
   Proof.
-    intros (l,Hl,Hd); induction l.
-    intros (l',Hl',Hd'); unfold eq; simpl.
-    destruct l'; unfold equal; simpl; intuition.
-    intros (l',Hl',Hd'); unfold eq.
-    destruct l'.
-    destruct a; unfold equal; simpl; intuition.
-    destruct a as (x,e).
-    destruct p as (x',e').
-    unfold equal; simpl.
-    destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; intuition.
-    unfold cmp at 1.
-    case (compare e e');
-    subst; intro HH; try (apply lt_not_eq in HH; now contradict HH);
-    clear HH; simpl.
-    inversion_clear Hl.
-    inversion_clear Hl'.
-    apply nodefault_tail in Hd.
-    apply nodefault_tail in Hd'.
-    destruct (IHl H Hd (Build_farray H2 Hd')).
-    unfold equal, eq in H5; simpl in H5; auto.
-    destruct (andb_prop _ _ H); clear H.
-    generalize H0; unfold cmp.
-    case (compare e e');
-    subst; intro HH; try (apply lt_not_eq in HH; now contradict HH);
-      auto; intro; discriminate.
-    destruct (andb_prop _ _ H); clear H.
-    inversion_clear Hl.
-    inversion_clear Hl'.
-    apply nodefault_tail in Hd.
-    apply nodefault_tail in Hd'.
-    destruct (IHl H Hd (Build_farray H3 Hd')).
-    unfold equal, eq in H6; simpl in H6; auto.
+    intros (l,Hl,Hd); induction l as [ |a l IHl].
+    - intros (l',Hl',Hd'); unfold eq; simpl.
+      destruct l'; unfold equal; simpl; intuition.
+    - intros (l',Hl',Hd'); unfold eq.
+      destruct l' as [ |p l'].
+      + destruct a; unfold equal; simpl; intuition.
+      + destruct a as (x,e).
+        destruct p as (x',e').
+        unfold equal; simpl.
+        destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; [intuition| |intuition].
+        split.
+        * intros [H0 H1].
+          unfold cmp, compare2eqb at 1.
+          case (compare e e');
+            subst; intro HH; try (apply lt_not_eq in HH; now contradict HH);
+              clear HH; simpl.
+          inversion_clear Hl.
+          inversion_clear Hl'.
+          apply nodefault_tail in Hd.
+          apply nodefault_tail in Hd'.
+          destruct (IHl H Hd (Build_farray H2 Hd')).
+          unfold equal, eq in H5; simpl in H5; auto.
+        * { intro H. destruct (andb_prop _ _ H) as [H0 H1]; clear H. split.
+            - generalize H0; unfold cmp, compare2eqb.
+              case (compare e e');
+                subst; intro HH; try (apply lt_not_eq in HH; now contradict HH);
+                  auto; intro; discriminate.
+            - inversion_clear Hl.
+              inversion_clear Hl'.
+              apply nodefault_tail in Hd.
+              apply nodefault_tail in Hd'.
+              destruct (IHl H Hd (Build_farray H3 Hd')).
+              unfold equal, eq in H6; simpl in H6; auto.
+          }
   Qed.
 
   Lemma eq_1 : forall m m', Equivb m m' -> eq m m'.
@@ -1509,37 +1419,40 @@ Section FArray.
 
   Lemma raw_add_d_rem : forall m (Hm: Sorted (Raw.ltk key_ord) m) x,
       raw_add_nodefault x default_value m = Raw.remove key_comp x m.
-    intros.
+  Proof.
+    intros m Hm x.
     unfold raw_add_nodefault.
     rewrite cmp_refl.
-    case_eq (Raw.mem key_comp x m); intro.
-    auto.
+    case_eq (Raw.mem key_comp x m); intro H; auto.
     apply Raw.mem_3 in H; auto.
     apply raw_equal_eq; auto.
-    apply Raw.remove_sorted; auto.
-    apply Raw.equal_1; auto.
-    apply Raw.remove_sorted; auto.
-    unfold Raw.Equivb.
-    split.
-    intros.
-    destruct (eq_dec x k). subst.
-    split. intro. contradiction.
-    intro. contradict H0.
-    apply Raw.remove_1; auto.
-    apply Raw.remove_4; auto.
-
-    intros.
-    destruct (eq_dec x k).
-    assert (exists e, InA (Raw.eqk (elt:=elt)) (k, e) (Raw.remove key_comp x m)).
-    exists e'. apply Raw.InA_eqke_eqk; auto.
-    rewrite <- Raw.In_alt in H2; auto.
-    contradict H2.
-    apply Raw.remove_1; auto.
-    apply key_comp.
-    apply (Raw.remove_2 key_comp Hm n) in H0.
-    specialize (Raw.remove_sorted key_comp Hm x). intros.
-    specialize (Raw.MapsTo_inj key_dec H2 H0 H1).
-    intro. subst. apply cmp_refl.
+    - apply Raw.remove_sorted; auto.
+    - apply Raw.equal_1; auto.
+      + apply Raw.remove_sorted; auto.
+      + unfold Raw.Equivb.
+        split.
+        * { intros k.
+            destruct (eq_dec x k) as [e|n].
+            - subst.
+              split.
+              + intro. contradiction.
+              + intro. contradict H0.
+                apply Raw.remove_1; auto.
+            - apply Raw.remove_4; auto.
+          }
+        * { intros k e e' H0 H1.
+            destruct (eq_dec x k) as [e0|n].
+            - assert (H2:exists e, InA (Raw.eqk (elt:=elt)) (k, e) (Raw.remove key_comp x m)).
+              { exists e'. apply Raw.InA_eqke_eqk; auto. }
+              rewrite <- Raw.In_alt in H2; auto.
+              + contradict H2.
+                apply Raw.remove_1; auto.
+              + apply key_comp.
+            - apply (Raw.remove_2 key_comp Hm n) in H0.
+              specialize (Raw.remove_sorted key_comp Hm x). intros H2.
+              specialize (Raw.MapsTo_inj H2 H0 H1).
+              intro H3. subst. apply cmp_refl.
+          }
   Qed.
 
   Lemma add_d_rem : forall m x, add x default_value m = remove x m.
@@ -1559,19 +1472,18 @@ Section FArray.
   Lemma add_eq_d : forall m x y,
       x = y -> find y (add x default_value m) = None.
   Proof.
-    intros.
-    simpl.
+    intros m x y h.
     rewrite add_d_rem.
     case_eq (find y (remove x m)); auto.
-    intros.
+    intros e H0.
     apply find_2 in H0.
     unfold MapsTo, Raw.MapsTo in H0.
-    assert (exists e, InA (Raw.eqk (elt:=elt)) (y, e) (remove x m).(this)).
-    exists e. apply Raw.InA_eqke_eqk in H0. auto.
+    assert (H1:exists e, InA (Raw.eqk (elt:=elt)) (y, e) (remove x m).(this)).
+    { exists e. apply Raw.InA_eqke_eqk in H0. auto. }
     rewrite <- Raw.In_alt in H1; auto.
-    contradict H1.
-    apply remove_1; auto.
-    apply key_comp.
+    - contradict H1.
+      apply remove_1; auto.
+    - apply key_comp.
   Qed.
 
   Lemma add_neq_o : forall m x y e,
@@ -1626,8 +1538,8 @@ Section FArray.
   Lemma Equiv_Equivb : forall m m', Equiv m m' <-> Equivb m m'.
   Proof.
     unfold Equiv, Equivb, Raw.Equivb, cmp; intuition; specialize (H1 k e e' H H2).
-    destruct (compare e e'); auto; apply lt_not_eq in l; auto.
-    destruct (compare e e'); auto; now contradict H1.
+    - unfold compare2eqb; destruct (compare e e'); auto; apply lt_not_eq in l; auto.
+    - unfold compare2eqb in *; destruct (compare e e'); auto; inversion H1.
   Qed.
 
   (** Composition of the two last results: relation between [Equal]
@@ -1653,17 +1565,17 @@ Section FArray.
   Proof.
     intros a i j v Heq.
     unfold select, store.
-    case_eq (cmp v default_value); intro; auto.
-    unfold cmp in H.
-    case (compare v default_value) in H; auto; try now contradict H.
-    rewrite e.
-    rewrite add_eq_d; auto.
-    assert (v <> default_value).
-    unfold cmp in H.
-    case (compare v default_value) in H; auto; try now contradict H.
-    apply lt_not_eq in l. auto.
-    apply lt_not_eq in l. auto.
-    rewrite (add_eq_o a Heq H0). auto.
+    case_eq (cmp v default_value); intro H; auto.
+    - unfold cmp, compare2eqb in H.
+      case (compare v default_value) as [ | |e] in H; auto; try now contradict H.
+      rewrite e.
+      rewrite add_eq_d; auto.
+    - assert (H0: v <> default_value).
+      { unfold cmp, compare2eqb in H.
+        case (compare v default_value) as [l|e|l] in H; auto; try now contradict H.
+        - apply lt_not_eq in l. auto.
+        - apply lt_not_eq in l. auto. }
+      rewrite (add_eq_o a Heq H0). auto.
   Qed.
 
   Lemma read_over_write : forall a i v, select (store a i v) i = v.
@@ -1904,10 +1816,10 @@ Section FArray.
     Qed.
 
     Definition diff (a b: farray) : key.
-      case_eq (equal a b); intro.
+    Proof.
+      case_eq (equal a b); intro H.
       - apply default_value.
       - apply (diff_index (notequal_neq H)).
-        (* destruct (diff_index_p H). apply x. *)
     Defined.
 
    Lemma select_at_diff: forall a b, a <> b ->
@@ -1934,12 +1846,12 @@ Arguments store {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
 Arguments diff {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _.
 Arguments equal {_} {_} {_} {_} {_} {_} {_}  _ _.
 Arguments equal_iff_eq {_} {_} {_} {_} {_} {_} {_} _ _.
-Arguments read_over_same_write {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _ _ _.
-Arguments read_over_write {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
-Arguments read_over_other_write {_} {_} {_} {_} {_} {_} {_} {_} _ _ _ _ _.
-Arguments extensionality {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
+Arguments read_over_same_write {_} {_} {_} {_} {_} {_} {_} _ _ _ _ _.
+Arguments read_over_write {_} {_} {_} {_} {_} {_} {_} _ _ _.
+Arguments read_over_other_write {_} {_} {_} {_} {_} {_} _ _ _ _ _.
+Arguments extensionality {_} {_} {_} {_} {_} {_} {_} _ _ _.
 Arguments extensionality2 {_} {_} {_} {_} {_} {_} {_} {_} {_} _.
-Arguments select_at_diff {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
+Arguments select_at_diff {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
 
 
 Declare Scope farray_scope.
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index e7acfa7..71450dc 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -1179,132 +1179,132 @@ Proof. intro la.
 Qed.
 
 Lemma valid_check_bbDiseq lres : C.valid rho (check_bbDiseq lres).
-Proof. 
-      unfold check_bbDiseq.
-      case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
-      case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
-        intros f Heq2.
-      case_eq (t_atom .[ f]); try (intros; now apply C.interp_true).
-
-      intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N| | | | ];
-         try (intros; now apply C.interp_true). intros a b Heq3.
-      case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
-      intros c Heq4.
-      case_eq c; try (intros; now apply C.interp_true).
-      intros la n1 Heq5.
-      case_eq (t_atom .[ b]); try (intros; now apply C.interp_true).
-      intros c0 Heq6.
-      case_eq c0; try (intros; now apply C.interp_true).
-      intros lb n2 Heq7.
-      case_eq (List_diseqb la lb && (N.of_nat (Datatypes.length la) =? n)%N
-              && (N.of_nat (Datatypes.length lb) =? n)%N 
-              && (n1 =? n)%N && (n2 =? n)%N);
-         try (intros; now apply C.interp_true). intros Heq8.
+Proof.
+  unfold check_bbDiseq.
+  case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
+  case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
+  intros f Heq2.
+  case_eq (t_atom .[ f]); try (intros; now apply C.interp_true).
 
-      unfold C.valid. simpl. rewrite orb_false_r.
-      unfold Lit.interp. rewrite Heq.
-      unfold Var.interp.
-      rewrite wf_interp_form; trivial. rewrite Heq2. simpl.
-      unfold Atom.interp_form_hatom, interp_hatom.
-      rewrite Atom.t_interp_wf; trivial.
-      rewrite Heq3. simpl.
-      rewrite !Atom.t_interp_wf; trivial.
-      rewrite Heq4, Heq6. simpl.
-      rewrite Heq5, Heq7. simpl.
+  intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N| | | | ];
+    try (intros; now apply C.interp_true). intros a b Heq3.
+  case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
+  intros c Heq4.
+  case_eq c; try (intros; now apply C.interp_true).
+  intros la n1 Heq5.
+  case_eq (t_atom .[ b]); try (intros; now apply C.interp_true).
+  intros c0 Heq6.
+  case_eq c0; try (intros; now apply C.interp_true).
+  intros lb n2 Heq7.
+  case_eq (List_diseqb la lb && (N.of_nat (Datatypes.length la) =? n)%N
+           && (N.of_nat (Datatypes.length lb) =? n)%N
+           && (n1 =? n)%N && (n2 =? n)%N);
+    try (intros; now apply C.interp_true). intros Heq8.
 
-        rewrite !andb_true_iff in Heq8.
-        destruct Heq8 as (((Heq8, Ha), Hb), Hc).
-        destruct Heq8 as (Heq8, Hd).
-        rewrite N.eqb_eq in Hb, Hc.
-        rewrite Hb, Hc.
-        rewrite Typ.N_cast_refl. simpl.
+  unfold C.valid. simpl. rewrite orb_false_r.
+  unfold Lit.interp. rewrite Heq.
+  unfold Var.interp.
+  rewrite wf_interp_form; trivial. rewrite Heq2. simpl.
+  unfold Atom.interp_form_hatom, interp_hatom.
+  rewrite Atom.t_interp_wf; trivial.
+  rewrite Heq3. simpl.
+  rewrite !Atom.t_interp_wf; trivial.
+  rewrite Heq4, Heq6. simpl.
+  rewrite Heq5, Heq7. simpl.
+
+  rewrite !andb_true_iff in Heq8.
+  destruct Heq8 as (((Heq8, Ha), Hb), Hc).
+  destruct Heq8 as (Heq8, Hd).
+  rewrite N.eqb_eq in Hb, Hc.
+  rewrite Hb, Hc.
+  rewrite Typ.N_cast_refl. simpl.
 
-        generalize wt_t_atom. unfold Atom.wt. unfold is_true.
-        rewrite PArray.forallbi_spec;intros.
+  generalize wt_t_atom. unfold Atom.wt. unfold is_true.
+  rewrite PArray.forallbi_spec;intros.
 
-        (* a *)
-        pose proof (H a). 
-        assert (a < PArray.length t_atom).
-        { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4, Heq5. easy. }
-        specialize (@H0 H1). rewrite Heq4 in H0. simpl in H0.
-        unfold get_type' in H0. unfold v_type in H0.
-        case_eq (t_interp .[ a]).
-        intros v_typea v_vala Htia. rewrite Htia in H0.
-        rewrite Atom.t_interp_wf in Htia; trivial.
-        rewrite Heq4, Heq5 in Htia. simpl in Htia.
-        rewrite Hb in Htia.
-        unfold Bval in Htia.
-        rewrite Heq5 in H0. simpl in H0.
-        inversion Htia.
-
-        generalize dependent v_vala.
-        rewrite <- H3. intros.
-
-        (* b *)
-        pose proof (H b). 
-        assert (b < PArray.length t_atom).
-        { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6, Heq7. easy. }
-        specialize (@H2 H4). rewrite Heq6 in H2. simpl in H2.
-        unfold get_type' in H2. unfold v_type in H2.
-        case_eq (t_interp .[ b]).
-        intros v_typeb v_valb Htib. rewrite Htib in H2.
-        rewrite Atom.t_interp_wf in Htib; trivial.
-        rewrite Heq6, Heq7 in Htib. simpl in Htib.
-        rewrite Hc in Htib.
-        unfold Bval in Htib.
-        rewrite Heq7 in H2. simpl in H2.
-        inversion Htib.
-
-        generalize dependent v_valb.
-        rewrite <- H6. intros.
-
-        (* f *)
-        pose proof (H f). 
-        assert (f < PArray.length t_atom).
-        { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. }
-        specialize (@H5 H7). rewrite Heq3 in H5. simpl in H5.
-        unfold get_type' in H5. unfold v_type in H5.
-        case_eq (t_interp .[ f]).
-        intros v_typef v_valf Htif. rewrite Htif in H5.
-        rewrite Atom.t_interp_wf in Htif; trivial.
-        rewrite Heq3 in Htif. simpl in Htif.
-        rewrite !Atom.t_interp_wf in Htif; trivial.
-        rewrite Heq4, Heq6 in Htif.
-        rewrite Heq5, Heq7 in Htif.
-        simpl in Htif.
-        rewrite Hb, Hc in Htif.
-        rewrite Typ.N_cast_refl in Htif.
-        unfold Bval in Htif.
-        rewrite !andb_true_iff in H5.
-        destruct H5. destruct H5.
-
-        inversion Htif.
-
-        generalize dependent v_valf.
-        rewrite <- H11. intros.
-
-        unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits.
-        rewrite N.eqb_eq in Ha, Hd.
-
-        generalize (BITVECTOR_LIST._of_bits_size la n).
-
-        unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits.
-
-        rewrite Hd.
-
-        generalize (BITVECTOR_LIST._of_bits_size lb n).
-        unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits.
-        rewrite Ha.
-        intros.
+  (* a *)
+  pose proof (H a).
+  assert (H1: a < PArray.length t_atom).
+  { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4, Heq5. easy. }
+  specialize (@H0 H1). rewrite Heq4 in H0. simpl in H0.
+  unfold get_type' in H0. unfold v_type in H0.
+  case_eq (t_interp .[ a]).
+  intros v_typea v_vala Htia. rewrite Htia in H0.
+  rewrite Atom.t_interp_wf in Htia; trivial.
+  rewrite Heq4, Heq5 in Htia. simpl in Htia.
+  rewrite Hb in Htia.
+  unfold Bval in Htia.
+  rewrite Heq5 in H0. simpl in H0.
+  inversion Htia.
+
+  generalize dependent v_vala.
+  rewrite <- H3. intros.
+
+  (* b *)
+  pose proof (H b).
+  assert (H4: b < PArray.length t_atom).
+  { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6, Heq7. easy. }
+  specialize (@H2 H4). rewrite Heq6 in H2. simpl in H2.
+  unfold get_type' in H2. unfold v_type in H2.
+  case_eq (t_interp .[ b]).
+  intros v_typeb v_valb Htib. rewrite Htib in H2.
+  rewrite Atom.t_interp_wf in Htib; trivial.
+  rewrite Heq6, Heq7 in Htib. simpl in Htib.
+  rewrite Hc in Htib.
+  unfold Bval in Htib.
+  rewrite Heq7 in H2. simpl in H2.
+  inversion Htib.
+
+  generalize dependent v_valb.
+  rewrite <- H6. intros.
+
+  (* f *)
+  pose proof (H f).
+  assert (H7: f < PArray.length t_atom).
+  { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. }
+  specialize (@H5 H7). rewrite Heq3 in H5. simpl in H5.
+  unfold get_type' in H5. unfold v_type in H5.
+  case_eq (t_interp .[ f]).
+  intros v_typef v_valf Htif. rewrite Htif in H5.
+  rewrite Atom.t_interp_wf in Htif; trivial.
+  rewrite Heq3 in Htif. simpl in Htif.
+  rewrite !Atom.t_interp_wf in Htif; trivial.
+  rewrite Heq4, Heq6 in Htif.
+  rewrite Heq5, Heq7 in Htif.
+  simpl in Htif.
+  rewrite Hb, Hc in Htif.
+  rewrite Typ.N_cast_refl in Htif.
+  unfold Bval in Htif.
+  rewrite !andb_true_iff in H5.
+  destruct H5. destruct H5.
+
+  inversion Htif.
+
+  generalize dependent v_valf.
+  rewrite <- H11. intros.
+
+  unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits.
+  rewrite N.eqb_eq in Ha, Hd.
+
+  generalize (BITVECTOR_LIST._of_bits_size la n).
+
+  unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits.
+
+  rewrite Hd.
+
+  generalize (BITVECTOR_LIST._of_bits_size lb n).
+  unfold BITVECTOR_LIST._of_bits, RAWBITVECTOR_LIST._of_bits.
+  rewrite Ha.
+  intros.
 
-        unfold Typ.i_eqb. simpl.
-        unfold BITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.bv_eq.
-        simpl.
-        rewrite e, e0.
-        rewrite N.eqb_refl.
-        unfold RAWBITVECTOR_LIST.bits.
+  change (Typ.i_eqb t_i (Typ.TBV n)) with (@BITVECTOR_LIST.bv_eq n).
+  unfold BITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.bv_eq.
+  simpl.
+  rewrite e, e0.
+  rewrite N.eqb_refl.
+  unfold RAWBITVECTOR_LIST.bits.
 
-        apply diseq_neg_eq. easy.
+  apply diseq_neg_eq. easy.
 Qed.
 
 Lemma prop_checkbb: forall (a: int) (bs: list _lit) (i n: nat),
@@ -4718,8 +4718,8 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres).
        (** case symmetry **)
 
 
-        (* interp_form_hatom_bv a1' = 
-                 interp_bv t_i (interp_atom (t_atom .[a1'])) *)
+        (* interp_form_hatom_bv a1' =  *)
+(*                  interp_bv t_i (interp_atom (t_atom .[a1'])) *)
         assert (interp_form_hatom_bv a1' =
                 interp_bv t_i (interp_atom (t_atom .[a1']))).
         {
@@ -4737,8 +4737,8 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres).
         rewrite Htia1 in HSp2.
         unfold interp_bv in HSp2.
 
-        (* interp_form_hatom_bv a2' =
-                 interp_bv t_i (interp_atom (t_atom .[a2'])) *)
+        (* interp_form_hatom_bv a2' = *)
+(*                  interp_bv t_i (interp_atom (t_atom .[a2'])) *)
         assert (interp_form_hatom_bv a2' =
                 interp_bv t_i (interp_atom (t_atom .[a2']))).
         {
diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 5f79faf..f8d5b50 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -28,7 +28,7 @@ Definition eqb_to_eq_dec :
   Defined.
 
 
-(** Types with a Boolean equality that reflects in Leibniz equality *)
+(** Types with a Boolean equality that reflects Leibniz equality *)
 Class EqbType T := {
  eqb : T -> T -> bool;
  eqb_spec : forall x y, eqb x y = true <-> x = y
@@ -37,32 +37,65 @@ Class EqbType T := {
 
 (** Types with a decidable equality *)
 Class DecType T := {
- eq_refl : forall x : T, x = x;
- eq_sym : forall x y : T, x = y -> y = x;
- eq_trans : forall x y z : T, x = y -> y = z -> x = z;
  eq_dec : forall x y : T, { x = y } + { x <> y }
 }.
 
 
-Hint Immediate eq_sym.
-Hint Resolve eq_refl eq_trans.
-
 (** Types equipped with Boolean equality are decidable *)
-Instance EqbToDecType T `(EqbType T) : DecType T.
-Proof.
-  destruct H.
-  split; auto.
-  intros; subst; auto.
-  apply (eqb_to_eq_dec _ eqb0); auto.
-Defined.
+Section EqbToDecType.
+  Generalizable Variable T.
+  Context `{ET : EqbType T}.
+
+  Instance EqbToDecType : DecType T.
+  Proof.
+    destruct ET as [eqb0 Heqb0]. split.
+    apply (eqb_to_eq_dec _ eqb0); auto.
+  Defined.
+End EqbToDecType.
+
+
+(** Basic properties on types with Boolean equality *)
+Section EqbTypeProp.
+  Generalizable Variable T.
+  Context `{ET : EqbType T}.
+
+  Lemma eqb_refl x : eqb x x = true.
+  Proof. now rewrite eqb_spec. Qed.
+
+  Lemma eqb_sym x y : eqb x y = true -> eqb y x = true.
+  Proof. rewrite !eqb_spec. now intros ->. Qed.
+
+  Lemma eqb_trans x y z : eqb x y = true -> eqb y z = true -> eqb x z = true.
+  Proof. rewrite !eqb_spec. now intros ->. Qed.
+
+  Lemma eqb_spec_false x y : eqb x y = false <-> x <> y.
+  Proof.
+    split.
+    - intros H1 H2. subst y. rewrite eqb_refl in H1. inversion H1.
+    - intro H. case_eq (eqb x y); auto. intro H1. elim H. now rewrite <- eqb_spec.
+  Qed.
+
+  Lemma reflect_eqb x y : reflect (x = y) (eqb x y).
+  Proof.
+    case_eq (eqb x y); intro H; constructor.
+    - now rewrite eqb_spec in H.
+    - now rewrite eqb_spec_false in H.
+  Qed.
+
+  Lemma eqb_sym2 x y : eqb x y = eqb y x.
+  Proof.
+    case_eq (eqb y x); intro H.
+    - now apply eqb_sym.
+    - rewrite eqb_spec_false in *. auto.
+  Qed.
+End EqbTypeProp.
 
 
 (** Class of types with a partial order *)
 Class OrdType T := {
   lt: T -> T -> Prop;
   lt_trans : forall x y z : T, lt x y -> lt y z -> lt x z;
-  lt_not_eq : forall x y : T, lt x y -> ~ eq x y
-  (* compare : forall x y : T, Compare lt eq x y *)
+  lt_not_eq : forall x y : T, lt x y -> x <> y
 }.
 
 Hint Resolve lt_not_eq lt_trans.
@@ -84,6 +117,29 @@ Class Comparable T {ot:OrdType T} := {
 }.
 
 
+(* A Comparable type is also an EqbType *)
+Section Comparable2EqbType.
+  Generalizable Variable T.
+  Context `{OTT : OrdType T}.
+  Context `{CT : Comparable T}.
+
+  Definition compare2eqb (x y:T) : bool :=
+    match compare x y with
+    | EQ _ => true
+    | _ => false
+    end.
+
+  Lemma compare2eqb_spec x y : compare2eqb x y = true <-> x = y.
+  Proof.
+    unfold compare2eqb.
+    case_eq (compare x y); simpl; intros e He; split; try discriminate;
+      try (intros ->; elim (lt_not_eq _ _ e (eq_refl _))); auto.
+  Qed.
+
+  Instance Comparable2EqbType : EqbType T := Build_EqbType _ _ compare2eqb_spec.
+End Comparable2EqbType.
+
+
 (** Class of inhabited types *)
 Class Inhabited T := {
   default_value : T
@@ -92,53 +148,44 @@ Class Inhabited T := {
 (** * CompDec: Merging all previous classes *)
 
 Class CompDec T := {
-  ty := T;
-  Eqb :> EqbType ty;
-  Decidable := EqbToDecType ty Eqb;
-  Ordered :> OrdType ty;       
-  Comp :> @Comparable ty Ordered;
-  Inh :> Inhabited ty
+  Eqb :> EqbType T;             (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *)
+  Ordered :> OrdType T;
+  Comp :> @Comparable T Ordered;
+  Inh :> Inhabited T
 }.
 
 
-Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) := 
-  let (_, _, _, ord, _, _) := c in ord.
+Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) :=
+  let (eqb, _, _, _) := c in eqb.
 
-Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) := 
-  let (_, _, _, _, _, inh) := c in inh.
+Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) :=
+  let (_, ord, _, _) := c in ord.
+
+Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) :=
+  let (_, _, _, inh) := c in inh.
 
 Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t).
-destruct c; trivial.
+  destruct c; trivial.
 Defined.
 
-Instance eqbtype_of_compdec t `{c: CompDec t} : EqbType t :=
-  let (_, eqbtype, _, _, _, inh) := c in eqbtype.
-
-Instance dec_of_compdec t `{c: CompDec t} : DecType t :=
-  let (_, _, dec, _, _, inh) := c in dec.
-
-
-Definition type_compdec {ty:Type} (cd : CompDec ty) := ty.
 
 Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool :=
-  match c with
-  | {| ty := ty; Eqb := {| eqb := eqb |} |} => eqb
+  match eqbtype_of_compdec t with
+  | {| eqb := eqb |} => eqb
   end.
 
 
 Lemma compdec_eq_eqb {T:Type} {c : CompDec T} : forall x y : T,
     x = y <-> eqb_of_compdec c x y = true.
 Proof.
-  destruct c. destruct Eqb0.
-  simpl. intros. rewrite eqb_spec0. reflexivity.
+  intros x y. destruct c as [[E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
 Qed.
 
 Hint Resolve
      ord_of_compdec
      inh_of_compdec
      comp_of_compdec
-     eqbtype_of_compdec
-     dec_of_compdec : typeclass_instances.
+     eqbtype_of_compdec : typeclass_instances.
 
 
 Record typ_compdec : Type := Typ_compdec {
@@ -146,28 +193,30 @@ Record typ_compdec : Type := Typ_compdec {
   te_compdec : CompDec te_carrier
 }.
 
+
 Section CompDec_from.
 
   Variable T : Type.
+
   Variable eqb' : T -> T -> bool.
+  Variable eqb'_spec : forall x y, eqb' x y = true <-> x = y.
+
   Variable lt' : T -> T -> Prop.
-  Variable d : T.
+  Hypothesis lt'_trans : forall x y z : T, lt' x y -> lt' y z -> lt' x z.
+  Hypothesis lt'_neq : forall x y : T, lt' x y -> x <> y.
 
-  Hypothesis eqb_spec' : forall x y : T, eqb' x y = true <-> x = y.
-  Hypothesis lt_trans': forall x y z : T, lt' x y -> lt' y z -> lt' x z.
-  Hypothesis lt_neq': forall x y : T, lt' x y -> x <> y.
-  
   Variable compare': forall x y : T, Compare lt' eq x y.
-  
+
+  Variable d : T.
+
   Program Instance CompDec_from : (CompDec T) := {|
-    Eqb := {| eqb := eqb' |};
-    Ordered := {| lt := lt'; lt_trans := lt_trans' |};
+    Eqb := {| eqb := eqb'; eqb_spec := eqb'_spec |};
+    Ordered := {| lt := lt'; lt_trans := lt'_trans |};
     Comp := {| compare := compare' |};
     Inh := {| default_value := d |}
   |}.
 
-  
   Definition typ_compdec_from : typ_compdec :=
     Typ_compdec T CompDec_from.
-  
+
 End CompDec_from.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 71318df..339d710 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -18,45 +18,37 @@ Require Export SMT_classes.
 
 
 Section Unit.
-
   Let eqb : unit -> unit -> bool := fun _ _ => true.
 
   Let lt : unit -> unit -> Prop := fun _ _ => False.
-  
-  Instance unit_ord : OrdType unit.
+
+  Global Instance unit_ord : OrdType unit.
   Proof. exists lt; unfold lt; trivial.
     intros; contradict H; trivial.
   Defined.
 
-  Instance unit_eqbtype : EqbType unit.
+  Global Instance unit_eqbtype : EqbType unit.
   Proof.
     exists eqb. intros. destruct x, y. unfold eqb. split; trivial.
   Defined.
 
-  Instance unit_comp : @Comparable unit unit_ord.
+  Global Instance unit_comp : @Comparable unit unit_ord.
   Proof.
     split. intros. destruct x, y.
     apply OrderedType.EQ; trivial.
   Defined.
 
-  Instance unit_inh : Inhabited unit := {| default_value := tt |}.
-  
-  Instance unit_compdec : CompDec unit := {|
+  Global Instance unit_inh : Inhabited unit := {| default_value := tt |}.
+
+  Global Instance unit_compdec : CompDec unit := {|
     Eqb := unit_eqbtype;
     Ordered := unit_ord;
     Comp := unit_comp;
     Inh := unit_inh
   |}.
 
-
-  
   Definition unit_typ_compdec := Typ_compdec unit unit_compdec.
 
-
-  Lemma eqb_eq_unit : forall x y, eqb x y <-> x = y.
-  Proof. intros. split; case x; case y; unfold eqb; intros; now auto.
-  Qed.
-  
 End Unit.
 
 
@@ -65,23 +57,17 @@ Section Bool.
   Definition ltb_bool x y := negb x && y.
 
   Definition lt_bool x y := ltb_bool x y = true.
-  
-  Instance bool_ord : OrdType bool.
+
+  Global Instance bool_ord : OrdType bool.
   Proof.
     exists lt_bool.
     intros x y z.
-    case x; case y; case z; intros; simpl; subst; auto. 
+    case x; case y; case z; intros; simpl; subst; auto.
     intros x y.
-    case x; case y; intros; simpl in H; easy. 
+    case x; case y; intros; simpl in H; easy.
   Defined.
 
-  Instance bool_eqbtype : EqbType bool :=
-    {| eqb := Bool.eqb; eqb_spec := eqb_true_iff |}.
-  
-  Instance bool_dec : DecType bool :=
-    EqbToDecType _ bool_eqbtype.
-
-  Instance bool_comp: Comparable bool.
+  Global Instance bool_comp: Comparable bool.
   Proof.
     constructor.
     intros x y.
@@ -99,11 +85,16 @@ Section Bool.
     case x in *; case y in *; auto.
   Defined.
 
-  Instance bool_inh : Inhabited bool := {| default_value := false|}.
+  Global Instance bool_eqbtype : EqbType bool :=
+    {| eqb := Bool.eqb; eqb_spec := eqb_true_iff |}.
+
+  Global Instance bool_dec : DecType bool := EqbToDecType.
+
+  Global Instance bool_inh : Inhabited bool := {| default_value := false|}.
 
-  Instance bool_compdec : CompDec bool := {|
-    Eqb := bool_eqbtype;                                    
-    Ordered := bool_ord;                                    
+  Global Instance bool_compdec : CompDec bool := {|
+    Eqb := bool_eqbtype;
+    Ordered := bool_ord;
     Comp := bool_comp;
     Inh := bool_inh
   |}.
@@ -119,36 +110,32 @@ End Bool.
 
 Section Z.
 
-  Instance Z_ord : OrdType Z.
+  Global Instance Z_ord : OrdType Z.
   Proof.
     exists Z_as_OT.lt.
     exact Z_as_OT.lt_trans.
     exact Z_as_OT.lt_not_eq.
   Defined.
 
-  Instance Z_eqbtype : EqbType Z :=
-    {| eqb := Z.eqb; eqb_spec := Z.eqb_eq |}.
-
-  (* Instance Z_eqbtype : EqbType Z := *)
-  (*   {| eqb := Zeq_bool; eqb_spec := fun x y => symmetry (Zeq_is_eq_bool x y) |}. *)
-  
-  Instance Z_dec : DecType Z :=
-    EqbToDecType _ Z_eqbtype.
 
-  
-  Instance Z_comp: Comparable Z.
+  Global Instance Z_comp: Comparable Z.
   Proof.
     constructor.
     apply Z_as_OT.compare.
   Defined.
 
+  Global Instance Z_eqbtype : EqbType Z :=
+    {| eqb := Z.eqb; eqb_spec := Z.eqb_eq |}.
+
+  Global Instance Z_dec : DecType Z := @EqbToDecType _ Z_eqbtype.
+
+
+  Global Instance Z_inh : Inhabited Z := {| default_value := 0%Z |}.
 
-  Instance Z_inh : Inhabited Z := {| default_value := 0%Z |}.
 
-    
-  Instance Z_compdec : CompDec Z := {|
-    Eqb := Z_eqbtype;                                    
-    Ordered := Z_ord;                                    
+  Global Instance Z_compdec : CompDec Z := {|
+    Eqb := Z_eqbtype;
+    Ordered := Z_ord;
     Comp := Z_comp;
     Inh := Z_inh
   |}.
@@ -202,7 +189,7 @@ Section Z.
 
   Lemma lt_Z_B2P': forall x y, ltP_Z x y <-> Z.lt x y.
   Proof. intros x y; split; intro H.
-         unfold ltP_Z in H. 
+         unfold ltP_Z in H.
          case_eq ((x <? y)%Z ); intros; rewrite H0 in H; try easy.
          now apply Z.ltb_lt in H0.
          apply lt_Z_B2P.
@@ -211,7 +198,7 @@ Section Z.
 
   Lemma le_Z_B2P': forall x y, leP_Z x y <-> Z.le x y.
   Proof. intros x y; split; intro H.
-         unfold leP_Z in H. 
+         unfold leP_Z in H.
          case_eq ((x <=? y)%Z ); intros; rewrite H0 in H; try easy.
          now apply Z.leb_le in H0.
          apply le_Z_B2P.
@@ -220,7 +207,7 @@ Section Z.
 
   Lemma gt_Z_B2P': forall x y, gtP_Z x y <-> Z.gt x y.
   Proof. intros x y; split; intro H.
-         unfold gtP_Z in H. 
+         unfold gtP_Z in H.
          case_eq ((x >? y)%Z ); intros; rewrite H0 in H; try easy.
          now apply Zgt_is_gt_bool in H0.
          apply gt_Z_B2P.
@@ -229,7 +216,7 @@ Section Z.
 
   Lemma ge_Z_B2P': forall x y, geP_Z x y <-> Z.ge x y.
   Proof. intros x y; split; intro H.
-         unfold geP_Z in H. 
+         unfold geP_Z in H.
          case_eq ((x >=? y)%Z ); intros; rewrite H0 in H; try easy.
          rewrite Z.geb_leb in H0. rewrite le_Z_B2P in H0.
          apply le_Z_B2P' in H0. now apply Z.ge_le_iff.
@@ -250,34 +237,33 @@ End Z.
 
 Section Nat.
 
-  Instance Nat_ord : OrdType nat.
+  Global Instance Nat_ord : OrdType nat.
   Proof.
-    
+
     exists Nat_as_OT.lt.
     exact Nat_as_OT.lt_trans.
     exact Nat_as_OT.lt_not_eq.
   Defined.
 
-  Instance Nat_eqbtype : EqbType nat :=
-    {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}.
-  
-  Instance Nat_dec : DecType nat :=
-    EqbToDecType _ Nat_eqbtype.
 
-  
-  Instance Nat_comp: Comparable nat.
+  Global Instance Nat_comp: Comparable nat.
   Proof.
     constructor.
     apply Nat_as_OT.compare.
   Defined.
 
+  Global Instance Nat_eqbtype : EqbType nat :=
+    {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}.
+
+  Global Instance Nat_dec : DecType nat := EqbToDecType.
+
 
-  Instance Nat_inh : Inhabited nat := {| default_value := O%nat |}.
+  Global Instance Nat_inh : Inhabited nat := {| default_value := O%nat |}.
 
-    
-  Instance Nat_compdec : CompDec nat := {|
-    Eqb := Nat_eqbtype;                                    
-    Ordered := Nat_ord;                                    
+
+  Global Instance Nat_compdec : CompDec nat := {|
+    Eqb := Nat_eqbtype;
+    Ordered := Nat_ord;
     Comp := Nat_comp;
     Inh := Nat_inh
   |}.
@@ -287,30 +273,29 @@ End Nat.
 
 Section Positive.
 
-  Instance Positive_ord : OrdType positive.
+  Global Instance Positive_ord : OrdType positive.
   Proof.
     exists Positive_as_OT.lt.
     exact Positive_as_OT.lt_trans.
     exact Positive_as_OT.lt_not_eq.
   Defined.
 
-  Instance Positive_eqbtype : EqbType positive :=
-    {| eqb := Pos.eqb; eqb_spec := Pos.eqb_eq |}.
-  
-  Instance Positive_dec : DecType positive :=
-    EqbToDecType _ Positive_eqbtype.
-
-  Instance Positive_comp: Comparable positive.
+  Global Instance Positive_comp: Comparable positive.
   Proof.
     constructor.
     apply Positive_as_OT.compare.
   Defined.
 
-  Instance Positive_inh : Inhabited positive := {| default_value := 1%positive |}.
+  Global Instance Positive_eqbtype : EqbType positive :=
+    {| eqb := Pos.eqb; eqb_spec := Pos.eqb_eq |}.
+
+  Global Instance Positive_dec : DecType positive := EqbToDecType.
 
-  Instance Positive_compdec : CompDec positive := {|
-    Eqb := Positive_eqbtype;                                    
-    Ordered := Positive_ord;                                    
+  Global Instance Positive_inh : Inhabited positive := {| default_value := 1%positive |}.
+
+  Global Instance Positive_compdec : CompDec positive := {|
+    Eqb := Positive_eqbtype;
+    Ordered := Positive_ord;
     Comp := Positive_comp;
     Inh := Positive_inh
   |}.
@@ -323,8 +308,8 @@ Section BV.
 
   Import BITVECTOR_LIST.
 
-  
-  Instance BV_ord n : OrdType (bitvector n).
+
+  Global Instance BV_ord n : OrdType (bitvector n).
   Proof.
     exists (fun a b => (bv_ult a b)).
     unfold bv_ult, RAWBITVECTOR_LIST.bv_ult.
@@ -342,15 +327,8 @@ Section BV.
     apply H. easy.
   Defined.
 
-  Instance BV_eqbtype n : EqbType (bitvector n) :=
-    {| eqb := @bv_eq n;
-       eqb_spec := @bv_eq_reflect n |}.
 
-  Instance BV_dec n : DecType (bitvector n) :=
-    EqbToDecType _ (BV_eqbtype n).
-
-  
-  Instance BV_comp n: Comparable (bitvector n).
+  Global Instance BV_comp n: Comparable (bitvector n).
   Proof.
     constructor.
     intros x y.
@@ -388,13 +366,19 @@ Section BV.
     now apply RAWBITVECTOR_LIST.rev_neq in H.
   Defined.
 
-  Instance BV_inh n : Inhabited (bitvector n) :=
+  Global Instance BV_eqbtype n : EqbType (bitvector n) :=
+    {| eqb := @bv_eq n;
+       eqb_spec := @bv_eq_reflect n |}.
+
+  Global Instance BV_dec n : DecType (bitvector n) := EqbToDecType.
+
+  Global Instance BV_inh n : Inhabited (bitvector n) :=
     {| default_value := zeros n |}.
 
 
-  Instance BV_compdec n: CompDec (bitvector n) := {|
-    Eqb := BV_eqbtype n;                                    
-    Ordered := BV_ord n;                                    
+  Global Instance BV_compdec n: CompDec (bitvector n) := {|
+    Eqb := BV_eqbtype n;
+    Ordered := BV_ord n;
     Comp := BV_comp n;
     Inh := BV_inh n
   |}.
@@ -405,10 +389,9 @@ End BV.
 
 Section FArray.
 
-  Instance FArray_ord key elt
+  Global Instance FArray_ord key elt
            `{key_ord: OrdType key}
            `{elt_ord: OrdType elt}
-           `{elt_dec: DecType elt}
            `{elt_inh: Inhabited elt}
            `{key_comp: @Comparable key key_ord} : OrdType (farray key elt).
   Proof.
@@ -419,10 +402,30 @@ Section FArray.
     apply lt_farray_not_eq in H.
     apply H.
     rewrite H0.
-    apply eqfarray_refl. auto.
+    apply eqfarray_refl.
   Defined.
 
-  Instance FArray_eqbtype key elt
+
+  Global Instance FArray_comp key elt
+           `{key_ord: OrdType key}
+           `{elt_ord: OrdType elt}
+           `{key_comp: @Comparable key key_ord}
+           `{elt_inh: Inhabited elt}
+           `{elt_comp: @Comparable elt elt_ord} : Comparable (farray key elt).
+  Proof.
+    constructor.
+    intros.
+    destruct (compare_farray key_comp elt_comp x y).
+    - apply OrderedType.LT. auto.
+    - apply OrderedType.EQ.
+      specialize (@eq_equal key elt key_ord key_comp elt_ord elt_comp elt_inh x y).
+      intros.
+      apply H in e.
+      now apply equal_eq in e.
+    - apply OrderedType.GT. auto.
+  Defined.
+
+  Global Instance FArray_eqbtype key elt
            `{key_ord: OrdType key}
            `{elt_ord: OrdType elt}
            `{elt_eqbtype: EqbType elt}
@@ -436,88 +439,48 @@ Section FArray.
     split.
     apply FArray.equal_eq.
     intros. subst. apply eq_equal. apply eqfarray_refl.
-    apply EqbToDecType. auto.
   Defined.
 
-  
-  Instance FArray_dec key elt
+  Global Instance FArray_dec key elt
            `{key_ord: OrdType key}
            `{elt_ord: OrdType elt}
            `{elt_eqbtype: EqbType elt}
            `{key_comp: @Comparable key key_ord}
            `{elt_comp: @Comparable elt elt_ord}
            `{elt_inh: Inhabited elt}
-    : DecType (farray key elt) :=
-    EqbToDecType _ (FArray_eqbtype key elt).
+    : DecType (farray key elt) := EqbToDecType.
 
-  
-  Instance FArray_comp key elt
-           `{key_ord: OrdType key}
-           `{elt_ord: OrdType elt}
-           `{elt_eqbtype: EqbType elt}
-           `{key_comp: @Comparable key key_ord}
-           `{elt_inh: Inhabited elt}
-           `{elt_comp: @Comparable elt elt_ord} : Comparable (farray key elt).
-  Proof.
-    constructor.
-    intros.
-    destruct (compare_farray key_comp (EqbToDecType _ elt_eqbtype) elt_comp x y).
-    - apply OrderedType.LT. auto.
-    - apply OrderedType.EQ.
-      specialize (@eq_equal key elt key_ord key_comp elt_ord elt_comp elt_inh x y).
-      intros.
-      apply H in e.
-      now apply equal_eq in e.
-    - apply OrderedType.GT. auto.
-  Defined.
-
-  Instance FArray_inh key elt
+  Global Instance FArray_inh key elt
            `{key_ord: OrdType key}
            `{elt_inh: Inhabited elt} : Inhabited (farray key elt) :=
     {| default_value := FArray.empty key_ord elt_inh |}.
 
 
-  Program Instance FArray_compdec key elt
+  Global Instance FArray_compdec key elt
           `{key_compdec: CompDec key}
           `{elt_compdec: CompDec elt} :
     CompDec (farray key elt) :=
     {|
       Eqb := FArray_eqbtype key elt;
       Ordered := FArray_ord key elt;
-      (*  Comp := FArray_comp key elt ; *)
+      Comp := FArray_comp key elt ;
       Inh := FArray_inh key elt
     |}.
-  
-  Next Obligation.
-    constructor.
-    destruct key_compdec, elt_compdec.
-    simpl in *.
-    unfold lt_farray.
-    intros. simpl.
-    unfold EqbToDecType. simpl.
-    case_eq (compare x y); intros.
-    apply OrderedType.LT.
-    destruct (compare x y); try discriminate H; auto.
-    apply OrderedType.EQ.
-    destruct (compare x y); try discriminate H; auto.
-    apply OrderedType.GT.
-    destruct (compare y x); try discriminate H; auto; clear H.
-  Defined.
 
 End FArray.
 
 
 Section Int63.
-  
+
   Local Open Scope int63_scope.
 
   Let int_lt x y :=
     if Int63Native.ltb x y then True else False.
-  
-  Instance int63_ord : OrdType int.
+
+  Global Instance int63_ord : OrdType int.
   Proof.
     exists int_lt; unfold int_lt.
-    - intros x y z. 
+    - intros x y z.
       case_eq (x < y); intro;
         case_eq (y < z); intro;
           case_eq (x < z); intro;
@@ -533,15 +496,9 @@ Section Int63.
       rewrite <- Int63Properties.to_Z_eq.
       exact (Z.lt_neq _ _ H).
   Defined.
-  
-  Instance int63_eqbtype : EqbType int :=
-    {| eqb := Int63Native.eqb; eqb_spec := Int63Properties.eqb_spec |}.
 
-  Instance int63_dec : DecType int :=
-    EqbToDecType _ int63_eqbtype.
 
-
-  Instance int63_comp: Comparable int.
+  Global Instance int63_comp: Comparable int.
   Proof.
     constructor.
     intros x y.
@@ -566,16 +523,20 @@ Section Int63.
       rewrite H0. auto.
   Defined.
 
+  Global Instance int63_eqbtype : EqbType int :=
+    {| eqb := Int63Native.eqb; eqb_spec := Int63Properties.eqb_spec |}.
+
+  Global Instance int63_dec : DecType int := EqbToDecType.
+
 
-  Instance int63_inh : Inhabited int := {| default_value := 0 |}.
-    
-  Instance int63_compdec : CompDec int := {|
-    Eqb := int63_eqbtype;                                    
-    Ordered := int63_ord;                                    
+  Global Instance int63_inh : Inhabited int := {| default_value := 0 |}.
+
+  Global Instance int63_compdec : CompDec int := {|
+    Eqb := int63_eqbtype;
+    Ordered := int63_ord;
     Comp := int63_comp;
     Inh := int63_inh
   |}.
-         
 
 End Int63.
 
@@ -586,25 +547,6 @@ Section option.
   Context `{HA : CompDec A}.
 
 
-  Definition option_eqb (x y : option A) : bool :=
-    match x, y with
-    | Some a, Some b => eqb a b
-    | None, None => true
-    | _, _ => false
-    end.
-
-
-  Lemma option_eqb_spec : forall (x y : option A), option_eqb x y = true <-> x = y.
-  Proof.
-    intros [a| ] [b| ]; simpl; split; try discriminate; auto.
-    - intro H. rewrite eqb_spec in H. now subst b.
-    - intros H. inversion H as [H1]. now rewrite eqb_spec.
-  Qed.
-
-
-  Instance option_eqbtype : EqbType (option A) := Build_EqbType _ _ option_eqb_spec.
-
-
   Definition option_lt (x y : option A) : Prop :=
     match x, y with
     | Some a, Some b => lt a b
@@ -631,7 +573,7 @@ Section option.
   Qed.
 
 
-  Instance option_ord : OrdType (option A) :=
+  Global Instance option_ord : OrdType (option A) :=
     Build_OrdType _ _ option_lt_trans option_lt_not_eq.
 
 
@@ -647,15 +589,15 @@ Section option.
     - now apply EQ.
   Defined.
 
+  Global Instance option_comp : Comparable (option A) := Build_Comparable _ _ option_compare.
 
-  Instance option_comp : Comparable (option A) := Build_Comparable _ _ option_compare.
+  Global Instance option_eqbtype : EqbType (option A) := Comparable2EqbType.
 
 
-  Instance option_inh : Inhabited (option A) := Build_Inhabited _ None.
+  Global Instance option_inh : Inhabited (option A) := Build_Inhabited _ None.
 
 
-  Instance option_compdec : CompDec (option A) := {|
-    Eqb := option_eqbtype;
+  Global Instance option_compdec : CompDec (option A) := {|
     Ordered := option_ord;
     Comp := option_comp;
     Inh := option_inh
@@ -670,27 +612,6 @@ Section list.
   Context `{HA : CompDec A}.
 
 
-  Fixpoint list_eqb (xs ys : list A) : bool :=
-    match xs, ys with
-    | nil, nil => true
-    | x::xs, y::ys => eqb x y && list_eqb xs ys
-    | _, _ => false
-    end.
-
-
-  Lemma list_eqb_spec : forall (x y : list A), list_eqb x y = true <-> x = y.
-  Proof.
-    induction x as [ |x xs IHxs]; intros [ |y ys]; simpl; split; try discriminate; auto.
-    - rewrite andb_true_iff. intros [H1 H2]. rewrite eqb_spec in H1. rewrite IHxs in H2. now subst.
-    - intros H. inversion H as [H1]. rewrite andb_true_iff; split.
-      + now rewrite eqb_spec.
-      + subst ys. now rewrite IHxs.
-  Qed.
-
-
-  Instance list_eqbtype : EqbType (list A) := Build_EqbType _ _ list_eqb_spec.
-
-
   Fixpoint list_lt (xs ys : list A) : Prop :=
     match xs, ys with
     | nil, nil => False
@@ -700,6 +621,22 @@ Section list.
     end.
 
 
+  Definition list_compare : forall (x y : list A), Compare list_lt Logic.eq x y.
+  Proof.
+    induction x as [ |x xs IHxs]; intros [ |y ys]; simpl.
+    - now apply EQ.
+    - now apply LT.
+    - now apply GT.
+    - case_eq (compare x y); intros l H.
+      + apply LT. simpl. now left.
+      + case_eq (IHxs ys); intros l1 H1.
+        * apply LT. simpl. right. split; auto. now apply eqb_spec.
+        * apply EQ. now rewrite l, l1.
+        * apply GT. simpl. right. split; auto. now apply eqb_spec.
+      + apply GT. simpl. now left.
+  Defined.
+
+
   Lemma list_lt_trans : forall (x y z : list A),
       list_lt x y -> list_lt y z -> list_lt x z.
   Proof.
@@ -720,39 +657,24 @@ Section list.
     induction x as [ |x xs IHxs]; intros [ |y ys]; simpl; auto.
     - discriminate.
     - intros [H1|[H1 H2]]; intros H; inversion H; subst.
-      + eapply lt_not_eq; eauto.
-      + eapply IHxs; eauto.
+      + now apply (lt_not_eq _ _ H1).
+      + now apply (IHxs _ H2).
   Qed.
 
 
-  Instance list_ord : OrdType (list A) :=
+  Global Instance list_ord : OrdType (list A) :=
     Build_OrdType _ _ list_lt_trans list_lt_not_eq.
 
 
-  Definition list_compare : forall (x y : list A), Compare list_lt Logic.eq x y.
-  Proof.
-    induction x as [ |x xs IHxs]; intros [ |y ys]; simpl.
-    - now apply EQ.
-    - now apply LT.
-    - now apply GT.
-    - case_eq (compare x y); intros l H.
-      + apply LT. simpl. now left.
-      + case_eq (IHxs ys); intros l1 H1.
-        * apply LT. simpl. right. split; auto. now apply eqb_spec.
-        * apply EQ. now rewrite l, l1.
-        * apply GT. simpl. right. split; auto. now apply eqb_spec.
-      + apply GT. simpl. now left.
-  Defined.
-
+  Global Instance list_comp : Comparable (list A) := Build_Comparable _ _ list_compare.
 
-  Instance list_comp : Comparable (list A) := Build_Comparable _ _ list_compare.
+  Global Instance list_eqbtype : EqbType (list A) := Comparable2EqbType.
 
 
-  Instance list_inh : Inhabited (list A) := Build_Inhabited _ nil.
+  Global Instance list_inh : Inhabited (list A) := Build_Inhabited _ nil.
 
 
-  Instance list_compdec : CompDec (list A) := {|
-    Eqb := list_eqbtype;
+  Global Instance list_compdec : CompDec (list A) := {|
     Ordered := list_ord;
     Comp := list_comp;
     Inh := list_inh